[FOM] 164:Foundations with (almost) no axioms
Harvey Friedman
friedman at math.ohio-state.edu
Tue Apr 22 17:31:55 EDT 2003
Here we initiate a set theoretic foundation for mathematics with a
special purpose. We want to use almost no axioms. The axioms for set
theory will have exactly one model up to isomorphism, and this model
will be finite.
Obviously, we need to recast mathematics in finite terms. It is
clear(?) that some mathematics will not survive this. However, I
suspect that with deep originality, some mathematics can unexpectedly
survive, at least in a form that does not compromise its essential
intellectual content.
How are we going to get, say, the statement of FLT to survive, since
it quantifies over all integers?
The idea is that we limit the universal quantifiers in FLT. Obviously
it has only the force of being true for integers below a certain
level. But this certain level is so high that one can somewhat
reasonably take the view that we don't care about integers any
higher. The essential content survives, since it seems no easier to
establish FLT for all integers below a very very very large finite
level, than to establish FLT for all integers.
Of course, it is not clear whether the current *proof* of FLT would
survive, or at least survive without major reworking. That is typical
of the interesting issues that arise out of this kind of foundations.
Analysis is where one has to be very careful from the beginning. One
has to be talking about finite precision, round off error, and the
like even before beginning any serious analysis. A very important
tool is something like the IEEE standard for arithmetic operations.
One might consider redoing all analysis, or as much analysis as
possible, as theorems about things like the IEEE standard.
Of course, if one is not superbly careful using subtle finesse, this
can easily degenerate into a horrible mess of nonrobust junk. Let's
see what happens as (if) people come to grips with this approach to
foundations.
****************
THE AXIOM SYSTEM F[16].
There will be exactly one axiom. We will use the usual predicate
calculus with equality, and the one binary relation symbol epsilon.
We assume the usual axioms and rules for logic with equality.
We are going to assume that predicate calculus has the usual
mechanisms for abbreviations that mathematicians cannot live without.
We will state the two axioms of set theory in primitive notation,
without using any abbreviation mechanisms. After that, we will
introduce abbreviations that are important for the development.
INFORMAL AXIOM 1. For all x,y, if there is no length 15 epsilon chain
ending with y, then there exists z whose elements are exactly the
elements of x together with y.
INFORMAL AXIOM 2. There is no length 16 epsilon chain.
INFORMAL AXIOM 3. If two sets have the same elements then they are equal.
AXIOM 1. (forall x1,...,x14)(not(x1 epsilon x2 and x2 epsilon x3 and
x3 epsilon x4 and x4 epsilon x5 and x5 epsilon x6 and x6 epsilon x7
and x7 epsilon x8 and x8 epsilon x9 and x9 epsilon x10 and x10
epsilon x11 and x11 epsilon x12 and x12 epsilon x13 and x13 epsilon
x14 and x14 epsilon y)) arrows (therexists z)(forall w)( epsilon z
iff w epsilon x or w = y).
AXIOM 2. not(x1 epsilon x2 and x2 epsilon x3 and x3 epsilon x4 and x4
epsilon x5 and x5 epsilon x6 and x6 epsilon x7 and x7 epsilon x8 and
x8 epsilon x9 and x9 epsilon x10 and x10 epsilon x11 and x11 epsilon
x12 and x12 epsilon x13 and x13 epsilon x14 and x14 epsilon x15 and
x15 epsilon y).
AXIOM 3. x = y iff (forall z)(z epsilon x iff z epsilon y).
We introduce the following abbreviations.
P1(x) iff x has no elements.
P2(x) iff (forall y)(y epsilon x arrows P1(y)).
P3(x) iff (forall y)(y epsilon x arrows P2(y)).
P4(x) iff (forall y)(y epsilon x arrows P3(y)).
P5(x) iff (forall y)(y epsilon x arrows P4(y)).
P6(x) iff (forall y)(y epsilon x arrows P5(y)).
P7(x) iff (forall y)(y epsilon x arrows P6(y)).
P8(x) iff (forall y)(y epsilon x arrows P7(y)).
P9(x) iff (forall y)(y epsilon x arrows P8(y)).
P10(x) iff (forall y)(y epsilon x arrows P9(y)).
P11(x) iff (forall y)(y epsilon x arrows P10(y)).
P12(x) iff (forall y)(y epsilon x arrows P11(y)).
P13(x) iff (forall y)(y epsilon x arrows P12(y)).
P14(x) iff (forall y)(y epsilon x arrows P13(y)).
P15(x) iff (forall y)(y epsilon x arrows P14(y)).
P16(x) iff (forall y)(y epsilon x arrows P15(y)).
We now restate the axioms with the help of these abbreviations.
Obviously we don't need all these abbreviations to make this
restatement. We could use one giant abbreviation. However, this
sequence of abbreviations will be very useful.
RESTATED AXIOM 1. P15(y) arrows (therexists z)(forall w)(w epsilon z
iff (w epsilon x or w = y)).
RESTATED AXIOM 2. P16(x).
RESTATED AXIOM 3. x = y iff (forall z)(z epsilon x iff z epsilon y).
Note that F[16] has exactly one model up to isomorphism, and it is
(V(16),epsilon). Here V(0) = emptyset, V(i+1) = powerset of V(i). So
V(16) is the set of all x such that P16(x).
I like the idea of this axiomatization set theory having exactly one
model, so that there are no issues (from standard viewpoints, at
least) as to what the universe of objects is.
In a fully polished presentation of F[16] one should completely
formalize the abbreviation mechanisms being allowed, and also one
should definitely put a humanly reasonably upper bound on the
appropriate sizes of all formulas allowed in proofs, and on the
appropriate sizes of any proof. Of course this includes subscripts on
the letter x for variables, and subscripts on letters used for
abbreviations. So there are only finitely many proofs in this system.
One starts off the development as follows.
1. Exhibit a proof that the empty set exists.
2. For each 1 <= i <= 15 exhibit a proof that (therexists x)(forall
y)(y epsilon x iff P15(y)).
3. In light of 2, introducing the following constants as
abbreviations: V(0), V(1), V(2), V(3), V(4), V(5), V(6), V(7), V(8),
V(9), V(10), V(11), V(12), V(13), V(14), V(15).
4. Exhibiting proofs that every nonempty subset of each of these
fifteen above has an epsilon least element. Exhibiting a proof that
every nonempty set has an epsilon least element. Exhibiting proofs
that they form a proper tower under inclusion, and a proper chain
under epsilon.
5. Introducing as abbreviations, the standard linear orderings on the
15 items in 3. Exhibiting proofs that these are indeed linear
orderings.
6. Establishing a metatheorem that tells us how to prove any instance
of comprehension over V(15) by a process that does not run into any
serious blowup over the formula used in the comprehension.
7. 6 is to be interpreted as a private matter between people. 6 is
used to help a word processor cut and paste in order to actually
exhibit proofs of instances of comprehension that come up in various
proofs that are to be exhibited.
8. Some sort of appropriate normal form theorem is developed (i.e.,
proof exhibited!!), so that one doesn't have to do any (or much)
cutting and pasting anymore to support instances of comprehension
that come up.
9. Integer arithmetic is developed based on the position of elements
of V(15) in the standard linear ordering of V(15). Overflow is
handled appropriately.
Enough. This is a good start.
*********************************************
I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 163rd in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones counting from #100 are:
100:Boolean Relation Theory IV corrected 3/21/01 11:29AM
101:Turing Degrees/1 4/2/01 3:32AM
102: Turing Degrees/2 4/8/01 5:20PM
103:Hilbert's Program for Consistency Proofs/1 4/11/01 11:10AM
104:Turing Degrees/3 4/12/01 3:19PM
105:Turing Degrees/4 4/26/01 7:44PM
106.Degenerative Cloning 5/4/01 10:57AM
107:Automated Proof Checking 5/25/01 4:32AM
108:Finite Boolean Relation Theory 9/18/01 12:20PM
109:Natural Nonrecursive Sets 9/26/01 4:41PM
110:Communicating Minds I 12/19/01 1:27PM
111:Communicating Minds II 12/22/01 8:28AM
112:Communicating MInds III 12/23/01 8:11PM
113:Coloring Integers 12/31/01 12:42PM
114:Borel Functions on HC 1/1/02 1:38PM
115:Aspects of Coloring Integers 1/3/02 10:02PM
116:Communicating Minds IV 1/4/02 2:02AM
117:Discrepancy Theory 1/6/02 12:53AM
118:Discrepancy Theory/2 1/20/02 1:31PM
119:Discrepancy Theory/3 1/22.02 5:27PM
120:Discrepancy Theory/4 1/26/02 1:33PM
121:Discrepancy Theory/4-revised 1/31/02 11:34AM
122:Communicating Minds IV-revised 1/31/02 2:48PM
123:Divisibility 2/2/02 10:57PM
124:Disjoint Unions 2/18/02 7:51AM
125:Disjoint Unions/First Classifications 3/1/02 6:19AM
126:Correction 3/9/02 2:10AM
127:Combinatorial conditions/BRT 3/11/02 3:34AM
128:Finite BRT/Collapsing Triples 3/11/02 3:34AM
129:Finite BRT/Improvements 3/20/02 12:48AM
130:Finite BRT/More 3/21/02 4:32AM
131:Finite BRT/More/Correction 3/21/02 5:39PM
132: Finite BRT/cleaner 3/25/02 12:08AM
133:BRT/polynomials/affine maps 3/25/02 12:08AM
134:BRT/summation/polynomials 3/26/02 7:26PM
135:BRT/A Delta fA/A U. fA 3/27/02 5:45PM
136:BRT/A Delta fA/A U. fA/nicer 3/28/02 1:47AM
137:BRT/A Delta fA/A U. fA/beautification 3/28/02 4:30PM
138:BRT/A Delta fA/A U. fA/more beautification 3/28/02 5:35PM
139:BRT/A Delta fA/A U. fA/better 3/28/02 10:07PM
140:BRT/A Delta fA/A U. fA/yet better 3/29/02 10:12PM
141:BRT/A Delta fA/A U. fA/grammatical improvement 3/29/02 10:43PM
142:BRT/A Delta fA/A U. fA/progress 3/30/02 8:47PM
143:BRT/A Delta fA/A U. fA/major overhaul 5/2/02 2:22PM
144: BRT/A Delta fA/A U. fA/finesse 4/3/02 4:29AM
145:BRT/A U. B U. TB/simplification/new chapter 4/4/02 4:01AM
146:Large large cardinals 4/18/02 4:30AM
147:Another Way 7:21AM 4/22/02
148:Finite forms by relativization 2:55AM 5/15/02
149:Bad Typo 1:59PM 5/15/02
150:Finite obstruction/statisics 8:55AM 6/1/02
151:Finite forms by bounding 4:35AM 6/5/02
152:sin 10:35PM 6/8/02
153:Large cardinals as general algebra 1:21PM 6/17/02
154:Orderings on theories 5:28AM 6/25/02
155:A way out 8/13/02 6:56PM
156:Societies 8/13/02 6:56PM
157:Finite Societies 8/13/02 6:56PM
158:Sentential Reflection 3/31/03 12:17AM
159.Elemental Sentential Reflection 3/31/03 12:17AM
160.Similar Subclasses 3/31/03 12:17AM
161:Restrictions and Extensions 3/31/03 12:18AM
162:Two Quantifier Blocks 3/31/03 12:28PM
163:Ouch! 4/20/03 3:08AM
More information about the FOM
mailing list