[FOM] 205:First Order Extremal Clauses

Harvey Friedman friedman at math.ohio-state.edu
Sun Jan 18 14:25:34 EST 2004


NOTE: Much of what is said here is well known, but the whole may be greater
than the sum of its parts. Also, the issue of first order maximality has
come up in certain axiomatizations of special relativistic kinematics. This
suggests the importance of a general discussion of first order extremal
clauses.

1. SOME SECOND ORDER EXAMPLES.

The fundamental importance and utility of extremal clauses has long been
recognized. 

Specifically, when defining a certain set, or a certain structure up to
isomorphism, one often writes down some conditions, and follows this by a
statement that "there is no proper subset or substructure satisfying these
conditions", or "there is no proper superset or superstructure satisfying
these conditions". 

It is clear that such extremal clauses take us out of the realm of first
order axiomatization.

For instance, in defining the nonnegative integers with 0 and successor, up
to isomorphism, we can write

1. S(x) not= 0.
2. S(x) = S(y) implies x = y.
3. No proper substructure obeys 1,2.

Of course, we know that we cannot replace 1,2,3 with a first order
axiomatization.

Also consider Hilbert's axiomatization of plane Euclidean geometry. These
are spelled out in

David Hilbert, Foundations of Geometry, Appendix II, Open Court Classics,
1971.

Original source:

David Hilbert, Uber den Satz von der Gleichheit der Basiswinkel, Proceedings
of the London Math. Soc., Vol. 35.

Hilbert uses the following primitives:

1. One sort for points.
2. One sort of lines.
3. A given point is on a given line. The "incidence relation".
4. A 3-ary relation among points of betweeness: B lies strictly between A
and B (on a line).
5. A 4-ary relation among points of equidistance (congruence): the distance
from A to B is the same as the distance from B to A.

Hilbert presents many first order axioms using these notions. He then
finishes with two non first order axioms. One is the Archimedean axiom. The
last is the Continuity Axiom, which asserts the following:

*there is no proper extension of the system of lines and points, which does
not disturb the relationships between the present lines and points, and
which satisfies the first order axioms and the Archimedean axiom.*

Hilbert shows that there is exactly one model of these axioms - the first
order axioms, the Archimedean axiom, and the maximality (continuity) axiom.

NOTE: Hilbert considers the Continuity Axiom formulated for various
fragments of "the first order axioms", and shows that some of these weaker
formulations are equivalent.

It is well known that it is far simpler to deal with elementary algebra
(real closed fields) than Euclidean geometry, and that there are some strong
equivalences. Nevertheless, we would like to keep Euclidean geometry in the
ensuing discussion.

For this reason, we give the following streamlined version of Euclidean
geometry. 

It is well known that it is enough to have just points and lines, and a
point being on a line.

A real field is a field in which -1 is not the sum of squares. A Pythagorean
field is a real field in which for every x, either x or -x has a square
root. 

A Pythagorean ordered field is an ordered field in which for every x, either
x or -x has a square root.

Every Pythagorean field can be made into a Pythagorean ordered field in
exactly one way. Every Pythagorean ordered field is a Pythagorean field
(dropping the <). 

A Pythagorean plane is a set of points and lines and incidence relation
which is built out of its "derived field", and where its "derived field" is
Pythagorean. 

It is well known that the following definition is equivalent:

A Pythagorean plane is a set of points and lines and incidence relation
which is built out of its "derived ordered field", and where its "derived
ordered field" is a Pythagorean ordered field.

It is also clear that "being a Pythagorean plane" is first order, and in
fact, finitely axiomatizable.

So Hilbert's axiomatization, in terms of Pythagorean planes, becomes

1. Pythagorean plane axioms. I.e., the derived field is Pythagorean.
2. Archimedean axiom. I.e., the derived field is Archimedean.
3. Continuity axiom, or maximality axiom. I.e., there is no proper
Archimedean Pythagorean extension of the derived field.

Alternatively, 

1. Pythagorean plane axioms. I.e., the derived ordered field is Pythagorean.
2. Archimedean axiom. I.e., the derived ordered field is Archimedean.
3. Continuity axiom, or maximality axiom. I.e., there is no proper
Archimedean Pythagorean extension of the derived ordered field.

There is only one model of 1-3, up to isomorphism, and its derived (ordered)
field is the (ordered) field of real numbers, up to isomorphism.

DIGRESSION. How "simple" can an axiomatization of Pythagorean planes be? Of
course, all known axiomatizatons are complicated enough so that, e.g.,
Hilbert and others like to use more primitives than just points, lines,
incidence. Hilbert also uses betweeness and equidistance. Even in Hilbert's
axiomatization, various auxiliary notions are created in order to keep the
horror controlled. 

