Proofs as Games
Proofs as Games
复制标题
证明作为游戏
DOI：
10.1080/00029890.2000.12005233
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
P. Pudlák
中科院分区：
文献类型：
--
作者：
P. Pudlák
1.导论.证明语言和布尔函数复杂度的下界是复杂性理论中最困难的问题。我们可以证明下界只有在非常特殊的情况下，和著名的开放问题，其中最重要的dJ=。YJ？保持开放。逻辑学中一个密切相关的领域是关于证明命题证明长度的下界。在那里，情况是类似的，因为我们只能证明限制证明系统的指数下界。在基于公理模式和规则的常用证明系统中，证明证明长度的非平凡下界是一个很难的开放问题。在本文中，我通过一个例子展示了如何考虑证明长度的下界。两人游戏。在与他人的交流和竞争中，我们每天都在无意识地玩游戏。我们的大脑很好地适应了它，因此把数学问题当作一个游戏来解决通常有助于我们的直觉。
1. INTRODUCTION. Proving lower bounds on the complexity of languages and boolean functions is the hardest problem in complexity theory. We can prove lower bounds only in very special cases, and the famous open problems, represented by the most important among them dJ=.# YJ?, remain open. A closely related area in logic is concerned with proving lower bounds on the lengths of propositional proofs. There the situation is similar in that we can prove exponential lower bounds only for restricted proof systems. It is a hard open problem to prove nontrivial lower bounds on the lengths of proofs in the usual proof systems based on axiom schemas and rules.In this paper I show, using an example, how one can think of lower bounds on the lengths of proofs in terms of a two-player game. In communicating and competing with other people we are unconsciously playing games every day. Our brain is well adapted to it. Thus presenting a mathematical problem as a game often helps our intuition.