If no optimal propositional proof system exists, we (and independently Pudl\'ak) prove that ruling out length $t$ proofs of any unprovable sentence is hard. This mapping from unprovable to hard-to-prove sentences powerfully translates facts about noncomputability into complexity theory. For instance, because proving string $x$ is Kolmogorov random ($x{\in}R$) is typically impossible, it is typically hard to prove "no length $t$ proof shows $x{\in}R$", or tautologies encoding this. Therefore, a proof system with one family of hard tautologies has these densely in an enumeration of families. The assumption also implies that a natural language is $\textbf{NP}$-intermediate: with $R$ redefined to have a sparse complement, the complement of the language $\{\langle x,1^t\rangle|$ no length $t$ proof exists of $x{\in}R\}$ is also sparse. Efficiently ruling out length $t$ proofs of $x{\in}R$ might violate the constraint on using the fact of $x{\in}R$'s unprovability. We conjecture: any computable predicate on $R$ that might be used in if-then statements (or case-based proofs) does no better than branching at random, because $R$ appears random by any effective test. This constraint could also inhibit the usefulness in circuits and propositional proofs of NOT gates and cancellation -- needed to encode if-then statements. If $R$ defeats if-then logic, exhaustive search is necessary.


翻译:如果不存在最优命题证明系统,我们(以及Pudl\'{a}k)证明,排除任何不可证明句子的长度为$t$的证明是困难的。从不可计算性到复杂性理论的这种映射将非计算性事实强有力地转化为复杂性理论。例如,因为证明字符串$x$为 Kolmogorov 随机序列($x{\in}R$)通常是不可能的,所以证明“长度为$t$的证明没有展示$x{\in}R$”或者编码这个的tautologies通常是困难的。因此,有一个具有一个困难tautologies族的证明系统在这个族的枚举中有着密集的存在。这个假设还意味着自然语言是$\textbf{NP}$-intermediate:当将$R$重新定义为具有稀疏补集时,$x{\in}R$不存在长度为$t$的证明的集合的补集也是稀疏的。有效地排除$x{\in}R$的长度为$t$的证明可能违反$x{\in}R$不可证明的事实的限制。我们猜想:任何可能被用于if-then语句(或基于案例的证明)中的$R$的计算谓词执行的效果都不会比随机分支更好,因为通过任何有效性检验,$R$看起来都是随机的。这个限制也可能阻碍NOT门和消除的电路和命题证明的有用性-这些都是用于编码if-then语句。如果$R$击败了if-then逻辑,穷尽搜索是必要的。

0
下载
关闭预览

相关内容

【2023新书】程序证明,Program Proofs,642页pdf
专知会员服务
63+阅读 · 2023年3月29日
Graph Transformer近期进展
专知会员服务
61+阅读 · 2023年1月5日
专知会员服务
21+阅读 · 2021年10月8日
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
征稿 | International Joint Conference on Knowledge Graphs (IJCKG)
开放知识图谱
2+阅读 · 2022年5月20日
使用BERT做文本摘要
专知
23+阅读 · 2019年12月7日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年5月23日
Arxiv
38+阅读 · 2021年8月31日
VIP会员
相关资讯
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员