[FOM] 195:The axiom of choice

Mon Nov 3 13:11:30 EST 2003

SUBSCRIBERS: Is there a reference for this equivalent of the AxC? Every
(symmetric, reflexive) binary relation has a maximal chain. I sketch the
argument below, but would appreciate a reference.

###############################

The purpose of this posting is twofold.

1. To correct an error in a calculation of the number of quantifiers needed
to state the axiom of choice that appears in print in two papers. We are
grateful to Aki Kanamori for pointing out this error to us.

2. To render the errors moot, by showing that the axiom of choice can be
stated with 6 quantifiers in primitive notation.

The two papers in question are

[1] D. Gogol, Sentences with three quantifiers are decidable in set theory,
Fund. Math., CII (1979), p. 3.

[2] H. Friedman, Primitive independence results, Journal of Mathematical
Logic, Vol. 3, No. 2, May 2003, p. 82.

In [2], we corrected a typographical error in the incorrect formalization of
the axiom of choice in [1]. However, we also repeated the error in question
by rewriting the axiom of choice in primitive notation in the incorrect form

for every set of pairwise disjoint sets, there is a set which meets each in
exactly one element.

We both neglected to use the correct form, which is

for every set of nonempty pairwise disjoint sets, there is a set which meets
each in exactly one element.

[1] gives a count of 8 quantifiers for the quantifiers used to formalize the
axiom of choice in primitive notation, whereas [2] gives a count of 7
quantifiers on the basis of the same incorrect formalization. When the
correction is made, the count rises to 8.

We now indicate how to formalize the axiom of choice over ZF in the
primitive notation of epsilon,= using 6 quantifiers.

The overall strategy is to begin with the familiar statement

*) every reflexive symmetric binary relation has a maximal chain.

The notion of R chain that we could use is a set A such that for all x,y in
A, R(x,y). Maximality is with respect to inclusion.

This principle is well known to imply the axiom of choice over ZF. E.g., let
B be a set of pairwise disjoint nonempty sets. Let X be the family of all
subsets of the union of B that meet every element of B in at most one
element. Let R be the reflexive symmetric binary relation

R(x,y) if and only if x,y in X and x containedin y or y containedin x.

The union of any R maximal chain an element of X that meets every element of
B.

In order to efficiently formalize *) in primitive notation, we need a
representation of symmetric binary relations avoiding the use of ordered
pairs. Note that every set E defines a symmetric binary relation E' given by

E'(x,y) if and only if (therexists z in E)(x,y in z).

Furthermore, every reflexive symmetric binary relation can be so defined.

Let phi(x,E) assert that x is a chain in E', which is AAE.

Let psi(x,E) assert that x is a maximal chain in E', which can be put in the
form 

phi(x,E) and (forall y notin x)(therexists z in x)(not E'(y,z)).

This is 

AAE and AEA.
A(AE and EA).
AA(E and EA).
AAEA.

The final form is 

(forall E)(therexists x)(psi(x,E))

which is AEAAEA, or 6 quantifiers.

The main result of [2] is the presentation of a 5 quantifier sentence that
is independent of ZFC (equivalent over ZFC to the existence of a subtle
cardinal. This raises the following question:

Is the axiom of choice equivalent, over ZF, to a 5 quantifier sentence in
epsilon,=? Or even a 4 quantifier sentence?

It follows from [3] that 3 quantifiers does not suffice.

[3] H. Friedman, Three-quantifier sentences, Fund. Math. 177 (2003),
213-240.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 194th 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