A semantics of evidence for classical arithmetic
A semantics of evidence for classical arithmetic
复制标题
经典算术证据的语义
DOI：
--
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
T. Coquand
中科院分区：
文献类型：
--
作者：
T. Coquand
如果从经典的观点很难给出一致性证明的确切意义，特别是根岑[2，6]和诺维科夫[14]的证明，这些证明的动机是非常直观的。因此，它们的意义不在于仅仅给出一个相容性证明，而在于对经典真理的概念给出一个直观的解释。例如，根岑总结他的证明如下：“因此，现实主义数学的命题似乎有一定的效用，但没有意义。然而，我的一致性证明的主要部分恰恰在于将有限主义意义归于现实主义命题。从这个观点来看，根岑和诺维科夫的论证的主要部分都可以说是确立了肯定前件在相对论意义上是有效的。这种解释把“有限意义”归于经典命题。在本文中，我们将根岑和诺维科夫的算术命题的“有限意义”重新表述为与之相关的博弈的获胜策略（将证明视为直觉主义逻辑的获胜策略）。根据并发理论[7]，将策略视为交互式程序是很有诱惑力的（因此它代表了算术命题的“有限意义”）。我们将证明，肯定前件的有效性，然后得到一个相当自然的公式，表明两个程序之间的“内部喋喋不休”最终结束。我们首先提出了Novikoff的正则公式的概念，它可以被看作是经典无穷命题演算的直觉真理定义。我们使用这一点，以激励第二部分，其中提出了一个博弈论的解释的概念，正规公式，并证明了可接受的肯定前件是基于这种解释。
If it is difficult to give the exact significance of consistency proofs from a classical point of view, in particular the proofs of Gentzen [2, 6], and Novikoff [14], the motivations of these proofs are quite clear intuitionistically. Their significance is then less to give a mere consistency proof than to present an intuitionistic explanation of the notion of classical truth. Gentzen for instance summarizes his proof as follows [6]: “Thus propositions of actualist mathematics seem to have a certain utility, but no sense. The major part of my consistency proof, however, consists precisely in ascribing a finitist sense to actualist propositions.” From this point of view, the main part of both Gentzen's and Novikoff's arguments can be stated as establishing that modus ponens is valid w.r.t. this interpretation ascribing a “finitist sense” to classical propositions. In this paper, we reformulate Gentzen's and Novikoff's “finitist sense” of an arithmetic proposition as a winning strategy for a game associated to it. (To see a proof as a winning strategy has been considered by Lorenzen [10] for intuitionistic logic.) In the light of concurrency theory [7], it is tempting to consider a strategy as an interactive program (which represents thus the “finitist sense” of an arithmetic proposition). We shall show that the validity of modus ponens then gets a quite natural formulation, showing that “internal chatters” between two programs end eventually. We first present Novikoff's notion of regular formulae, that can be seen as an intuitionistic truth definition for classical infinitary propositional calculus. We use this in order to motivate the second part, which presents a game-theoretic interpretation of the notion of regular formulae, and a proof of the admissibility of modus ponens which is based on this interpretation.