A System of Complete and Consistent Truth
A System of Complete and Consistent Truth
复制标题
完整且一致的真理体系
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
V. Halbach
中科院分区：
文献类型：
--
作者：
V. Halbach
To the axioms of Peano arithmetic formulated in a language with an additional unary predicate symbol T we add the rules of necessitation φ/Tφ and conecessitation Tφ/φ and axioms stating that T commutes with the logical connectives and quantifiers. By a result of McGee this theory is ω-inconsistent, but it can be approximated by models obtained by a kind of rule-of-revision semantics. Furthermore we prove that FS is equivalent to a system already studied by Friedman and Sheard and give an analysis of its proof theory. 1 Preliminaries Let L be the first-order language of arithmetic with symbols for all primitive recursive functions; that is, if [e] is a primitive recursive function with index e, a function symbol fe for [e] is available in L . We suppose that L has =, ¬, → and ∃ as logical symbols. If we expand L by adding the new predicate constant T we obtain the language LT. Throughout the whole paper we shall identify every expression ofLT with its Gödel number (under a standard gödelnumbering). Because we also identify languages with the set of their formulas, a language will be a set of natural numbers. All theories we shall discuss are extensions of Peano arithmetic: PA is the theory containing all defining equations of the primitive recursive functions and all the induction axioms in the full language LT. The index e of a primitive recursive function [e] will provide the defining equation(s) for the symbol fe associated with the index e. If a primitive recursive function h is explicitly given by some equations, we have a natural index e for this function which is again associated with a function symbol fe in the language L . Usually we shall denote this function symbol for h by h. . So h. naturally represents h in PA in the language L . It is useful to conceive of the logical connectives as functions of expressions (i.e., of natural numbers). So we have for negation a function symbol ¬. representing the operation of prefixing a negation symbol to an expression (and similarly for material implication and the existential quantifier). Hence we can show for every formula φ ∈ LT that: PA $ ¬. φ = ¬φ Received April 24, 1994; revised October 11, 1994
To the axioms of Peano arithmetic formulated in a language with an additional unary predicate symbol T we add the rules of necessitation φ/Tφ and conecessitation Tφ/φ and axioms stating that T commutes with the logical connectives and quantifiers. By a result of McGee this theory is ω-inconsistent, but it can be approximated by models obtained by a kind of rule-of-revision semantics. Furthermore we prove that FS is equivalent to a system already studied by Friedman and Sheard and give an analysis of its proof theory. 1 Preliminaries Let L be the first-order language of arithmetic with symbols for all primitive recursive functions; that is, if [e] is a primitive recursive function with index e, a function symbol fe for [e] is available in L . We suppose that L has =, ¬, → and ∃ as logical symbols. If we expand L by adding the new predicate constant T we obtain the language LT. Throughout the whole paper we shall identify every expression ofLT with its Gödel number (under a standard gödelnumbering). Because we also identify languages with the set of their formulas, a language will be a set of natural numbers. All theories we shall discuss are extensions of Peano arithmetic: PA is the theory containing all defining equations of the primitive recursive functions and all the induction axioms in the full language LT. The index e of a primitive recursive function [e] will provide the defining equation(s) for the symbol fe associated with the index e. If a primitive recursive function h is explicitly given by some equations, we have a natural index e for this function which is again associated with a function symbol fe in the language L . Usually we shall denote this function symbol for h by h. . So h. naturally represents h in PA in the language L . It is useful to conceive of the logical connectives as functions of expressions (i.e., of natural numbers). So we have for negation a function symbol ¬. representing the operation of prefixing a negation symbol to an expression (and similarly for material implication and the existential quantifier). Hence we can show for every formula φ ∈ LT that: PA $ ¬. φ = ¬φ Received April 24, 1994; revised October 11, 1994