[FOM] 307:Formalized Consistency Problem Solved
Harvey Friedman
friedman at math.ohio-state.edu
Sun Jan 14 18:24:58 EST 2007
FROMAL STATEMENTS OF GODEL'S SECOND INCOMPLETENESS THEOREM
by
Harvey M. Friedman
January 14, 2007
Abstract. Informal statements of Godel's Second Incompleteness Theorem,
referred to as Informal Second Incompleteness, are simple and dramatic.
However, current versions of Formal Second Incompleteness are complicated
and awkward. We present new versions of Formal Second Incompleteness that
are simple, and informally imply Informal Second Incompleteness. These
results rest on the isolation of simple formal properties shared by
consistency statements. Here we do not address any issues concerning proofs
of Second Incompleteness.
1. SECOND INCOMPLETENESS FOR PA.
We start with the most commonly quoted form of Godel's Second Incompleteness
Theorem - for the system PA = Peano Arithmetic.
PA can be formulated in a number of languages. Of these, L(prim) is the most
suitable for supporting formalizations of the consistency of Peano
Arithmetic.
We write L(prim) for the language based on 0,S and all primitive recursive
function symbols. We let PA(prim) be the formulation of Peano Arithmetic for
the language L(prim). I.e., the nonlogical axioms of PA(prim) consist of the
axioms for successor, primitive recursive defining equations, and the
induction scheme applied to all formulas in L(prim).
INFORMAL SECOND INCOMPLETENESS (PA(prim)). Let A be a sentence in L(prim)
that adequately formalizes the consistency of PA(prim), in the informal
sense. Then PA(prim) does not prove A.
We have discovered the following result. We let PRA be the important
subsystem of PA(prim), based on the same language L(prim), where we require
that the induction scheme be applied only to quantifier free formulas of
L(prim).
FORMAL SECOND INCOMPLETENESS (PA(prim)). Let A be a sentence in L(prim) such
that every equation in L(prim) that is provable in PA(prim), is also
provable in PRA + A. Then PA(prim) does not prove A.
NOTE: We are referring to equations which may contain variables (open
equations).
We can think of the condition in the above Formal Second Incompleteness
(PA(prim)) as a formal adequacy condition on a formalization in L(prim) of
the consistency of PR(prim).
The following Thesis provides the needed connection between Formal and
Informal Second Incompleteness (PA(prim)).
INFORMAL THESIS (PA(prim)). Let A be a sentence in L(prim) that adequately
formalizes the consistency of PA(prim), in the informal sense. Then every
equation in L(prim) that is provable in PR(prim), is also provable in PRA +
A.
Informal Proof: Let Con(PA(prim)) be an adequate formalization in L(prim) of
the consistency of PA(prim), in the informal sense. Assume
1) s(x1,...,xk) = t(x1,...,xk) is provable in PA(prim)
where s(x1,...,xk),t(x1,...,xk) are terms in L(prim) whose variables are
among x1,...,xk, k >= 0.
We now argue in PRA + Con(PA(prim)). Let x1,...,xk in N, and assume not
s(x1,...,xk) = t(x1,...,xk). Let xi^ be the numeral for xi; i.e., S...S0,
where there are xi S's. Then, according to PRA,
2) PRA proves not s(x1^,...,xk^) = t(x1^,...,xk^).
In particular,
3) PA(prim) proves not s(x1^,...,xk^) = t(x1^,...,xk^).
>From 1) and 3), we see that PA(prim) is inconsistent. This contradicts
Con(PA(prim)). QED
>From the Informal Thesis (PA(prim)), we immediately see that Formal Second
Incompleteness (PR(prim)) implies Informal Second Incompleteness (PR(prim)).
Previous attempts to give a Formal Second Incompleteness (PR(prim)) through
a formal adequacy condition were comparatively unsatisfactory. There were
two existing approaches.
One is through the Hilbert Bernays derivability conditions and its variants.
These do not provide a direct condition on a formalization in L(prim) of the
consistency of PA(prim). Instead, a proof predicate is introduced, as well
as some auxiliary syntactic notions, and conditions are placed on all of
these notions, simultaneously. A fully rigorous development is rather subtle
and involved, and uses the construction of auxiliary sentences.
Another is the approach of S. Feferman, which places conditions on the
formalization of all the relevant syntactic notions that lead up to the
formalization in L(prim) of the consistency of PA(prim). These are more
straightforward than the Hilbert Bernays conditions, but significantly more
complicated than the Hilbert Bernays conditions. They are significantly less
complicated and ad hoc than any direct formalization in L(prim) of the
consistency of PA(prim). However, they also remain unacceptably complicated
for use in the statement of this vitally important theorem.
The development presented here does NOT address any issues concerning the
complications and subtleties present in PROOFS of the Second Incompleteness
Theorem. It only relates to the STATEMENT of Second Incompleteness.
2. MANY SORTED EXTENSIONS OF FULL INDUCTION WITH PRIM.
Let L(many) be many sorted predicate calculus. Here the sorts, constants,
relations, and functions are indexed using nonnegative integers.
Let L be a fragment of L(many) that contains L(prim). For definiteness, we
require that L(prim) lives in the first sort. We let the theory PA(L) in L
consist of the axioms for successor, the defining equations for the
primitive recursive function symbols of L(prim), and the induction scheme
applied to all formulas of L.
INFORMAL SECOND INCOMPLETENESS (many sorted induction, prim). Let L be a
fragment of L(many) containing L(prim). Let T be a consistent extension of
PA(L) in L. Let A be a sentence in L that adequately formalizes the
consistency of T, in the informal sense. Then T does not prove A.
FORMAL SECOND INCOMPLETENESS (many sorted induction, prim). Let L be a
fragment of L(many) containing L(prim). Let T be a consistent extension of
PA(L) in L. Let A be a sentence in L such that every equation in L(prim)
that is provable in T, is also provable in PRA + A. Then T does not prove A.
INFORMAL THESIS (many sorted induction, prim). Let L be a fragment of
L(many) containing L(prim). Let T be a consistent extension of PA(L) in L.
Let A be a sentence in L that adequately formalizes the consistency of T, in
the informal sense. Then every equation in L(prim) that is provable in T, is
also provable in PRA + A.
We now address the question of just which sentences obey the conditions in
Formal Incompleteness above.
THEOREM 2.1. Let L be a fragment of L(many) containing L(prim). Let T be an
extension of PA(L) in L. Let A be a sentence in L. The following are
equivalent.
i. Every equation in L(prim) that is provable in T, is also provable in PRA
+ A.
ii. PRA + A proves the formal consistency of every finite fragment of T.
Furthermore, if T is recursively axiomatized then the formal consistency of
T, formulated on the basis of an algorithm for the recursive axiomatization,
obeys i,ii. If T contains all true universally quantified equations in
L(prim), then for all A obeying i,ii, A is refutable in PRA.
3. GENERAL MANY SORTED THEOREIS WITH PRIM.
So far, all of our theorems apply only to contexts in which the induction
scheme for all formulas in the language are present in the theory. In
particular, we have not addressed finitely axiomatized T.
We say that a sentence is in Pi1(prim) if and only if it is a universally
quantified bounded formula in L(prim).
For n >= 0, we write ISigman(prim) for the fragment of PA(prim) where the
induction scheme is applied to Sigman(prim) formulas only. I.e., formulas in
L(prim) starting with at most n quantifiers, the first of which is
existential, followed by a quantifier free formula.
The following refutes our previous Formal Second Incompleteness, if we do
not insist on extending induction with respect to all formulas.
THEOREM 3.1. Let T be a fragment of ISigman(prim) containing PRA. There is a
theorem A of T such that every theorem of T lying in Pi1(prim) is provable
in PRA + A.
The key notion needed for General Second Incompleteness is the notion of
relativization. Let S,T be two theories in L(many), where every symbol
appearing in S also appears in T (with the same sort information). A
relativization of S in T consists of a formula in L(T) which, provably in T,
defines a nonempty set which contains the constants appearing in the axioms
of S, and which is closed under the operation symbols appearing in S, and
where the result of restricting the quantifiers present in S to this
nonempty set, is provable in T.
INFORMAL SECOND INCOMPLETENESS (general many sorted, prim). Let L be a
fragment of L(many) containing L(prim). Let T be a consistent extension of
PRA in L. Let A be a sentence in L that adequately formalizes the
consistency of T, in the informal sense. Then T does not prove A.
FORMAL SECOND INCOMPLETENESS (general many sorted, prim). Let L be a
fragment of L(many) containing L(prim). Let T be a consistent extension of
PRA in L. Let A be a sentence in L such that every universalized equation in
L(prim) with a relativization in T, is provable in PRA + A. Then
T does not prove A.
INFORMAL THESIS (general many sorted, prim). Let L be a fragment of L(many)
containing L(prim). Let T be a consistent extension of PRA in L. Let A be a
sentence in L that adequately formalizes the consistency of T, in the
informal sense. Then every universalized equation in L(prim) with a
relativization in T, is provable in PRA + A.
We now address the question of just which sentences obey the conditions in
Formal Incompleteness above.
THEOREM 3.2. Let L be a fragment of L(many) containing L(prim). Let T be an
extension of PRA in L. Let A be a sentence in L. The following are
equivalent.
i. Every universalized equation in L(prim) with a relativization in T, is
provable in PRA + A.
ii. PRA + A proves the formal consistency of every finite fragment of T.
If T is finitely axiomatized, then condition ii asserts that PRA + A proves
the formal consistency of T.
4. MANY SORTED EXTENSIONS OF FULL INDUCTION WITH EXPARITH.
Let L(arith) be the single sorted language based on 0,S,+,dot. Let
L(exparith) be the single sorted language based on 0,S,+,dot,exp, where exp
is the binary exponential function (where exp(x,0) = 1).
Let ISigma0(exparith) be the fragment of PA(exparith) where induction is
applied to bounded formulas in L(exparith), only.
Let ISigma0(arith) be the fragment of PA(arith) where induction is applied
to bounded formulas in L(arith), only.
INFORMAL SECOND INCOMPLETENESS (many sorted induction, exparith). Let L be a
fragment of L(many) containing L(exparith). Let T be a consistent extension
of PA(L) in L. Let A be a sentence in L that adequately formalizes the
consistency of T, in the informal sense. Then T does not prove A.
FORMAL SECOND INCOMPLETENESS (many sorted induction, exparith). Let L be a
fragment of L(many) containing L(exparith). Let T be a consistent extension
of PA(L) in L. Let A be a sentence in L such that every inequation in
L(exparith) that is provable in T, is also provable in ISigma0(exparith) +
A. Then T does not prove A.
INFORMAL THESIS (many sorted induction, exparith). Let L be a fragment of
L(many) containing L(exparith). Let T be a consistent extension of PA(L) in
L. Let A be a sentence in L that adequately formalizes the consistency of T,
in the informal sense. Then every inequation in L(prim) that is provable in
T, is also provable in ISigma0(exparith) + A.
THEOREM 4.1. Let L be a fragment of L(many) containing L(exparith). Let T be
an extension of PA(L) in L. Let A be a sentence in L. The following are
equivalent.
i. Every inequation in L(exparith) that is provable in T, is also provable
in ISigma0(exparith) + A.
ii. ISigma0(exparith) + A proves the formal consistency of every finite
fragment of T.
Furthermore, if T is recursively axiomatized then the formal consistency of
T, formulated on the basis of an algorithm for the recursive axiomatization,
obeys i,ii. If T contains all true universally quantified equations in
L(exparith), then for all such A, ISigma0(exparith) + A is inconsistent.
5. GENERAL MANY SORTED THEORIES WITH EXPARITH.
INFORMAL SECOND INCOMPLETENESS (general many sorted, exparith). Let L be a
fragment of L(many) containing L(exparith). Let T be a consistent extension
of ISigma0(exparith) in L. Let A be a sentence in L that adequately
formalizes the consistency of T, in the informal sense. Then T does not
prove A.
FORMAL SECOND INCOMPLETENESS (general many sorted, exparith). Let L be a
fragment of L(many) containing L(exparith). Let T be a consistent extension
of ISigma0(exparith) in L. Let A be a sentence in L such that every
universalized inequation in L(exparith) with a relativization in T, is
provable in ISigma0(exparith) + A. Then T does not prove A.
INFORMAL THESIS (general many sorted, exparith). Let L be a fragment of
L(many) containing L(exparith). Let T be an extension of ISigma0(exparith)
in L. Let A be a sentence in L that adequately formalizes the consistency of
T, in the informal sense. Then every universalized inequation in L(exparith)
with a relativization in T, is provable in ISigma0(exparith) + A.
THEOREM 5.1. Let L be a fragment of L(many) containing L(prim). Let T be an
extension of ISigma0(exparith). Let A be as sentence in L. The following are
equivalent.
i. Every inequation in L(exparith) with a relativization in T, is also
provable in ISigma0(exparith) + A.
ii. ISigma0(exparith) + A proves the formal consistency of every finite
fragment of T.
If T is finitely axiomatized, then condition ii asserts that
ISigma0(exparith) + A proves the formal consistency of T.
6. GENERAL MANY SORTED THEORIES WITH ARITH.
Here we need to consider Pi1(arith) sentences. These are the result of
placing zero or more universal quantifiers in front of a bounded formula of
L(arith).
INFORMAL SECOND INCOMPLETENESS (general many sorted, arith). Let L be a
fragment of L(many) containing L(arith). Let T be a consistent extension
of ISigma0(arith) in L. Let A be a sentence in L that adequately
formalizes the consistency of T, in the informal sense. Then T does not
prove A.
FORMAL SECOND INCOMPLETENESS (general many sorted, arith). Let L be a
fragment of L(many) containing L(arith). Let T be a consistent extension
of ISigma0(arith) in L. Let A be a sentence in L such that every
sentence in Pi1(arith) with a relativization in T, is provable in
ISigma0(arith) + A. Then T does not prove A.
INFORMAL THESIS (general many sorted, arith). Let L be a fragment of
L(many) containing L(arith). Let T be an extension of ISigma0(arith) in L.
Let A be a sentence in L that adequately formalizes the consistency of T, in
the informal sense. Then every sentence in Pi1(arith) with a relativization
in T, is provable in ISigma0(arith) + A.
**********************************
I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 307th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.
250. Extreme Cardinals/Pi01 7/31/05 8:34PM
251. Embedding Axioms 8/1/05 10:40AM
252. Pi01 Revisited 10/25/05 10:35PM
253. Pi01 Progress 10/26/05 6:32AM
254. Pi01 Progress/more 11/10/05 4:37AM
255. Controlling Pi01 11/12 5:10PM
256. NAME:finite inclusion theory 11/21/05 2:34AM
257. FIT/more 11/22/05 5:34AM
258. Pi01/Simplification/Restatement 11/27/05 2:12AM
259. Pi01 pointer 11/30/05 10:36AM
260. Pi01/simplification 12/3/05 3:11PM
261. Pi01/nicer 12/5/05 2:26AM
262. Correction/Restatement 12/9/05 10:13AM
263. Pi01/digraphs 1 1/13/06 1:11AM
264. Pi01/digraphs 2 1/27/06 11:34AM
265. Pi01/digraphs 2/more 1/28/06 2:46PM
266. Pi01/digraphs/unifying 2/4/06 5:27AM
267. Pi01/digraphs/progress 2/8/06 2:44AM
268. Finite to Infinite 1 2/22/06 9:01AM
269. Pi01,Pi00/digraphs 2/25/06 3:09AM
270. Finite to Infinite/Restatement 2/25/06 8:25PM
271. Clarification of Smith Article 3/22/06 5:58PM
272. Sigma01/optimal 3/24/06 1:45PM
273: Sigma01/optimal/size 3/28/06 12:57PM
274: Subcubic Graph Numbers 4/1/06 11:23AM
275: Kruskal Theorem/Impredicativity 4/2/06 12:16PM
276: Higman/Kruskal/impredicativity 4/4/06 6:31AM
277: Strict Predicativity 4/5/06 1:58PM
278: Ultra/Strict/Predicativity/Higman 4/8/06 1:33AM
279: Subcubic graph numbers/restated 4/8/06 3:14AN
280: Generating large caridnals/self embedding axioms 5/2/06 4:55AM
281: Linear Self Embedding Axioms 5/5/06 2:32AM
282: Adventures in Pi01 Independence 5/7/06
283: A theory of indiscernibles 5/7/06 6:42PM
284: Godel's Second 5/9/06 10:02AM
285: Godel's Second/more 5/10/06 5:55PM
286: Godel's Second/still more 5/11/06 2:05PM
287: More Pi01 adventures 5/18/06 9:19AM
288: Discrete ordered rings and large cardinals 6/1/06 11:28AM
289: Integer Thresholds in FFF 6/6/06 10:23PM
290: Independently Free Minds/Collectively Random Agents 6/12/06 11:01AM
291: Independently Free Minds/Collectively Random Agents (more) 6/13/06
5:01PM
292: Concept Calculus 1 6/17/06 5:26PM
293: Concept Calculus 2 6/20/06 6:27PM
294: Concept Calculus 3 6/25/06 5:15PM
295: Concept Calculus 4 7/3/06 2:34AM
296: Order Calculus 7/7/06 12:13PM
297: Order Calculus/restatement 7/11/06 12:16PM
298: Concept Calculus 5 7/14/06 5:40AM
299: Order Calculus/simplification 7/23/06 7:38PM
300: Exotic Prefix Theory 9/14/06 7:11AM
301: Exotic Prefix Theory (correction) 9/14/06 6:09PM
302: PA Completeness 10/29/06 2:38AM
303: PA Completeness (restatement) 10/30/06 11:53AM
304: PA Completeness/strategy 11/4/06 10:57AM
305: Proofs of Godel's Second 12/21/06 11:31AM
306: Godel's Second/more 12/23/06 7:39PM
Harvey Friedman
More information about the FOM
mailing list