[FOM] 580: Goedel's Second Revisited
Harvey Friedman
hmflogic at gmail.com
Fri May 29 05:52:17 EDT 2015
I have written about Goedel's Second in these FOM postings:
http://www.cs.nyu.edu/pipermail/fom/2003-May/006496.html
http://www.cs.nyu.edu/pipermail/fom/2003-May/006504.html
http://www.cs.nyu.edu/pipermail/fom/2003-May/006518.html
http://www.cs.nyu.edu/pipermail/fom/2003-June/006694.html
http://www.cs.nyu.edu/pipermail/fom/2006-May/010524.html
http://www.cs.nyu.edu/pipermail/fom/2006-May/010525.html
http://www.cs.nyu.edu/pipermail/fom/2006-May/010529.html
http://www.cs.nyu.edu/pipermail/fom/2006-May/010532.html
http://www.cs.nyu.edu/pipermail/fom/2006-December/011194.html
http://www.cs.nyu.edu/pipermail/fom/2006-December/011223.html
http://www.cs.nyu.edu/pipermail/fom/2007-January/011282.html
http://www.cs.nyu.edu/pipermail/fom/2009-May/013753.html
http://www.cs.nyu.edu/pipermail/fom/2009-May/013778.html
http://www.cs.nyu.edu/pipermail/fom/2009-June/013828.html
http://www.cs.nyu.edu/pipermail/fom/2009-June/013837.html
http://www.cs.nyu.edu/pipermail/fom/2009-June/013843.html
http://www.cs.nyu.edu/pipermail/fom/2010-January/014290.html
I have a clearer way to present these ideas.
1. IN LANGUAGE OF ARITHMETtiC
2. IN LANGUAGE OF FINITE STRINGS
3. IN LANGUAGE OF SET THEORY
1. IN LANGUAGE OF ARITHMETIC
EFA = exponential function arithmetic, in 0,1,<,+,x,exp.
SEFA = super exponential function arithmetic, in 0,1,<,+,x,exp,superexp.
PRA = primitive recursive arithmetic.
Pi(0,1,<,...) consists of the sentences beginning with zero or more
universal quantifiers, followed by a formula with only bounded
quantifiers, in the language 0,1,<,... .
Note that PFA (bounded arithmetic), EFA, SEFA are axiomatized using
only Pi(0,1,<,+,x), Pi(0,1,<,+,x,exp), Pi(0,1,<,+,x,exp,superexp)
sentences, respectively. This means that these Pi sentences can carry
with them substantial base theories.
All systems are many sorted with equality required only on the sort
for N. The language and set of axioms can be infinite.
THEOREM 1.1. No consistent extension of EFA is interpretable in any of
its Pi(0,1,<,+,x) consequences.
THEOREM 1.2. No consistent extension of SEFA is interpretable in any
of its Pi(0,1,<,+,x,exp) consequences.
THEOREM 1.3. No consistent extension of PRA is interpretable in any of
its Pi(0,1,<,prim) consequences.
THEOREM 1.4. No consistent extension of ISigma1 is interpretable in
any of its PiSigma(0,1,<,+,x) consequences.
THEOREM 1.5. No consistent extension of PA is interpretable in any of
its arithmetic consequences.
The idea here is that any bona fide consistency statement for T is in
Pi form with few primitives, and the statement alone is sufficient to
interpret T. This can be rigorously or "rigorously" established for
any legitimate or "legitimate" consistency statement - a well known
fact that requires less finesse as we move from the settings of
Theorem 1.1 to Theorem 1.5.
Thus we have transparently avoided dealing with "legitimate
consistency statements" at the syntactic level such as the Hilbert
Bernay's adequacy conditions. This is the whole point of this series
about Goedel's Second.
2. IN LANGUAGE OF FINITE STRINGS
It can be reasonably argued that using arithmetic to formulate
consistency statements was an understandable historical accident. In
retrospect, it appears more natural to use N and finite strings from
N. In addition to primitives 0,1,<,+,x for N, we will use lth
(length), and "the value of the finite sequence at position n". For
the purpose of bounded quantifiers, we bound finite sequences by
length. Here EFA* is the same as EFA except we incorporate finite
strings in the obvious way.
THEOREM 2.1. No consistent extension of EFA* is interpretable in any
of its Pi(0,1,<,+,x,lth,val) consequences.
Since Pi(0,1,<,+,x,lth,val) is no naturally rich for the purposes of
formulating syntactic statements, we won't give multiple ascending
versions as we did in section 1.They would be straightforward
adaptations.
3. IN THE LANGUGE OF SET THEORY
An important new phenomena occurs with Goedel's Second when formulated
in the language of set theory that allows us to immediately circumvent
syntactic issues. This was presented in
http://www.cs.nyu.edu/pipermail/fom/2010-January/014290.html
Let RST (rudimentary set theory) be the following convenient set
theory in epsilon,=:
a. Extensionality.
b. Pairing.
c. Union.
d. Cartesian product.
e. Separation for bounded formulas.
It can be shown that RST is finitely axiomatizable.
THEOREM 3.1. No finitely axiomatized consistent extension of RST
proves the existence of a set structure which satisfies all its axioms
(stated by relativization).
THEOREM 3.2. If T is a consistent extension of RST, then there is no
definition gamma such that the following holds. T proves that gamma
defines a set structure M, where for each axiom A of T, T proves that
M satisfies A (stated by relativization).
THEOREM 3.3. If T is a consistent extension of RST, then there is no
property P (without parameters) such that the following holds.
i. T proves that P holds of some set structure,.
ii. For each axiom A of T, T proves that all set structures obeying P
satisfies A (stated by relativization).
THEOREM 3.4. No consistent extension of RST is interpretable in any of
its existential consequences.
Here existential consequences are provable sentences that begin with
one or more existential quantifiers, followed by a formula with
bounded quantifiers only.
************************************************************
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 580th 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-527 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-August/018092.html
528: More Perfect Pi01 8/16/14 5:19AM
529: Yet more Perfect Pi01 8/18/14 5:50AM
530: Friendlier Perfect Pi01
531: General Theory/Perfect Pi01 8/22/14 5:16PM
532: More General Theory/Perfect Pi01 8/23/14 7:32AM
533: Progress - General Theory/Perfect Pi01 8/25/14 1:17AM
534: Perfect Explicitly Pi01 8/27/14 10:40AM
535: Updated Perfect Explicitly Pi01 8/30/14 2:39PM
536: Pi01 Progress 9/1/14 11:31AM
537: Pi01/Flat Pics/Testing 9/6/14 12:49AM
538: Progress Pi01 9/6/14 11:31PM
539: Absolute Perfect Naturalness 9/7/14 9:00PM
540: SRM/Comparability 9/8/14 12:03AM
541: Master Templates 9/9/14 12:41AM
542: Templates/LC shadow 9/10/14 12:44AM
543: New Explicitly Pi01 9/10/14 11:17PM
544: Initial Maximality/HUGE 9/12/14 8:07PM
545: Set Theoretic Consistency/SRM/SRP 9/14/14 10:06PM
546: New Pi01/solving CH 9/26/14 12:05AM
547: Conservative Growth - Triples 9/29/14 11:34PM
548: New Explicitly Pi01 10/4/14 8:45PM
549: Conservative Growth - beyond triples 10/6/14 1:31AM
550: Foundational Methodology 1/Maximality 10/17/14 5:43AM
551: Foundational Methodology 2/Maximality 10/19/14 3:06AM
552: Foundational Methodology 3/Maximality 10/21/14 9:59AM
553: Foundational Methodology 4/Maximality 10/21/14 11:57AM
554: Foundational Methodology 5/Maximality 10/26/14 3:17AM
555: Foundational Methodology 6/Maximality 10/29/14 12:32PM
556: Flat Foundations 1 10/29/14 4:07PM
557: New Pi01 10/30/14 2:05PM
558: New Pi01/more 10/31/14 10:01PM
559: Foundational Methodology 7/Maximality 11/214 10:35PM
560: New Pi01/better 11/314 7:45PM
561: New Pi01/HUGE 11/5/14 3:34PM
562: Perfectly Natural Review #1 11/19/14 7:40PM
563: Perfectly Natural Review #2 11/22/14 4:56PM
564: Perfectly Natural Review #3 11/24/14 1:19AM
565: Perfectly Natural Review #4 12/25/14 6:29PM
566: Bridge/Chess/Ultrafinitism 12/25/14 10:46AM
567: Counting Equivalence Classes 1/2/15 10:38AM
568: Counting Equivalence Classes #2 1/5/15 5:06AM
569: Finite Integer Sums and Incompleteness 1/515 8:04PM
570: Philosophy of Incompleteness 1 1/8/15 2:58AM
571: Philosophy of Incompleteness 2 1/8/15 11:30AM
572: Philosophy of Incompleteness 3 1/12/15 6:29PM
573: Philosophy of Incompleteness 4 1/17/15 1:44PM
574: Characterization Theory 1 1/17/15 1:44AM
575: Finite Games and Incompleteness 1/23/15 10:42AM
576: Game Correction/Simplicity Theory 1/27/15 10:39 AM
577: New Pi01 Incompleteness 3/7/15 2:54PM
578: Provably Falsifiable Propositions 3/7/15 2:54PM
579: Impossible Counting 5/16/15 8:58PM
Harvey Friedman
More information about the FOM
mailing list