[FOM] 343:Goedel's Second Revisited 1
Harvey Friedman
friedman at math.ohio-state.edu
Wed May 27 06:07:33 EDT 2009
There have been some breakthroughs in our understanding of Goedel's
Second Incompleteness Theorem that goes well beyond our previous
postings on this topic.
GOEDEL'S SECOND INCOMPLETENESS THEOREM REVISITED 1
by
Harvey M. Friedman
May 27, 2009
1. Introduction.
2. The Innovation.
3. Extensions of PA(0,S,+,dot) in L(0,S,+,dot).
4. Extensions of EFA(0,S,+,dot) in L(0,S,+,dot).
5. To be continued.
1. INTRODUCTION.
There are some unresolved issues regarding Goedel's Second
Incompleteness Theorem. These concern both statements of the theorem,
and its proofs.
I have already written about Goedel's Second in FOM postings:
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
305: Proofs of Godel's Second 12/21/06 11:31AM
306: Godel's Second/more 12/23/06 7:39PM
307: Formalized Consistency Problem Solved 1/14/07 6:24PM
The most innovative of these postings is #307, at http://www.cs.nyu.edu/pipermail/fom/2007-January/011282.html
Also see
[1] H. Friedman, Formal statements of Goedel's second incompleteness
theorem, January 14, 2007, 8 pages, abstract. #56, http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html
[2] H. Friedman, My Forty Years On His Shoulders, November 5, 2008, to
appear in the proceedings of the Goedel Centenary meeting in Vienna,
held in April, 2006, Horizons of Truth, 69 pages. #58, http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html
look at section 4.
[2] has an account of #307, [1], and my modern form of Hilbert Bernays
type derivability conditions.
There I address the following state of affairs with regard to Godel's
Second:
All of the formal statements of Goedel's Second range from extremely
complicated to uncomfortably complicated.
This is not an ideal state of affairs for arguably the greatest
theorem of mathematical logic. E.g., compare these extremely
complicated to very complicated statements to the extremely simple
case of FLT.
Here are current approaches to stating Goedel's Second for PA, formally:
A. Slog through in complete detail, some formalization of syntax of
PA, finally arriving at the consistency statement, Con(PA), in the
language of PA. Goedel's Second asserts that this particular Con(PA)
is not provable in PA, assuming PA is consistent. This corresponds to
Goedel's original.
B. Do 1 more generally, identifying exactly what PA provability
properties are required concerning the large number of notions
introduced in 1. This is the approach of Feferman in
S. Feferman, Arithmetization of metamathematics in a general setting,
Fund. Math., vol. 49, pp. 35-92, 1960.
S. Feferman, Inductively presented systems and the formalization of
meta-mathematics, in Logic Colloquium '80, pp. 95-128, North-Holland,
Amsterdam, 1982.
S. Feferman, My route to arithmetization. Theoria 63(1997), 168-181.
C. An approach of Quine, mentioned in my [2]. Instead of formalizing
Con(PA) within PA, as in 1,2 above, create an extension of PA using
new symbols, which are added for all of the relevant concepts in 1.
Use lots of new sorts. The axioms consist of facts about these new
notions. Goedel's Second asserts that Con(PA) - which is stated in the
extended language - is not provable in the extended system. A benefit
of Quine's approach is that we avoid having formal systems talk about
their own syntax.
D. Hilbert Bernays, and some more modern, derivability conditions. For
my modern version, see [2].
ASSESSMENT: A-C are extremely complicated, and D is uncomfortably
complicated. The layers of provability are confusing, if done
absolutely correctly.
E. New approach in #307, [1], and also see [2]. The statement is
comparatively very simple.
2. THE INNOVATION.
The idea is to drastically simplify the hypotheses. The problem is
that we still have to argue that we really have proved the intended
theorem.
We can all imagine what is involved in constructing a reasonable
formalization of Con(PA) within PA. Our approach is to state simple
and convincing formal properties of what formal sentence of PA results
in this imagined process. The Principal Innovation is that
*we avoid any use of provability predicates.*
The reasons for taking this approach: provability predicates lead to
unpleasant complications, although they are perfectly handled in my
[2]. I am very happy with that - for what it is - and I do use it in
the classroom.
The crucial methodological idea is this, which we illustrate only for
the system PA based on 0,S,+,dot:
i. Formulate a necessary formal condition for a statement to express
Con(PA) within PA.
ii. Prove that the standard formal Con(PA) obeys this formal condition.
iii. Observe that almost nobody actually constructs a formal Con(PA) -
but rather simply imagines what is involved. In fact, there is no one
preferred formal Con(PA), and so one naturally reasons only semi
formally about imagined formal Con(PA) statements. So ii is really a
semi formal proof that any reasonable formulation of Con(PA) obeys
this formal condition.
iv. Prove that any sentence that obeys the formal condition is
unprovable in PA (assuming PA is consistent). Again, this is done
according to the usual standards for publication in mathematical
logic. Of course, this is an entirely rigorous statement that is
subject to the usual standards of proof in mathematics.
This was carried out in #307, [1], [2]. We go deeper into this here,
with some major simplifications, clarifications, and breakthroughs.
3. THE SYSTEMS Q(0,S,+,dot), PFA(0,S,+,dot), EFA(0,S,+,dot), SEFA(0,S,
+,dot), PA(0,S,+,dot).
Q(0,S,+,dot) is Robinson's arithmetic for L(0,S,+,dot). This has the
axioms
not Sx = 0
Sx = Sy implies x = y
x + 0 = x
x + Sy = S(x + y)
x dot 0 = 0
x dot Sy = (x dot y) + x
(therexists x)(Sx = y or y = 0).
PFA(0,S,+,dot) is polynomial arithmetic for L(0,S,+,dot), which is the
same as what is normally called bounded arithmetic. This extends Q(0,S,
+,dot) by adding the axiom scheme of induction for all bounded
formulas (< is defined by x < y iff (therexists z)(Sz + x = y)).
It is not known whether PFA(0,S,+,dot) is finitely axiomatizable.
EFA(0,S,+,dot) is exponential function arithmetic for L(0,S,+,dot). A
particularly nice axiomatization is PFA(0,S,+,dot) together with
(forall x)(therexists y)(y is a multiple of all positive integers < x).
SEFA(0,S,+,dot) is super exponential function arithmetic for L(0,S,
+,dot). A convenient axiomatization is EFA(0,S,+,dot) together with
(forall x)(there is a code for a sequence of length x where each
succeeding term is a multiple of all positive integers less than the
preceding term).
PA(0,S,+,dot) is Q(0,S,+,dot) together with the axiom scheme of
induction with respect to all formulas in L(0,S,+,dot).
Obviously Q(0,S,+,dot) is finitely axiomatizable. It is well known
that EFA(0,S,+,dot) is finitely axiomatizable. Hence SEFA(0,S,+,dot)
is also finitely axiomatizable. It is well known that PA(0,S,+,dot) is
not finitely axiomatizable.
We take the point of view that formalizations of consistency in L(0,S,
+,dot) must use EFA(0,S,+,dot) as background.
3. EXTENSIONS OF PA(0,S,+,dot) IN L(0,S,+,dot).
Let T be a theory in L(0,S,+,dot).
CONDITION A. phi is a sentence in L(0,S,+,dot) such that EFA(0,S,
+,dot) + phi proves every inequation not(s = t) that is provable in T.
Note that Condition A is trivial if T is finitely axiomatized. Just
take phi to be the conjunction of the axioms of T.
Obviously, here s,t are terms in L(0,S,+,dot) that may have many
variables.
THEOREM 3.1. Let T be a consistent r.e. theory in L(0,S,+,dot). Every
standard consistency statement for T, using any r.e. presentation of
T, obeys condition A.
THEOREM 3.2. Let T be a consistent theory in L(0,S,+,dot) extending
PA(0,S,+,dot). No theorem of T obeys condition A.
Theorem 3.2 follows from this:
THEOREM 3.3. Let T be a consistent r.e. theory in L(0,S,+,dot)
extending PA(0,S,+,dot). Let phi obey condition A. Then EFA(0,S,+,dot)
+ phi proves every standard consistency statement for every theorem of
T.
THEOREM 3.4. Let T be a consistent r.e. theory in L(0,S,+,dot)
extending PA(0,S,+,dot). There exists phi obeying condition A such
that PA(0,S,+,dot) + phi does not prove any (all) standard consistency
statement for T.
The bounded formulas of L(0,S,+,dot) are the formulas of L(0,S,+,dot)
that have all quantifiers (Qx) bounded to terms not mentioning x. The
PI formulas of L(0,S,+,dot) are the formulas obtained by putting zero
or more universal quantifiers in front of bounded formulas of L(0,S,
+,dot).
We can strengthen Condition A so that these Theorems still hold.
Specifically,
CONDITION A'. phi is a sentence in L(0,S,+,dot) such that EFA(0,S,
+,dot) + phi proves every PI formula of L(0,S,+,dot) that is provable
in T.
4. EXTENSIONS OF EFA(0,S,+,dot) in L(0,S,+,dot).
Let T be a theory in L(0,S,+,dot).
CONDITION B. phi is a PI sentence in L(0,S,+,dot) such that EFA(0,S,
+,dot) + phi proves every inequation not(s = t) that is provable in T.
THEOREM 4.1. Let T be a consistent r.e. theory in L(0,S,+,dot). Every
standard consistency statement for T, using any r.e. presentation of
T, obeys condition B.
Note that Theorem 4.1 is the same as Theorem 3.1 together with the
observation that standard consistency statements are in PI form.
THEOREM 4.2. Let T be a consistent theory in L(0,S,+,dot) extending
EFA(0,S,+,dot). No theorem of T obeys condition B.
Note that Theorem 4.2 applies far more generally than Theorem 3.2. The
cause for this is that condition B requires the sentence to be in PI
form.
We can strengthen Condition B so that these Theorems still holds.
Specifically,
CONDITION B'. phi is a PI sentence in L(0,S,+,dot) such that EFA(0,S,
+,dot) + phi proves every PI formula of L(0,S,+,dot) that is provable
in T.
5. TO BE CONTINUED.
**********************************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 343rd 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
307: Formalized Consistency Problem Solved 1/14/07 6:24PM
308: Large Large Cardinals 7/05/07 5:01AM
309: Thematic PA Incompleteness 10/22/07 10:56AM
310: Thematic PA Incompleteness 2 11/6/07 5:31AM
311: Thematic PA Incompleteness 3 11/8/07 8:35AM
312: Pi01 Incompleteness 11/13/07 3:11PM
313: Pi01 Incompleteness 12/19/07 8:00AM
314: Pi01 Incompleteness/Digraphs 12/22/07 4:12AM
315: Pi01 Incompleteness/Digraphs/#2 1/16/08 7:32AM
316: Shift Theorems 1/24/08 12:36PM
317: Polynomials and PA 1/29/08 10:29PM
318: Polynomials and PA #2 2/4/08 12:07AM
319: Pi01 Incompleteness/Digraphs/#3 2/12/08 9:21PM
320: Pi01 Incompleteness/#4 2/13/08 5:32PM
321: Pi01 Incompleteness/forward imaging 2/19/08 5:09PM
322: Pi01 Incompleteness/forward imaging 2 3/10/08 11:09PM
323: Pi01 Incompleteness/point deletion 3/17/08 2:18PM
324: Existential Comprehension 4/10/08 10:16PM
325: Single Quantifier Comprehension 4/14/08 11:07AM
326: Progress in Pi01 Incompleteness 1 10/22/08 11:58PM
327: Finite Independence/update 1/16/09 7:39PM
328: Polynomial Independence 1 1/16/09 7:39PM
329: Finite Decidability/Templating 1/16/09 7:01PM
330: Templating Pi01/Polynomial 1/17/09 7:25PM
331: Corrected Pi01/Templating 1/20/09 8:50PM
332: Preferred Model 1/22/09 7:28PM
333: Single Quantifier Comprehension/more 1/26/09 4:32PM
334: Progress in Pi01 Incompleteness 2 4/3/09 11:26PM
335: Undecidability/Euclidean geometry 4/27/09 1:12PM
336: Undecidability/Euclidean geometry/2 4/29/09 1:43PM
337: Undecidability/Euclidean geometry/3 5/3/09 6:54PM
338: Undecidability/Euclidean geometry/4 5/5/09 6:38PM
339: Undecidability/Euclidean geometry/5 5/7/09 2:25PM
340: Thematic Pi01 Incompleteness 1 5/13/09 5:56PM
341: Thematic Pi01 Incompleteness 2 5/21/09 7:25PM
342: Thematic Pi01 Incompleteness 3 5/23/09 7:48PM
Harvey Friedman
More information about the FOM
mailing list