A System of Complete and Consistent Truth

Abstract 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 se-mantics. 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 log-ical 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 $ ¬. ϕ = ¬