FOM: 122:Communicating Minds IV-revised

[Harvey Friedman]

Holmes, A recent claim of Friedman  11:41AM 1/28/02,  points out that in
section 13 of Communicating Minds IV, the system is too weak to interpret
infinity. This problem affects section 14 also, and I am not happy with the
various fixes one can make. So I have deleted sections 13 and 14 in the
revised version below, and renumbered the sections. In addition, some other
material has been revised. I thank Holmes for help in rooting out this and
other misstatements.

COMMUNICATING MINDS IV/revised
by
Harvey M. Friedman
January 31, 2002

The first two sections of this posting are based on two minds communicating
about the concept of
extensional classes. In the last two sections, we formulate the simplest
single sorted set theories that we know of that lead to ZFC and ZFC with
large cardinals.

13. I's CLASSES, II's CLASSES, COMPREHENSION, COMMUNICATION.

We use variables x1,x2,... over I's classes.

We use variables y1,y2,... over II's classes.

The atomic formulas are of the following forms:

i. u = v, where u,v are variables of either sort.
ii. u in v, where u,v are variables of either sort.

We close under atomic formulas under connectives and quantifiers in the
usual way. We call this language L6. We use the standard 2 sorted predicate
calculus with equality appropriate for L6.

6a. y1 = y2 iff (forall y3)(y3 in y1 iff y3 in y2).

6b. (therexists y1)(forall x1)(x1 in y1).

6c. (therexists x1)(forall x2)(x2 in x1 iff (x2 in x3 and phi)), where phi
is a formula of L6 in which x1 is not free.

6d. phi iff phi*, where phi is a formula of L6 whose variables are among
x1,x2,..., and phi* is the result of replacing each bound occurrence of xi
by yi.

We can derive

i) (therexists y1)(x1 = y1);
ii) (therexists y1)(forall y2)(y2 in y1 iff (therexists x1)(x1 = y2)).

THEOREM 13.1. The system 6a-6d is mutually interpretable with ZFC.

14. I's CLASSES, II's CLASSES, COMPREHENSION, COMMUNICATION, DOMINANCE.

We consider a dominance axiom scheme.

6e. (therexists y1)(phi and (forall x1)(x1 not= y1)) implies (therexists
y1)(phi and (forall x1)(x1 not= y1) and (therexists x1)(y1 in x1)), where
phi is a formula of L6 with all free variables among y1,x1,x2,..., and all
bound variables among y1,y2,... .

THEOREM 14.1. The system 6a-6e  can be proved consistent in, and hence is
interpretable in, ZFC + "there exists a nontrivial elementary embedding
j:V(kappa + 1) into V(lambda + 1). The system  6a-6e  proves the consistency
of, and hence interprets, ZFC + "there ZFC + there exists arbitrarily large
Woodin cardinals".

15. SINGLE SORTED SYSTEM CORRESPONDING TO ZFC.

Here we use variables x1,x2,..., membership, and the constant symbol W.
Call this single sorted language L7.

7a. (forall x3)(x3 in x1 iff x3 in x2) implies (x1 in x3 iff x2 in x3).

7b. x3 in W implies (therexists x1 in W)(forall x2 in W)(x2 in x1 iff (x2
in x3 and phi)), where phi
is a formula of L7 in which x1 is not free.

7c. (x1,...,xk in W and (therexists xk+1)(phi)) implies (therexists
xk+1)(phi and xk+1 in W), where phi is a formula of L7 not mentioning W, and
all free variables are among x1,...,xk+1.

THEOREM 15.1. The system 7a-7c and the system 7b-7c are mutually
interpretable with ZFC.

16. SINGLE SORTED SYSTEM CORRESPONDING TO LARGE CARDINALS.

We strengthen 7c as follows.

7d. (x1,...,xk in W and (therexists xk+1 notin W)(phi)) implies
((therexists xk+1 in W)(phi) and (therexists xk+1 notin W)(phi and
(therexists xk+2 in W)(xk+1 in xk+2))), where phi is a formula of L7 not
mentioning W, and all free variables are among x1,...,xk.

THEOREM 16.1. The system 7a,7b,7d has the properties in Theorem 14.1.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.

This is the 122nd in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones counting from #100 are:

100:Boolean Relation Theory IV corrected  3/21/01  11:29AM
101:Turing Degrees/1  4/2/01  3:32AM
102: Turing Degrees/2  4/8/01  5:20PM
103:Hilbert's Program for Consistency Proofs/1 4/11/01  11:10AM
104:Turing Degrees/3   4/12/01  3:19PM
105:Turing Degrees/4   4/26/01  7:44PM
106.Degenerative Cloning  5/4/01  10:57AM
107:Automated Proof Checking  5/25/01  4:32AM
108:Finite Boolean Relation Theory   9/18/01  12:20PM
109:Natural Nonrecursive Sets  9/26/01  4:41PM
110:Communicating Minds I  12/19/01  1:27PM
111:Communicating Minds II  12/22/01  8:28AM
112:Communicating MInds III   12/23/01  8:11PM
113:Coloring Integers  12/31/01  12:42PM
114:Borel Functions on HC  1/1/02  1:38PM
115:Aspects of Coloring Integers  1/3/02  10:02PM
116:Communicating Minds IV  1/4/02  2:02AM
117:Discrepancy Theory   1/6/02  12:53AM
118:Discrepancy Theory/2   1/20/02  1:31PM
119:Discrepancy Theory/3  1/22.02  5:27PM
120:Discrepancy Theory/4  1/26/02  1:33PM
121:Discrepancy Theory/4-revised  1/31/02  11:34AM