FOM: 77:Missing axiom/atonement
Harvey Friedman
friedman at math.ohio-state.edu
Tue Jan 4 15:51:53 EST 2000
My axiomatizations in posting #75, section 1, (and also in posting #74),
were to include all of the axioms for ordered rings, and I used the well
known approach in terms of positivity. But I forgot to add the axiom that
defines the ordering in terms of positivity (pointed out to me by Randy
Dougherty):
x < y if and only if 0 < y-x.
So this should be added to the two axiomatizations in posting #75, section
1 (as well as the axiomatization in posting #74).
**********
You can derive trichotomy
x < y or y < x or x = y
with exclusive or.
And you can derive
x < y and 0 < z implies xz < yz
as follows. We have 0 < y-x and 0 < z, and so 0 < yz-xz.
And you can derive
x < y and 0 < z <= w implies xz < yw
as follows. The case z = w is from above. Assume z < w. Then xz < xw from
above. And xw < yw from above.
**********
In order to atone for this error, I include a relevant theorem and some
relevant questions. This interesting theorem is at least implicit in the
literature, and perhaps explicit. However, not all subscribers will be
familiar with it.
How do we know that we have written down a correct axiomatization of
ordered rings; i.e., commutative ordered rings with unit? Here is a
semantic condition.
THEOREM (well known). The following theories are logically equivalent.
i) the axioms of commutative ordered rings with unit.
ii) all quantifier free formulas in the language of commutative ordered
rings with unit that are universally true in the reals as a commutative
ordered ring with unit.
Proof: It suffices to show that every purely universal sentence phi true in
the reals is true in all commutative ordered rings with unit. Let phi be so
given and let M be a commutative ordered ring with unit. Let M* be the
ordered field of fractions via the usual construction. Let R be the real
closure of M*. Since all real closed fields are elementary equivalent, phi
is true in R. Since R extends M and phi is universal, we see that phi is
true in M. QED
One can apply the test in a practical, though limited, way. Consider
various true universal sentences about the reals (in the language of
ordered commutative rings with unit), and check that they can be proved in
the theory. This will likely spot an oversight.
But is there a fully practical way to tell that you haven't made an error
of omission? Of course, one obvious fully practical way to avoid an error
is to correctly remember one of the many standard axiomatizations.
**********
This general situation comes up a lot in mathematics, where there are
various important classes of structures, some of which of which are defined
via quite a lot of axioms when written down completely. How do you avoid
writing down too few axioms? By the way, the axioms are not always first
order as they are here. They might involve integers or real numbers or
complex numbers, etcetera.
So in such situations, there is always the relevant question of giving an
essentially semantic equivalent to the axiomatization - such as the well
known one in the Theorem above. It would be interesting to actually carry
this out systematically in the principal contexts in mathematics, and
explore under what general circumstances this kind of thing can be done.
GENERAL POLICY: When I make an error I will try to atone for it.
APPENDIX
corrected axiomatizations from posting #75
1. Additive identity. x+0 = x.
2. Additive commutativity. x+y = y+x.
3. Additive associativity. x+(y+z) = (x+y)+z.
4. Additive inverse. x+(-x) = 0.
5. Multiplicative identity. x*1 = x.
6. Multiplicative commutativity. x*y = y*x.
7. Multiplicative associativity. x*(y*z) = (x*y)*z.
8. Distributivity. x*(y+z) = (x*y)+(x*z).
9. Linearity. x = 0 or 0 < x or 0 < -x.
10. Additive positivity. (0 < x and 0 < y) implies 0 < x+y.
11. Multiplicative positivity. (0 < x and 0 < y) implies 0 < x*y.
12. Unit positivity. 0 < 1.
13. Irreflexivity. not(0 < 0).
14. x < y if and only if 0 < y-x.
15. Finite intervals. (therexists A)(forall x)(x epsilon A iff (y < x and x
< z)).
16. Boolean difference. (therexists C)(forall x)(x epsilon C iff (x epsilon
A and not(x epsilon B)).
17. Set addition. (therexists C)(forall x)(x epsilon C iff (therexists
y)(therexists z)(y epsilon A and z epsilon B and x = y+z)).
18. Least elements. (therexists x)(x epsilon A) implies (therexists x)(x
epsilon A and (forall y)(y epsilon A implies not(y < x))).
19. Common multiples. (therexists x)(0 < x and (forall y)((y epsilon A and
0 < y) implies (therexists z)(x = y*z))).
20. Set multiplication. (therexists C)(forall x)(x epsilon C iff (therexists
y)(therexists z)(y epsilon A and z epsilon B and x = y*z)).
Or we can use the following modification:
1. Additive identity. x+0 = x.
2. Additive commutativity. x+y = y+x.
3. Additive associativity. x+(y+z) = (x+y)+z.
4. Additive inverse. x+(-x) = 0.
5. Multiplicative identity. x*1 = x.
6. Multiplicative commutativity. x*y = y*x.
7. Multiplicative associativity. x*(y*z) = (x*y)*z.
8. Distributivity. x*(y+z) = (x*y)+(x*z).
9. Linearity. x = 0 or 0 < x or 0 < -x.
10. Additive positivity. (0 < x and 0 < y) implies 0 < x+y.
11. Multiplicative positivity. (0 < x and 0 < y) implies 0 < x*y.
12. Unit positivity. 0 < 1.
13. Irreflexivity. not(0 < 0).
14. x < y if and only if 0 < y-x.
15. Finite intervals. (therexists A)(forall x)(x epsilon A iff (y < x and x
< z)).
16. Boolean difference. (therexists C)(forall x)(x epsilon C iff (x epsilon
A and not(x epsilon B)).
17. Set addition. (therexists C)(forall x)(x epsilon C iff (therexists
y)(therexists z)(y epsilon A and z epsilon B and x = y+z)).
18. Least elements. (therexists x)(x epsilon A) implies (therexists x)(x
epsilon A and (forall y)(y epsilon A implies not(y < x))).
19. Common multiples. (therexists x)(0 < x and (forall y)((y epsilon A and
0 < y) implies (therexists z)(x = y*z))).
20. Scalar set multiplication. (therexists B)(forall y)(x epsilon B iff
(therexists z)(z epsilon A and y = x*z)).
21. Squares. (therexists A)(forall y)(y in A iff (therexists z)(0 < z and z
< x and y = z*z)).
The two groups have the same first 19 axioms, and differ after that.
In the first group, Axioms 1-20 correspond to ISigma_0(exp) = EFA. Axioms
1-20 without axiom 19 corresponds to ISigma_0. This means that the
corresponding theories have the same theorems in the language of
commutative ordered rings with unit or the language of Peano Arithmetic,
when adjusted in the standard way for the shift in context between these
two languages.
The second group of axioms 1-21 is logically equivalent to the first group
of axioms 1-20. The second group of axioms 1-21 without axiom 19 is
logically equivalent to the first group of axioms 1-21 without axiom 19.
**********
This is the 77th in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones are:
1:Foundational Completeness 11/3/97, 10:13AM, 10:26AM.
2:Axioms 11/6/97.
3:Simplicity 11/14/97 10:10AM.
4:Simplicity 11/14/97 4:25PM
5:Constructions 11/15/97 5:24PM
6:Undefinability/Nonstandard Models 11/16/97 12:04AM
7.Undefinability/Nonstandard Models 11/17/97 12:31AM
8.Schemes 11/17/97 12:30AM
9:Nonstandard Arithmetic 11/18/97 11:53AM
10:Pathology 12/8/97 12:37AM
11:F.O.M. & Math Logic 12/14/97 5:47AM
12:Finite trees/large cardinals 3/11/98 11:36AM
13:Min recursion/Provably recursive functions 3/20/98 4:45AM
14:New characterizations of the provable ordinals 4/8/98 2:09AM
14':Errata 4/8/98 9:48AM
15:Structural Independence results and provable ordinals 4/16/98
10:53PM
16:Logical Equations, etc. 4/17/98 1:25PM
16':Errata 4/28/98 10:28AM
17:Very Strong Borel statements 4/26/98 8:06PM
18:Binary Functions and Large Cardinals 4/30/98 12:03PM
19:Long Sequences 7/31/98 9:42AM
20:Proof Theoretic Degrees 8/2/98 9:37PM
21:Long Sequences/Update 10/13/98 3:18AM
22:Finite Trees/Impredicativity 10/20/98 10:13AM
23:Q-Systems and Proof Theoretic Ordinals 11/6/98 3:01AM
24:Predicatively Unfeasible Integers 11/10/98 10:44PM
25:Long Walks 11/16/98 7:05AM
26:Optimized functions/Large Cardinals 1/13/99 12:53PM
27:Finite Trees/Impredicativity:Sketches 1/13/99 12:54PM
28:Optimized Functions/Large Cardinals:more 1/27/99 4:37AM
28':Restatement 1/28/99 5:49AM
29:Large Cardinals/where are we? I 2/22/99 6:11AM
30:Large Cardinals/where are we? II 2/23/99 6:15AM
31:First Free Sets/Large Cardinals 2/27/99 1:43AM
32:Greedy Constructions/Large Cardinals 3/2/99 11:21PM
33:A Variant 3/4/99 1:52PM
34:Walks in N^k 3/7/99 1:43PM
35:Special AE Sentences 3/18/99 4:56AM
35':Restatement 3/21/99 2:20PM
36:Adjacent Ramsey Theory 3/23/99 1:00AM
37:Adjacent Ramsey Theory/more 5:45AM 3/25/99
38:Existential Properties of Numerical Functions 3/26/99 2:21PM
39:Large Cardinals/synthesis 4/7/99 11:43AM
40:Enormous Integers in Algebraic Geometry 5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees 5/25/99 5:11PM
43:More Enormous Integers/AlgGeom 5/25/99 6:00PM
44:Indiscernible Primes 5/27/99 12:53 PM
45:Result #1/Program A 7/14/99 11:07AM
46:Tamism 7/14/99 11:25AM
47:Subalgebras/Reverse Math 7/14/99 11:36AM
48:Continuous Embeddings/Reverse Mathematics 7/15/99 12:24PM
49:Ulm Theory/Reverse Mathematics 7/17/99 3:21PM
50:Enormous Integers/Number Theory 7/17/99 11:39PN
51:Enormous Integers/Plane Geometry 7/18/99 3:16PM
52:Cardinals and Cones 7/18/99 3:33PM
53:Free Sets/Reverse Math 7/19/99 2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry 8/27/99 3:01PM
57:Fixpoints/Summation/Large Cardinals 9/10/99 3:47AM
57':Restatement 9/11/99 7:06AM
58:Program A/Conjectures 9/12/99 1:03AM
59:Restricted summation:Pi-0-1 sentences 9/17/99 10:41AM
60:Program A/Results 9/17/99 1:32PM
61:Finitist proofs of conservation 9/29/99 11:52AM
62:Approximate fixed points revisited 10/11/99 1:35AM
63:Disjoint Covers/Large Cardinals 10/11/99 1:36AM
64:Finite Posets/Large Cardinals 10/11/99 1:37AM
65:Simplicity of Axioms/Conjectures 10/19/99 9:54AM
66:PA/an approach 10/21/99 8:02PM
67:Nested Min Recursion/Large Cardinals 10/25/99 8:00AM
68:Bad to Worse/Conjectures 10/28/99 10:00PM
69:Baby Real Analysis 11/1/99 6:59AM
70:Efficient Formulas and Schemes 11/1/99 1:46PM
71:Ackerman/Algebraic Geometry/1 12/10/99 1:52PM
72:New finite forms/large cardinals 12/12/99 6:11AM
73:Hilbert's program wide open? 12/20/99 8:28PM
74:Reverse arithmetic beginnings 12/22/99 8:33AM
75:Finite Reverse Mathematics 12/28/99 1:21PM
76: Finite set theories 12/28/99 1:28PM
More information about the FOM
mailing list