[FOM] 697: Refuting the Continuum Hypothesis?/8
Harvey Friedman
hmflogic at gmail.com
Wed Jul 6 18:40:23 EDT 2016
1. Some Remarks on the Consistent Truth Program.
2. Concerning Inconsistent Truth.
1. SOME REMAKS ON THE CONSISTENT TRUTH PROGRAM
Thanks to http://www.cs.nyu.edu/pipermail/fom/2016-July/019955.html
for making a correction.
I have just posted a reply to
http://www.cs.nyu.edu/pipermail/fom/2016-July/019954.html, which
should appear on the FOM before this posting, which contains yet more
remarks on the Consistent Truth Program and how it differs from the
usual matter of fact absolute truth programs.
But here I want to make an additional point. In addition to being
equivalent to the negation of $, where $ is in a very basic form of
the languages we are considering whose grammar conforms to those of so
many theorems of classical analysis and beyond, CH can also be put in
these forms:
*) (for all A containedin R)(there exists f;R into R)(phi)
**) (for all f:R into R)(there exists g:R into R)(phi)
where phi is local, like the kind of phi that we are proposing to use
in the Consistent Truth program in [1].
HOWEVER, a principal feature of the languages that we propose to use is that
a. The outermost quantifier is a universal quantifier over the rich objects.
b. The innermost quantifiers are over simple parts of these rich objects.
NOTE that *),**) conform to a) but not to b). I.e., we have an inner
existential quantifier more complicated (in *) or as complicated (in
**) as the outermost quantifier.
2. CONCERNING INCONSISTENT TRUTH
Here we want to come up with some good examples of the kind of
languages L under consideration for which CT(L) is inconsistent. The
only method we have for doing this is to come up with L which is
strong enough to express any Pi-2-1 sentence, and therefore express
"every real is constructible", as well as the very minimal stuff
needed to express $.
First, a little background about Pi-2-1 sentences. Here are three very
logic oriented languages.
1. Sentences in three sorted (PPN,PN,N,epsilon), where N is the set of
all nonnegative integers, starting with a block of universal
quantifiers of sort PPN, followed by formula with no quantifiers of
sort PPN.
2. Sentences in the language of set theory beginning with a block of
universal quantifiers over transitive sets of cardinality at most c,
followed by a formula with bounded quantifiers only.
3. In any reasonable version of third order logic over N, sentences
beginning with a block of universal third order quantifiers, followed
by a formula with no third order quantifiers.
Reductions are by recursive functions which, provably in ZC, preserve truth.
It is obvious that 1,3 reduce to 2. Also 1 obviously reduces to 3. So
we want to reduce 2 to 1.In 2, we are using the structure (W,epsilon),
where W is the set of all transitive sets of cardinality at most c.
We want to interpret (W,epsilon) appropriately in (PPN,PN,epsilon). We
say x in PPN is omega-like if and only if
i. The union of x is N.
ii. The empty set is an element of x.
iii. The elements of x form a linear ordering under inclusion with no
greatest element.
iv. Every element has an immediate successor, and the immediate
successor is obtained by adding exactly one new element.
v. Every nonempty subset of x has an inclusion minimum element.
The interpretation uses any given omega-like x in PPN as a parameter.
We fix X to be omega-like. We define n <' m if and only if some
element of A with n omits m. It follows that <' is a well ordering of
N with no limit point, a least element, and no greatest element.
We define ordered triple on N by <n,m,r> = {n,m,r,t,t+1,...,t+k}, where
i. max(n,m,r)+1 = t.
ii. k = 1,...,13 according to which of the 13 order types of n,m,r, using <'.
We now have access to ternary relations on N as sets of interpreted
ordered triples from N. Then we can easily interpret addition and
multiplication on N using quantifiers over PPN, and then a pairing
function from N to N. We have to be careful with quantifiers over PPN
since we are concerned with Pi-2-1. But these definitions are in both
Pi-2-1 and Sigma-2-1 forms.
>From the pairing function from N to N, we get finite tupling from N to
N. Then we get finite tupling from PN to PN. All definitions involved
are in both Pi-2-1 and Sigma-2-1 forms.
>From here, we have multivariate relations on PN as objects in PPN.
Well founded binary relations on PN can be handled without additional
quantification over PPN. Then we are in a position to complete the
interpretation of (W,epsilon) where Pi-2-1 goes to Pi-2-1.
There is a manuscript
[2] http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#68. Equational Representations. This is an advanced draft nearing
completion for publication. September 23, 2010. 17 pages.
EquatReps092310
that is very relevant here. We restate Theorems 5.1, 6.1, and 7.5 from that ms.
THEOREM 5.1. restated. Every Pi-2-1 sentence is provably equivalent,
over ZC, to a sentence of the form
(for all f:(PN)^2 into PN)(there exist x,y in PN)(phi)
where φ is quantifier free in f,x,y,inclusion.
THEOREM 6.1 restated. Every Pi-2-1 sentence) is provably equivalent,
over ZC, to a sentence of the form
(for all f:R^2 into R)(there exist x,y in R)(phi)
where phi is quantifier free in f,x,y,<.
THEOREM 7.5. restated. Every Pi-2-1 sentence is provably equivalent,
over ZC, to a sentence of the form
(for all f:R into R)(there exist x,y in R)(s not= t)
where s,t are terms in f,x,y,+,dot,0,1.
[2] is concerned with the dual forms, Sigma-2-1, and so the original
Theorem 7.5 has s = t. So let's consolidate this with the following.
THEOREM A. Every Pi-2-1 (Sigma-2-1) sentence is provably equivalent,
over ZC, to a sentence of the each of the first two (last two) forms.
(for all f:R into R)(there exist x,y,z in R)(s = t)
(for all f:R into R)(there exist x,y in R)(s not= t)
(there exists f:R into R)(there exist x,y in R)(s = t)
(there exists f:R into R)(there exist x,y,z in R)(s not= t)
where s,t are terms in f,x,y,+,dot,0,1.
Thus we see that CT(L) for any of the above languages is inconsistent.
However, the way that these were proved in [2] does not even remotely
give any inconsistency if we restrict these languages to any kind of
reasonable sentences. You can pick your favorite complexity measure
and cut down to the sentences of these forms that that are within the
complexity that you desire. It would seem rather unlikely that the
corresponding CT(L-) is inconsistent.
It is somewhat remarkable that in Theorem A, there is no use of Z as
we used in $. This seems to be connected to the fact that the terms
used in Theorem A are very significantly richer than those used in $
and in
[1] http://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#89. On the Principle of Consistent Truth, June 20, 2016, 13 pages,
draft. ConsTruth062016
with allowing nesting and the ring operations. With Theorem 6.1
(restated), the terms considerably more restricted, not even +1, but
the nesting and the binary f are very powerful.
With the start of the Consistent Truth Program, I now have an
incentive to dig into [2] and try to make improvements.
***********************************************
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 697th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html
600: Removing Deep Pathology 1 8/15/15 10:37PM
601: Finite Emulation Theory 1/perfect? 8/22/15 1:17AM
602: Removing Deep Pathology 2 8/23/15 6:35PM
603: Removing Deep Pathology 3 8/25/15 10:24AM
604: Finite Emulation Theory 2 8/26/15 2:54PM
605: Integer and Real Functions 8/27/15 1:50PM
606: Simple Theory of Types 8/29/15 6:30PM
607: Hindman's Theorem 8/30/15 3:58PM
608: Integer and Real Functions 2 9/1/15 6:40AM
609. Finite Continuation Theory 17 9/315 1:17PM
610: Function Continuation Theory 1 9/4/15 3:40PM
611: Function Emulation/Continuation Theory 2 9/8/15 12:58AM
612: Binary Operation Emulation and Continuation 1 9/7/15 4:35PM
613: Optimal Function Theory 1 9/13/15 11:30AM
614: Adventures in Formalization 1 9/14/15 1:43PM
615: Adventures in Formalization 2 9/14/15 1:44PM
616: Adventures in Formalization 3 9/14/15 1:45PM
617: Removing Connectives 1 9/115/15 7:47AM
618: Adventures in Formalization 4 9/15/15 3:07PM
619: Nonstandardism 1 9/17/15 9:57AM
620: Nonstandardism 2 9/18/15 2:12AM
621: Adventures in Formalization 5 9/18/15 12:54PM
622: Adventures in Formalization 6 9/29/15 3:33AM
623: Optimal Function Theory 2 9/22/15 12:02AM
624: Optimal Function Theory 3 9/22/15 11:18AM
625: Optimal Function Theory 4 9/23/15 10:16PM
626: Optimal Function Theory 5 9/2515 10:26PM
627: Optimal Function Theory 6 9/29/15 2:21AM
628: Optimal Function Theory 7 10/2/15 6:23PM
629: Boolean Algebra/Simplicity 10/3/15 9:41AM
630: Optimal Function Theory 8 10/3/15 6PM
631: Order Theoretic Optimization 1 10/1215 12:16AM
632: Rigorous Formalization of Mathematics 1 10/13/15 8:12PM
633: Constrained Function Theory 1 10/18/15 1AM
634: Fixed Point Minimization 1 10/20/15 11:47PM
635: Fixed Point Minimization 2 10/21/15 11:52PM
636: Fixed Point Minimization 3 10/22/15 5:49PM
637: Progress in Pi01 Incompleteness 1 10/25/15 8:45PM
638: Rigorous Formalization of Mathematics 2 10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2 10/27/15 10:38PM
640: Progress in Pi01 Incompleteness 3 10/30/15 2:30PM
641: Progress in Pi01 Incompleteness 4 10/31/15 8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1 11/3/15 11:57PM
644: Fixed Point Selectors 1 11/16/15 8:38AM
645: Fixed Point Minimizers #1 11/22/15 7:46PM
646: Philosophy of Incompleteness 1 Nov 24 17:19:46 EST 2015
647: General Incompleteness almost everywhere 1 11/30/15 6:52PM
648: Necessary Irrelevance 1 12/21/15 4:01AM
649: Necessary Irrelevance 2 12/21/15 8:53PM
650: Necessary Irrelevance 3 12/24/15 2:42AM
651: Pi01 Incompleteness Update 2/2/16 7:58AM
652: Pi01 Incompleteness Update/2 2/7/16 10:06PM
653: Pi01 Incompleteness/SRP,HUGE 2/8/16 3:20PM
654: Theory Inspired by Automated Proving 1 2/11/16 2:55AM
655: Pi01 Incompleteness/SRP,HUGE/2 2/12/16 11:40PM
656: Pi01 Incompleteness/SRP,HUGE/3 2/13/16 1:21PM
657: Definitional Complexity Theory 1 2/15/16 12:39AM
658: Definitional Complexity Theory 2 2/15/16 5:28AM
659: Pi01 Incompleteness/SRP,HUGE/4 2/22/16 4:26PM
660: Pi01 Incompleteness/SRP,HUGE/5 2/22/16 11:57PM
661: Pi01 Incompleteness/SRP,HUGE/6 2/24/16 1:12PM
662: Pi01 Incompleteness/SRP,HUGE/7 2/25/16 1:04AM
663: Pi01 Incompleteness/SRP,HUGE/8 2/25/16 3:59PM
664: Unsolvability in Number Theory 3/1/16 8:04AM
665: Pi01 Incompleteness/SRP,HUGE/9 3/1/16 9:07PM
666: Pi01 Incompleteness/SRP,HUGE/10 13/18/16 10:43AM
667: Pi01 Incompleteness/SRP,HUGE/11 3/24/16 9:56PM
668: Pi01 Incompleteness/SRP,HUGE/12 4/7/16 6:33PM
669: Pi01 Incompleteness/SRP,HUGE/13 4/17/16 2:51PM
670: Pi01 Incompleteness/SRP,HUGE/14 4/28/16 1:40AM
671: Pi01 Incompleteness/SRP,HUGE/15 4/30/16 12:03AM
672: Refuting the Continuum Hypothesis? 5/1/16 1:11AM
673: Pi01 Incompleteness/SRP,HUGE/16 5/1/16 11:27PM
674: Refuting the Continuum Hypothesis?/2 5/4/16 2:36AM
675: Embedded Maximality and Pi01 Incompleteness/1 5/7/16 12:45AM
676: Refuting the Continuum Hypothesis?/3 5/10/16 3:30AM
677: Embedded Maximality and Pi01 Incompleteness/2 5/17/16 7:50PM
678: Symmetric Optimality and Pi01 Incompleteness/1 5/19/16 1:22AM
679: Symmetric Maximality and Pi01 Incompleteness/1 5/23/16 9:21PM
680: Large Cardinals and Continuations/1 5/29/16 10:58PM
681: Large Cardinals and Continuations/2 6/1/16 4:01AM
682: Large Cardinals and Continuations/3 6/2/16 8:05AM
683: Large Cardinals and Continuations/4 6/2/16 11:21PM
684: Large Cardinals and Continuations/5 6/3/16 3:56AM
685: Large Cardinals and Continuations/6 6/4/16 8:39PM
686: Refuting the Continuum Hypothesis?/4 6/616 9:29PM
687: Large Cardinals and Continuations/7 6/7/16 10:28PM
688: Large Cardinals and Continuations/8 6/9/16 11::41PM
689: Large Cardinals and Continuations/9 6/11/16 2:51PM
690: Two Brief Sketches 6/13/16 1:18AM
691: Large Cardinals and Continuations/10 6/13/16 9:09PM
692: Large Cardinals and Continuations/11 6/15/16 10:22PM
693: Refuting the Continuum Hypothesis?/5 6/21/16 10:44AM
694: Large Cardinals and Continuations/12 6/29/16 11:46PM
695: Refuting the Continuum Hypothesis?/6 7/16 2:28AM
696: Refuting the Continuum Hypothesis?/7 7/ 5/16 7:41PM
Harvey Friedman
More information about the FOM
mailing list