FOM: 35':Restatement

[Harvey Friedman]

This is a self contained restatement of the 35th 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

A complete archiving of fom, message by message, is available at
http://www.math.psu.edu/simpson/fom/
Also, my series of self contained postings (only) is archived at
http://www.math.ohio-state.edu/foundations/manuscripts.html

FAVORITE SELF CONTAINED POSTINGS: 21, 25, 27, 31, 32, 34, 35'. (This
supercedes and clarifies 35.)

SPECIAL AE SENTENCES
by
Harvey M. Friedman
March 21, 1999

Here we use the class of AE sentences to provide a model theoretic
interpretation of set theory with small large cardinals. It will be
convenient to allow the empty model. Thus any sentence that begins with a
universal quantifier has an empty model.

The special AE sentences are the sentences A of first order predicate
calculus with equality, the distinguished binary relation symbol <, and
zero or more constant, relation, and function symbols, with the following
properties:

1) A is a prenex sentence starting with one or more universal quantifiers
followed by one or more existential quantifiers followed by a quantifier
free formula;
2) in every countable model (M,<) of A, < is a linear ordering of the domain;
3) Let (M,<) be a countable model of A and x be any object outside its
domain. Then there is a unique model (M',<') of A, where (M,<) is a
submodel of (M',<'), dom(M') = dom(M) union {x}, and x is the greatest
element of M' (with respect to <').

The following provide useful background information:

THEOREM 1. Let A be a special AE sentence. Then 2) and 3) hold for
arbitrary M.

THEOREM 2. Every special AE sentence has models of every well ordered type.
The set of special AE sentences is recursively enumerable.

Let (M,<) be a model of the special AE sentence A. An embedding of (M,<) is
(as usual)
an isomorphism from (M,<) onto a submodel of (M,<). The crticial point of j
is the least element of dom(M) that is
moved.

PROPOSITION 3. Every special AE sentence has a countable model with an
embdding that has a critical point.

THEOREM 4. In ACA_0, Proposition 3 is equivalent to the consistency of ZFC
+ {there exists an n-subtle cardinal}_n.