[FOM] 324: Existential Comprehension
Harvey Friedman
friedman at math.ohio-state.edu
Thu Apr 10 22:16:48 EDT 2008
EXISTENTIAL COMPREHENSION
by
Harvey M. Friedman
April 10, 2008
TOPIC: HOW CAN INFINITE SET THEORY BE VIEWED AS AN EXTRAPOLATION OF
FINITE SET THEORY THROUGH THE ADDITION OF THE AXIOM OF INFINITY?
Some time ago on the FOM email list, I suggested that this question
has an affirmative answer.
Here we present an affirmative answer through what we call existential
comprehension.
We take Zermelo set theory to be: extensionality, pairing, union,
separation, and the modern axiom of infinity (using x union {x}). The
primitives are epsilon and =.
Sigma_1 separation is separation for Sigma_1 formulas; i.e., formulas
in epsilon,= with existential quantifiers followed by a formula with
only bounded quantifiers.
No epsilon cycles is the scheme
not (x1 epsilon x2 epsilon ... epsilon xk epsilon x1)
where k >= 1.
V(omega) is the set of all hereditarily finite sets.
1. ECFIN(epsilon,inclusion,=).
Let ECFIN(epsilon,inclusion,=) be the set of all existential
comprehension axioms in epsilon, inclusion, =, that hold in
(V(omega),epsilon).
I.e., we are looking at axioms
{x: (therexists y1,...,yk)(phi)} exists
where phi is quantifier free in epsilon, inclusion, =, that hold in
(V(omega),epsilon). We treat inclusion here as an abbreviation, and
not as a primitive.
THEOREM 1.1. ECFIN(epsilon, inclusion,=) is logically equivalent to
extensionality, pairing, union, power set, Sigma_1 separation, no
epsilon cycles.
COROLLARY 1.2. ECFIN(epsilon, inclusion,=) + Infinity is equivalent to
the following variant of Zermelo set theory: extensionality, pairing,
union, power set, infinity, Sigma_1 separation, no epsilon cycles.
THEOREM 1.3. ECFIN(epsilon, inclusion,=) is decidable, and quite
robust. E.g., we can replace "hold" by provable in various finite set
theories, and also has combinatorial characterizations.
2. ECFIN(epsilon,inclusion,=,R).
Let ECFIN(epsilon,inclusion,=,R) be the set of all existential
comprehension axioms in epsilon, inclusion, =, and the unary schematic
relation symbol R, that hold in (V(omega),epsilon).
I.e., we are looking at axiom schemes
{x: (therexists y1,...,yk)(phi)} exists
where phi is quantifier free in epsilon, inclusion, =, R, that hold in
(V(omega),epsilon). We treat inclusion as an abbreviation, and allow R
to range over all unary relations on V(omega).
For the purpose of logical equivalence below, we treat
ECFIN(epsilon,inclusion,=,R) as a set of axiom schemes which require R
be appropriately subsituted by first order formulas in epsilon,= (or,
equivalently, in epsilon,inclusion,=).
THEOREM 2.1. ECFIN(epsilon,inclusion,=,R) is logically equivalent to
extensionality, pairing, union, power set, separation, no epsilon
cycles.
COROLLARY 2.2. ECFIN(epsilon,inclusion,=,R) + Infinity is logically
equivalent to the following variant of Zermelo set theory:
extensionality, pairing, union, power set, infinity, separation, no
epsilon cycles.
THEOREM 2.3. ECFIN(epsilon,inclusion,=,R) remains logically equivalent
if we require that we use at most 1 existential quantifier in the
formula phi.
THEOREM 2.4. ECFIN(epsilon,inclusion,=,R) is decidable, and quite
robust. E.g., we can replace all unary R by very simple R, or all
"true" by provable in various finite set theories. There are also
combinatorial characterizations.
3. ECFIN(epsilon,inclusion,=,R*).
Let ECFIN(epsilon,inclusion,=,R*) be the set of all existential
comprehension axioms in epsilon, inclusion, =, and the binary
schematic relation symbol R, with functional hypothesis, that hold in
(V(omega),epsilon).
I.e., we are looking at axiom schemes
(forall x)(therexists unique y)(R(x,y)) implies {x: (therexists
y1,...,yk)(phi)} exists
where phi is quantifier free in epsilon, inclusion, =, R*, that hold
in (V(omega),epsilon). We treat inclusion as an abbreviation, and
allow R to range over all binary relations on V(omega).
For the purpose of logical equivalence, we treat
ECFIN(epsilon,inclusion,=,R) as a set of axiom schemes which require R
be appropriately subsituted by first order formulas in epsilon,= (or,
equivalently, in epsilon,inclusion,=).
THEOREM 3.1. ECFIN(epsilon,inclusion,=,R*) is logically equivalent to
extensionality, pairing, union, power set, no epsilon cycles,
separation, replacement.
THEOREM 3.2. ECFIN(epsilon,inclusion,=,R*) + Infinity is equivalent to
ZF with no epsilon cycles replacing foundation.
THEOREM 3.3. ECFIN(epsilon,inclusion,=,R*) remains logically
equivalent if we require that we use at most 1 existential quantifier
in the formula phi.
THEOREM 3.4. ECFIN(epsilon,inclusion,=,R) is decidable, and quite
robust. E.g., we can replace all binary R by very simple R, or all
"true" by provable in various finite set theories. There are also
combinatorial characterizations.
4. ECFIN(epsilon,inclusion,=,rel), ECFIN(epsilon,inclusion,=,rel*).
ECFIN(epsilon,inclusion,=,rel) extends ECFIN(epsilon,inclusion,=,R) to
incorporate infinitely many relations of every arity.
ECFIN(epsilon,inclusion,=,rel*) extends ECFIN(epsilon,inclusion,=,R*)
to incorporate infinitely many relations of every arity with
functional hypothesis.
In the first case, we get logical equivalence with
ECFIN(epsilon,inclusion,=,R). In the second case, we get logical
equivalence with ECFIN(epsilon,inclusion,=,R*).
**********************************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 323rd 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected
from the original.
250. Extreme Cardinals/Pi01 7/31/05 8:34PM
251. Embedding Axioms 8/1/05 10:40AM
252. Pi01 Revisited 10/25/05 10:35PM
253. Pi01 Progress 10/26/05 6:32AM
254. Pi01 Progress/more 11/10/05 4:37AM
255. Controlling Pi01 11/12 5:10PM
256. NAME:finite inclusion theory 11/21/05 2:34AM
257. FIT/more 11/22/05 5:34AM
258. Pi01/Simplification/Restatement 11/27/05 2:12AM
259. Pi01 pointer 11/30/05 10:36AM
260. Pi01/simplification 12/3/05 3:11PM
261. Pi01/nicer 12/5/05 2:26AM
262. Correction/Restatement 12/9/05 10:13AM
263. Pi01/digraphs 1 1/13/06 1:11AM
264. Pi01/digraphs 2 1/27/06 11:34AM
265. Pi01/digraphs 2/more 1/28/06 2:46PM
266. Pi01/digraphs/unifying 2/4/06 5:27AM
267. Pi01/digraphs/progress 2/8/06 2:44AM
268. Finite to Infinite 1 2/22/06 9:01AM
269. Pi01,Pi00/digraphs 2/25/06 3:09AM
270. Finite to Infinite/Restatement 2/25/06 8:25PM
271. Clarification of Smith Article 3/22/06 5:58PM
272. Sigma01/optimal 3/24/06 1:45PM
273: Sigma01/optimal/size 3/28/06 12:57PM
274: Subcubic Graph Numbers 4/1/06 11:23AM
275: Kruskal Theorem/Impredicativity 4/2/06 12:16PM
276: Higman/Kruskal/impredicativity 4/4/06 6:31AM
277: Strict Predicativity 4/5/06 1:58PM
278: Ultra/Strict/Predicativity/Higman 4/8/06 1:33AM
279: Subcubic graph numbers/restated 4/8/06 3:14AN
280: Generating large caridnals/self embedding axioms 5/2/06 4:55AM
281: Linear Self Embedding Axioms 5/5/06 2:32AM
282: Adventures in Pi01 Independence 5/7/06
283: A theory of indiscernibles 5/7/06 6:42PM
284: Godel's Second 5/9/06 10:02AM
285: Godel's Second/more 5/10/06 5:55PM
286: Godel's Second/still more 5/11/06 2:05PM
287: More Pi01 adventures 5/18/06 9:19AM
288: Discrete ordered rings and large cardinals 6/1/06 11:28AM
289: Integer Thresholds in FFF 6/6/06 10:23PM
290: Independently Free Minds/Collectively Random Agents 6/12/06
11:01AM
291: Independently Free Minds/Collectively Random Agents (more) 6/13/06
5:01PM
292: Concept Calculus 1 6/17/06 5:26PM
293: Concept Calculus 2 6/20/06 6:27PM
294: Concept Calculus 3 6/25/06 5:15PM
295: Concept Calculus 4 7/3/06 2:34AM
296: Order Calculus 7/7/06 12:13PM
297: Order Calculus/restatement 7/11/06 12:16PM
298: Concept Calculus 5 7/14/06 5:40AM
299: Order Calculus/simplification 7/23/06 7:38PM
300: Exotic Prefix Theory 9/14/06 7:11AM
301: Exotic Prefix Theory (correction) 9/14/06 6:09PM
302: PA Completeness 10/29/06 2:38AM
303: PA Completeness (restatement) 10/30/06 11:53AM
304: PA Completeness/strategy 11/4/06 10:57AM
305: Proofs of Godel's Second 12/21/06 11:31AM
306: Godel's Second/more 12/23/06 7:39PM
307: Formalized Consistency Problem Solved 1/14/07 6:24PM
308: Large Large Cardinals 7/05/07 5:01AM
309: Thematic PA Incompleteness 10/22/07 10:56AM
310: Thematic PA Incompleteness 2 11/6/07 5:31AM
311: Thematic PA Incompleteness 3 11/8/07 8:35AM
312: Pi01 Incompleteness 11/13/07 3:11PM
313: Pi01 Incompleteness 12/19/07 8:00AM
314: Pi01 Incompleteness/Digraphs 12/22/07 4:12AM
315: Pi01 Incompleteness/Digraphs/#2 1/16/08 7:32AM
316: Shift Theorems 1/24/08 12:36PM
317: Polynomials and PA 1/29/08 10:29PM
318: Polynomials and PA #2 2/4/08 12:07AM
319: Pi01 Incompleteness/Digraphs/#3 2/12/08 9:21PM
320: Pi01 Incompleteness/#4 2/13/08 5:32PM
321: Pi01 Incompleteness/forward imaging 2/19/08 5:09PM
322: Pi01 Incompleteness/forward imaging 2 3/10/08 11:09PM
323: Pi01 Incompleteness/point deletion 3/17/08 2:18PM
Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/fom/attachments/20080410/c561cdaf/attachment.html
More information about the FOM
mailing list