We can turn this into an exact question using, e.g., our definition of
complexity in posting #204. The complexity of a finite axiomatization is the
sum of the complexities of the individual axioms.

We can first establish some benchmark by giving some axiomatizations, with
various primitives, and counting up their complexities. They will be
embarrassingly large.

Then we can pick some very small positive integers and try to prove that
there is no axiomatization of that complexity of less (under various choices
of primitives). If the number is small enough, then even I can do this.

Yet another simplicity study...

END OF DIGRESSION.

We now come to fields and real fields; i.e., algebra, without the geometry.

We can write down

1. Axioms for real fields.
2. Archimedean axiom. For all x, there exists an external positive integer n
such that x cannot be written as a square plus n copies of 1.
3. Maximality axiom. There is no proper field extension with 1 and 2.

This has a unique model up to isomorphism - the field of real numbers.

Alternatively, we can write down

1. Axioms for ordered fields.
2. Archimedean axiom. For all x, there exists an external positive integer n
such that 1+1+...+1 > x.
3. Maximality axiom. There is no proper ordered field extension with 1 and
2.

This has a unique model up to isomorphism - the ordered field of real
numbers.

2. FIRST ORDER MINIMALITY.

The first order formulation of first order minimality is straightforward.
Let T be a finitely axiomatized theory in a finite relational type in first
order predicate calculus with equality.

We take T(min) to be the axioms of T together with the set of axioms that
assert that in every definable restriction of the primitives to any subset
of the domain that forms a substructure, if all of the axioms of T hold then
the subset is the entire domain. Here the subset of the domain is given by a
first order formula with parameters in the language of T.

Let us see what T(min) is for certain classic T.

1. Language: 0,S. Axioms: S(x) not= 0, S(x) = S(y) implies x = y. We get the
theory of (N,0,S). 

2. Language: +,<. Axioms: discrete ordered group axioms. We get the theory
of (Z,+,<). 

3. Language: +,dot,<. Axioms: discrete ordered ring axioms. We get Peano
Arithmetic (for Z,<).


3. FIRST ORDER MAXIMALITY.

Here we have to be more careful in how we state first order maximality.

Let T be a finitely axiomatized theory in a finite relational type in first
order predicate calculus with equality.

We take T(max) to be the axioms of T together with the set of axioms that
assert that in every definable extension of the primitives to any definable
superset of the domain that forms a superstructure under some given
definable equivalence relation, if all of the axioms of T hold then the
superset is the domain.

What do we mean by definable superset here? We take this to mean a definable
subset (with parameters) of the union of some specified finite number of
Cartesian powers of the (old) domain, that includes the entire (old) domain.
Under a definable equivalence relation? A definable equivalence relation on
this definable superset (with parameters) that is the identity relation on
the (old) domain And a definable extension? We just mean that the primitives
have been extended to the definable superset, by formulas (with parameters).
Thus the new domain should be viewed as the definable superset modulo the
definable equivalence relation.

Let us see what T(max) is for certain classic T.

1. Language: +,dot. Axioms: field axioms. We get the theory of algebraically
closed fields. Write this as FA(max), where FA = field axioms. Write C0 for
the characteristic 0 axioms. Then FA(max) + C0 is the theory of the field of
complex numbers. 

2. Language: +,dot. Axioms: real field axioms. We get the theory of the
field of real numbers, which is the same as the theory of real closed
fields. 

3. Language: +,dot,<. Axioms: ordered field axioms. We get the theory of the
ordered field of real numbers, which is the same as the theory of ordered
real closed fields.

4. Language: points, lines, incidence. Axioms: derived "field" is a
Pythagorean field. We get complete Euclidean geometry; i.e., the derived
"field" is a real closed field. This is the theory of actual points, lines,
incidence in the actual Euclidean plane.

In 4, we need to adapt the whole discussion of T(max) to theories in many
sorted predicate calculus with equality. Or we can introduce unary predicate
symbols for points and lines, adhering to one sort. In the latter case, we
need the axiom that no line is a point (for completeness). These adaptations
are straightforward.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 205th 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-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  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
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM
194:PL Statement/clarification  11/2/03  8:10PM
195:The axiom of choice  11/3/03  1:11PM
196:Quantifier complexity in set theory  11/6/03  3:18AM
197:PL and primes 11/12/03  7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM
203:Proof(?) of Church's Thesis - Restatement 1/13/04 12:23AM
204:Finite Extrapolation 1/18/04 8:18AM

Harvey Friedman
























More information about the FOM mailing list