896: (R,<,0,1,+,-,x,Z)
Harvey Friedman
hmflogic at gmail.com
Mon Sep 27 04:52:32 EDT 2021
The ordered field of real numbers (R,<,0,1,+,-,x) plays a fundamental
role in f.o.m., with its elimination of quantifiers and decision
procedures for its first order theory. This is definitely in the realm
of what is called *tameness* as opposed to *wildness*.
This would be even much more powerful if it could be carried out for
(R,<,0,1,+,-,x,Z). It is well known that this is not possible on
various counts.
First of all, this would include all arithmetic sentences, well known
to be highly non recursive, and definitely well within the realm of
the wild.
But the situation is even much worse as the following well known
result indicates.
THEOREM. The structures (R,<,0,1,+,-,x,Z) and
(POW(N),N,epsilon,0,S,+,x) are mutually interpretable without
parameters.
COROLLARY. The first order definable subsets of R over
(R,<,0,1,+,-,x,Z) with parameters are the same as the projective sets
of real numbers. The first order theory of (R,<,0,1,+,-,x,Z) is
recursively isomorphic to the first order theory of
(POW(N),N,epsilon,0,S,+,x). Let X be a finite set of reals. The first
order definable subsets of R over (R,<,0,1,+,-,x,Z) with parameters
from X are the same as the first order definable subsets of R in
(POW(N),N,epsilon,0,S,+,x) with parameters from X (under any usual
view of R as a subset POW(N)). The first order definable subsets of Z
over (R,<,0,1,+,-,x,Z) with parameters from X are the same as the
first order definable subsets of Z over (POW(N),N,epsilon,0,S,+,x)
with parameters from X (under any usual view of R as a subset of
POW(N), and integers as elements of omega).
So the natural instinct for model theorists has been to abandon
investigations into (R,<,0,1,+,-,x,Z) and go for where there is
tameness for the first order theory and first order definable sets.
Broadly speaking, here are two general programs for investigating
(R,<,0,1,+,-,x,Z).
1. Explore the boundary for natural fragments W of first order logic,
where the W-theory of (R,<,0,1,+,-,x,Z) is "manageable". Of course,
recursive and subrecursive makes sense here. However, in light of
Hilbert's 10th, it also makes sense to look for when the W theory
becomes not arithmetic, or not recursive in the trus sentences of
arithmetic, or not hyperarithmetic, or whatever. I.e., when the W
theory lies at some natural level of definability as studied in f.o.m.
2. Same as 1 but instead of investigating the W theory, we investigate
the W definable sets (in R and in higher dimensions), with any finite
number of real parameters (or perhaps a fixed number of parameters,
including no parameters). We for example look at when this goes beyond
finite unions of intervals in R.
3. In general, one sensible thing to do is to try to "factor out" the
number theory entirely. Also to look for the geometric and analytic
features.
Now in light of proofs of the Theorem above, we know that there is a
threshold of definability where (R,<,0,1,+,-,x,Z) and (V(omega +
1),epsilon) merge into one. I.e., where our investigation goes from
model theory to set theory. The most general formulation of what I am
getting at is when this shift occurs and what do things look like
before that threshold?
Of course this is exploratory and investigatory. There could be
several interesting paths to where things transform from model theory
to set theory.
So here is a series of questions along the lines of 2 above. The
results should guide 1,3.
First stay in one dimension. Look at {x in R: phi(x,y1,...,yk)} where
phi is a formula in 0,1,<,+,x,Z, and
a. phi is quantifier free.
b. phi begins with E...EA...A over Z, followed by quantifier free.
Adjust the number of E's and the number of A's allowed, including zero
or one or the other or both. .
c. phi begins with a block of quantifiers over Z, followed by
quantifier free. Adjust the number of alternating quantifiers. Perhaps
adjust the size of blocks.
d. phi begins with E...EA...A, where E's over R and A's over Z,
followed by quantifier free. Adjust the number of E's and the number
of A's.
e. phi begins with E...EA...AE...E, where the first E's over R, the
A's over R, and the second E's over Z, followed by quantifier free.
Adjust the number of E's in both blocks, and the number of A's.
f. Restrict the quantifier free parts in various natural ways.
Now go from {x in R: phi(x,y1,...,yk)} to {(x,y) in R^2:
phi(x,y,z1,...,zk)}. And carry over 1-f. And then go to 3 and more
dimensions. Of course, at some point we get a match with what is going
on in (POW(N),N,epsilon,0,S,+,x), but where is that, and what are
things like below that?
##########################################
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 896th 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-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
800: Beyond Perfectly Natural/6 4/3/18 8:37PM
801: Big Foundational Issues/1 4/4/18 12:15AM
802: Systematic f.o.m./1 4/4/18 1:06AM
803: Perfectly Natural/7 4/11/18 1:02AM
804: Beyond Perfectly Natural/8 4/12/18 11:23PM
805: Beyond Perfectly Natural/9 4/20/18 10:47PM
806: Beyond Perfectly Natural/10 4/22/18 9:06PM
807: Beyond Perfectly Natural/11 4/29/18 9:19PM
808: Big Foundational Issues/2 5/1/18 12:24AM
809: Goedel's Second Reworked/1 5/20/18 3:47PM
810: Goedel's Second Reworked/2 5/23/18 10:59AM
811: Big Foundational Issues/3 5/23/18 10:06PM
812: Goedel's Second Reworked/3 5/24/18 9:57AM
813: Beyond Perfectly Natural/12 05/29/18 6:22AM
814: Beyond Perfectly Natural/13 6/3/18 2:05PM
815: Beyond Perfectly Natural/14 6/5/18 9:41PM
816: Beyond Perfectly Natural/15 6/8/18 1:20AM
817: Beyond Perfectly Natural/16 Jun 13 01:08:40
818: Beyond Perfectly Natural/17 6/13/18 4:16PM
819: Sugared ZFC Formalization/1 6/13/18 6:42PM
820: Sugared ZFC Formalization/2 6/14/18 6:45PM
821: Beyond Perfectly Natural/18 6/17/18 1:11AM
822: Tangible Incompleteness/1 7/14/18 10:56PM
823: Tangible Incompleteness/2 7/17/18 10:54PM
824: Tangible Incompleteness/3 7/18/18 11:13PM
825: Tangible Incompleteness/4 7/20/18 12:37AM
826: Tangible Incompleteness/5 7/26/18 11:37PM
827: Tangible Incompleteness Restarted/1 9/23/19 11:19PM
828: Tangible Incompleteness Restarted/2 9/23/19 11:19PM
829: Tangible Incompleteness Restarted/3 9/23/19 11:20PM
830: Tangible Incompleteness Restarted/4 9/26/19 1:17 PM
831: Tangible Incompleteness Restarted/5 9/29/19 2:54AM
832: Tangible Incompleteness Restarted/6 10/2/19 1:15PM
833: Tangible Incompleteness Restarted/7 10/5/19 2:34PM
834: Tangible Incompleteness Restarted/8 10/10/19 5:02PM
835: Tangible Incompleteness Restarted/9 10/13/19 4:50AM
836: Tangible Incompleteness Restarted/10 10/14/19 12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20 02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory 2/8/20 2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20 12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1: 5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1 5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1 6/19/20 1132PM :
860: Unary Regressive Growth/1 8/120 9:50PM
861: Simplified Axioms for Class Theory 9/16/20 9:17PM
862: Symmetric Semigroups 2/2/21 9:11 PM
863: Structural Mapping Theory/1 2/4/21 11:36PM
864: Structural Mapping Theory/2 2/7/21 1:07AM
865: Structural Mapping Theory/3 2/10/21 11:57PM
866: Structural Mapping Theory/4 2/13/21 12:47AM
867: Structural Mapping Theory/5 2/14/21 11:27PM
868: Structural Mapping Theory/6 2/15/21 9:45PM
869: Structural Proof Theory/1 2/24/21 12:10AM
870: Structural Proof Theory/2 2/28/21 1:18AM
871: Structural Proof Theory/3 2/28/21 9:27PM
872: Structural Proof Theory/4 2/28/21 10:38PM
873: Structural Proof Theory/5 3/1/21 12:58PM
874: Structural Proof Theory/6 3/1/21 6:52PM
875: Structural Proof Theory/7 3/2/21 4:07AM
876: Structural Proof Theory/8 3/2/21 7:27AM
877: Structural Proof Theory/9 3/3/21 7:46PM
878: Structural Proof Theory/10 3/3/21 8:53PM
879: Structural Proof Theory/11 3/4/21 4:22AM
880: Tangible Updates/1 4/15/21 1:46AM
881: Some Logical Thresholds 4/29/21 11:49PM
882: Logical Strength Comparability 5/8/21 5:49PM
883: Tangible Incompleteness Lecture Plans 5/16/21 1:29:44
884: Low Strength Zoo/1 5/16/21 1:34:
885: Effective Forms 5/16/21 1:47AM
886: Concerning Natural/1 5/16/21 2:00AM
887: Updated Adventures 9/9/21 9:47AM 2021
888: New(?) kinds of questions 9/9/21 12:32PM
889: Generating r.e. sets 9/12/21 3:38PM
890: Update on Tangible Incompleteness 9/18/21 9:50AM :
891: Remarks on Reverse Mathematics/1 9/21/21 12:50AM :
892: Remarks on Reverse Mathematics/2 9/21/21 8:37AM :
893: Remarks on Reverse Mathematics/3 9/23/21 10:04PM
894: Update on Tangible Incompleteness/2 9/25/21 2:51AM
895: Provably Recursive Functions and Sigma02
Harvey Friedman
More information about the FOM
mailing list