Some results on the length of proofs
Some results on the length of proofs
复制标题
关于证明长度的一些结果
DOI：
10.1090/s0002-9947-1973-0432416-x
复制
发表时间：
1973
影响因子：
1.3
通讯作者：
R. Parikh
中科院分区：
文献类型：
--
作者：
R. Parikh
摘要。给定一个理论T，设A表示“A在T中有一个至多k行的证明”。本文考虑一个具有完全归纳法但加法和乘法是三元关系的Peano算术公式PA*。我们证明了PA* 的kA是可判定的，因此PA* 在弱规则下是闭的.哥德尔定理关于证明长度的一个类似物是一个简单的推论。1.导论.在本文中，我们将考虑有关证明的长度问题。现在，形式系统中给定公式的（最短）证明长度强烈依赖于系统的呈现方式。将其中一个定理作为公理加以补充，可以减少某些证明的长度。因此，为了得到有意义的结果，我们要么把自己局限于特定理论的特定形式化，要么制定一个标准来区分同一理论的“好的”和“不那么好的“形式化。我们将在这里采取第二种方法。特别是我们将考虑理论形式化的一些语言thelower谓词演算的手段有限数量的公理，axiomschemata和图解规则的推理。这类形式化包括经典算术和直觉算术的Hilbert型和Gentzen型形式化.图解系统。由于公理图式和推理规则在文献中通常是借助于公式变量来解释的，为了定义图式系统的概念，我们做了显而易见的事情，即，我们扩展了谓词演算的符号，以包括元数学符号，并强调替换为中心思想。精确细节
ABSTRACT. Given a theory T, let \-^A mean "A has a proof in T of at most k lines". We consider a formulation PA* of Peano arithmetic withfull induction but addition and multiplication being ternary relations. We showthat \-k A is decidable for PA* and hence PA* is closed under a weak enrule. Ananalogue of Godel's theorem on the length of proofs is an easy corollary. 1. Introduction. In this paper we shall consider questions regarding thelengthOjof proofs. Now the length of (the shortest) proof of a given formulain a formal system depends strongly on the way in which the system is pre-sented. E.g. adjoining one of the theorems as an axiom reduces the lengthof some proofs. Thus in order to get significant results, we have either toconfine ourselves to particular formalisations of particular theories or elseto tormulate a criterion which distinguishes "nice" and "not so nice"formalisations of the same theory. We shall take here the second approach.In particular we shall consider theories formalised in some language of thelower predicate calculus by means of a finite number of axioms, axiomschemata and schematic rules of inference. Formalisations of this kind willinclude Hilbert type and Gentzen type formalisations of classical and in-tuitionistic arithmetic.2. Schematic systems. Since axiom schemata and rules of inference aregenerally explained in the literature with the help of formula variables, inorder to define the notion of a schematic system we do the obvious, namely,we expand the notation of the predicate calculus to include metamathematicalsymbols and emphasize substitution as the central idea. Precise details