[FOM] 774: Goedel's Second: Proofs/2
Harvey Friedman
hmflogic at gmail.com
Mon Dec 18 20:36:04 EST 2017
My Finite Goedel's Theorem was introduced in
H. Friedman, On the Consistency, Completeness, and Correctness
Problems, June, 1979, Ohio State University, unpublished.
NOTE: I am planning to place a copy of many binders of unpublished
manuscripts, on my website, dated 1969-1984.
We are not at all sure that it is a good idea to adapt our new(?)
proof of Goedel's Second Theorem, from #773: Goedel's Second: Proofs/1
- to our Finite Goedel's Theorem, at least at this stage.
So here we take the usual conventional approach, with the usual kind
of proof theoretic self reference.
In this posting we keep the development at the semiformal level. Here
we adhere generally to the development in the above 1979 reference.
BUT we have now seen how to improve this result to obtain at least
some of the 1980s improvements of Pavel Pudlak on my 1979 paper.
A next major step for our rekindled research on Finite Goedel's
Theorem is to adapt the ultimate level of rigor in our treatment of
the Goedel/Bernays/Jerosolow approach in our paper
H. Friedman, My Forty Years On His Shoulders, in: Kurt Goedel and the
Foundations of Mathematics, Horizons of Truth, ed. Baaz, Papdimitriou,
Putnam, Scott, Harper, Cambridge, 2011, 399-432. Proceedings of the
Goedel Centenary meeting in Vienna, held in April 2006.
http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
section on The Second Incompleteness Theorem.
Pavel Pudlak has done considerable research on Finite Goedel's
Theorem. See, e.g.,
http://users.math.cas.cz/~pudlak/inco.pdf and references 29,30 there
http://users.math.cas.cz/~pudlak/length.pdf
In our reworking of the Finite Goedel's Theorem of 1979 below, we seem
to have come up with one of the improvements that is properly credited
to Pavel Pudlak. Basically, we had only claimed in 1979 an asymptotic
estimate of n^1/4, resulting from applying what we call the
"reflection function" TWICE, which we estimated in 1979 to be the
square. Hence the power 4, and the inverse is power 1/4. (The
"reflection" in the Assumptions below, number 5.) The argument below
applies the reflection once only, and improves this from n^1/4 to
n^1/2 if we estimate the reflection to be quadratic.
HOWEVER, we have now realized that this blowup is much much closer to
no blowup than it is to anything like quadratic, resulting in
something close to k - or more accurately, O(k). Probably there is
going to be a log factor, or maybe an iterated log factor, perhaps
depending exactly on the nature of the formal system T. (I think that
is what Pavel Pudlak saw and worked out). Such sensitivity to actual
details of actual formal systems is of course totally unnecessary in
the case of ordinary Goedel's Theorem. But with Finite Goedel's
Theorem, it is of paramount importance.
There remains substantial issues as to the exact nature of the
formalisms T that are or should be used, which affects the estimates
given or the estimates that can be expected. It was clear in our 1979
manuscript that we are particularly interested in developing Finite
Goedel's Theorem specifically for specific finite formal systems that
correspond closely to actual mathematical practice - and not so much
in the direction of proof complexity theory. The status along these
lines, particularly with hard numbers (as we tried in 1979) is rather
unclear, and we regard it as important future research.
We have asked Pavel Pudlak to give a friendly nontechnical account of
his work on Finite Goedel's Theorem for the FOM and how it relates to
our comments above and development below.
ASSUMPTIONS.
1. T is a system in the first order predicate calculus, and uses a
vocabulary V(T) of finitely many letters.
2. The size of proofs and other items is measured by the number of
letters in V(T) that appear.
3. k-consistency asserts that there is no k-proof of any A & not(A).
4. T is k-consistent.
5. Proofs in T obtained by "reflecting" on (arbitrary, unstructured)
n-proofs in T have an at most hn symbols, where h depends on T. In
particular, if T n-proves A then T hn-proves (T n-proves A).
It is convenient to use f for the inverse of h. So if T fn-proves A
then T n-proves (T fn-proves A). We fix k to be sufficiently large
integer relative to the above data, T,f, and assume that k is given by
a definite description in T of negligible size relative to k. So the
approach is asymptotic. (We are deeply interested in much more
delicate non asymptotic approaches involving very realistic finite
formal systems for mathematical practice, but do not venture into this
complex subtle territory here).
We want to give a lower bound on proofs in T that T is k-consistent.
In the argument below, some of the proofs in T are of negligible size,
meaning that their sizes are a polynomial function of T and the size
of the term representing k. This is so small compared to k that it can
be safely ignored. We argue asymptotically, ignoring the negligible,
including tiny constant multiples.
LEMMA 1. There is a sentence A of negligible size and a proof in T of
negligible size of (A if and only if (T does not fk-prove A)).
Proof: This is by the standard proof theoretic self reference
argument. There is no "reflecting" as in 5 above. QED
LEMMA 2. There is a proof in T of negligible size of (if T is
k-consistent then A).
Proof: We argue in T. Suppose T is k-consistent and T fk-proves A. Then
1) T k-proves (T fk-proves A).
So far, this proof we are giving in T is of negligible size. Also by
Lemma 1, since T fk-proves A, we see that T fk-proves (T does not
fk-prove A).
2) T fk-proves (T does not fk-prove A).
since T fk-proves A. Hence by 1), 2),
3) T is k-inconsistent.
We have a contradiction, since we are assuming that T is k-consistent. Thus
4) T + T is k-consistent proves (T does not fk- prove A). Furthermore
this proof is of negligible size.
Now paste the negligible size proof in T of (A if and only if (T does
not fk-prove A)) provided by Lemma 1, into the proof provided by 4).
To obtain the result. QED
LEMMA 3. T does not fk-proves A.
Proof: Assume
5) T fk-proves A.
By Lemma 1, T fk-proves (T does not fk-prove A). Also by "reflection",
T k-proves (T fk-proves A). Hence T is k-inconsistent, contrary to the
hypotheses on T. QED
6) T fk-proves (T does not fk-prove A)
by taking the proof given by Lemma 1 and pasting the fk-proof of A
that we are assuming in 5).
7) T k-proves (T fk-proves A)
by "reflection" in the sense of condition 5 above on T, applied to 5).
By 6),7), we see that T is k-inconsistent, contrary to the hypotheses
on T. QED
ThEOREM 4. T does not fk-prove that T is k-consistent.
Proof: Suppose T fk-proves that T is k-consistent. By Lemma 2, T
fk-proves A. This contradicts Lemma 3. QED
What can we say about the reflection function h? In my 1979
manuscript, I took it for granted that one should take it to be
squaring.
However upon reflection (pun!) it appears that something much closer
to hn = n than hn = n^2 is appropriate, probably hn = n times a
logarithmic type of factor.
E.g., we can take an induction approach to this. Choose a function h
ambitiously close to the identity, and see what happens when we try to
prove by induction on n that "for any n-proof in T of any sentence phi
of T, there is an hn-proof in T of (T n-proves phi). For the induction
step from n to n+1, we need to treat the last step in the proof quite
carefully. We suspect that Pavel Pudlak has gone into this in detail.
Perhaps there are even lower bounds for this situation?
************************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 774th 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-699 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
708: Second Incompleteness/3 9/11/16 10:33PM
709: Large Cardinals and Continuations/19 9/13/16 4:17AM
710: Large Cardinals and Continuations/20 9/14/16 1:27AM
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
708: Second Incompleteness/3 9/11/16 10:33PM
709: Large Cardinals and Continuations/19 9/13/16 4:17AM
710: Large Cardinals and Continuations/20 9/14/16 1:27AM
711: Large Cardinals and Continuations/21 9/18/16 10:42AM
712: PA Incompleteness/1 9/23/16 1:20AM
713: Foundations of Geometry/1 9/24/16 2:09PM
714: Foundations of Geometry/2 9/25/16 10:26PM
715: Foundations of Geometry/3 9/27/16 1:08AM
716: Foundations of Geometry/4 9/27/16 10:25PM
717: Foundations of Geometry/5 9/30/16 12:16AM
718: Foundations of Geometry/6 101/16 12:19PM
719: Large Cardinals and Emulations/22
720: Foundations of Geometry/7 10/2/16 1:59PM
721: Large Cardinals and Emulations//23 10/4/16 2:35AM
722: Large Cardinals and Emulations/24 10/616 1:59AM
723: Philosophical Geometry/8 10/816 1:47AM
724: Philosophical Geometry/9 10/10/16 9:36AM
725: Philosophical Geometry/10 10/14/16 10:16PM
726: Philosophical Geometry/11 Oct 17 16:04:26 EDT 2016
727: Large Cardinals and Emulations/25 10/20/16 1:37PM
728: Philosophical Geometry/12 10/24/16 3:35PM
729: Consistency of Mathematics/1 10/25/16 1:25PM
730: Consistency of Mathematics/2 11/17/16 9:50PM
731: Large Cardinals and Emulations/26 11/21/16 5:40PM
732: Large Cardinals and Emulations/27 11/28/16 1:31AM
733: Large Cardinals and Emulations/28 12/6/16 1AM
734: Large Cardinals and Emulations/29 12/8/16 2:53PM
735: Philosophical Geometry/13 12/19/16 4:24PM
736: Philosophical Geometry/14 12/20/16 12:43PM
737: Philosophical Geometry/15 12/22/16 3:24PM
738: Philosophical Geometry/16 12/27/16 6:54PM
739: Philosophical Geometry/17 1/2/17 11:50PM
740: Philosophy of Incompleteness/2 1/7/16 8:33AM
741: Philosophy of Incompleteness/3 1/7/16 1:18PM
742: Philosophy of Incompleteness/4 1/8/16 3:45AM
743: Philosophy of Incompleteness/5 1/9/16 2:32PM
744: Philosophy of Incompleteness/6 1/10/16 1/10/16 12:15AM
745: Philosophy of Incompleteness/7 1/11/16 12:40AM
746: Philosophy of Incompleteness/8 1/12/17 3:54PM
747: PA Incompleteness/2 2/3/17 12:07PM
748: Large Cardinals and Emulations/30 2/15/17 2:19AM
749: Large Cardinals and Emulations/31 2/15/17 2:19AM
750: Large Cardinals and Emulations/32 2/15/17 2:20AM
751: Large Cardinals and Emulations/33 2/17/17 12:52AM
752: Emulation Theory for Pure Math/1 3/14/17 12:57AM
753: Emulation Theory for Math Logic 3/10/17 2:17AM
754: Large Cardinals and Emulations/34 3/12/17 12:34AM
755: Large Cardinals and Emulations/35 3/12/17 12:33AM
756: Large Cardinals and Emulations/36 3/24/17 8:03AM
757: Large Cardinals and Emulations/37 3/27/17 2:39AM
758: Large Cardinals and Emulations/38 4/10/17 1:11AM
759: Large Cardinals and Emulations/39 4/10/17 1:11AM
760: Large Cardinals and Emulations/40 4/13/17 11:53PM
761: Large Cardinals and Emulations/41 4/15/17 4:54PM
762: Baby Emulation Theory/Expositional 4/17/17 1:23AM
763: Large Cardinals and Emulations/42 5/817 2:18AM
764: Large Cardinals and Emulations/43 5/11/17 12:26AM
765: Large Cardinals and Emulations/44 5/14/17 6:03PM
766: Large Cardinals and Emulations/45 7/2/17 1:22PM
767: Impossible Counting 1 9/2/17 8:28AM
768: Theory Completions 9/4/17 9:13PM
769: Complexity of Integers 1 9/7/17 12:30AM
770: Algorithmic Unsolvability 1 10/13/17 1:55PM
771: Algorithmic Unsolvability 2 10/18/17 10/15/17 10:14PM
772: Algorithmic Unsolvability 3 Oct 19 02:41:32 EDT 2017
773: Goedel's Second: Proofs/1
Harvey Friedman
Harvey Friedman
More information about the FOM
mailing list