FOM: 111:Communicating Minds II
Harvey Friedman
friedman at math.ohio-state.edu
Sat Dec 22 08:28:53 EST 2001
COMMUNICATING MINDS II
by
Harvey Friedman
December 22, 2001
This is a continuation of posting #110.
We now consider the case where mind II has more objects than mind I. This
allows us to use the ultimately strong version of comprehension for I's and
II's relations.
In section 5, we give a particularly elemental version that proves the
consistency of ZFC + "there exists a measureable cardinal". This system
uses an axiom of choice. We only use binary relations on objects.
In section 6, we go up one more type, and still use an axiom of choice.
This allows us to use classes and classes of classes.
In section 7, we use the full type structure, and still use an axiom choice.
In the next posting, we will consider the case where mind II has more
objects than mind I, and where we do not make use of any axiom of choice.
5. I's OBJECTS, II's OBJECTS, I's RELATIONS, II's RELATIONS, COMMUNICATION,
CHOICE.
We use variables x1,x2,... over I's objects.
We use variables y1,y2,... over II's objects.
We use variables R1,R2,... over the binary relations on objects according to I.
We use variables S1,S2,... over the binary relations on objects according
to II.
We use the unary function symbol CHOICE which maps Ri's into xi's.
The object terms are the variables xi, and the construct CHOICE(Ri).
The atomic formulas are of the following forms:
i. X = Y, where X,Y are relation variables.
ii. s = t, where s,t are object terms.
iii. s in X, where X is a relation variable, and s is an object term.
We close under atomic formulas under connectives and quantifiers in the
usual way. We call this language L3. We use the standard 4 sorted predicate
calculus with equality appropriate for L3.
3a. (therexists S1)(S1 = R1), (therexists y1)(x1 = y1).
3b. S1 = S2 iff (forall y1,y2)(S1(y1,y2) iff S2(y1,y2)).
3c. (therexists S1)(forall y1,y2)(S1(y1,y2) iff phi), where phi is any
formula in L3 in which S1 is not free.
3d. (therexists R1)(forall x1,x2)(R1(x1,x2) iff phi), where phi is any
formula in L3 in which S1 is not free.
3e. R1(x1,x1) implies R1(CHOICE(R1),CHOICE(R1)).
3f. phi iff phi*, where phi is a formula of L3 whose only variables are
among x1,x2,...,R1,R2,..., and phi* is the result of replacing each bound
occurrence of each Ri by Si, and each bound occurrence of each xi by yi.
3g. (therexists y1)(forall x1)(y1 notequal x1).
THEOREM 5.1. The system 3a-3g is equiconsistent with VB\P + "there exists a
nontrivial elementary embedding j:P(L(kappa)) into P(L(lambda)), where
L(lambda) is a set".
In the above, we don't commit to P(L(lambda)) being a set.
COROLLARY 5.2. The system 3a-3g 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 3a-3g proves the consistency
of, and hence interprets, ZFC + "there exists a measureable cardinal". The
results hold even if the use of CHOICE is disallowed in 3f.
Alternatively, we can drop CHOICE from the language, and replace 3e by
3e'. (therexists R1)(R1 is a well ordering of the x1's).
This alternative system is, in an appropriate sense, synonymous, and so the
results will be the same.
6. I's OBJECTS, II'S OBJECTS, I's CLASSES, II's CLASSES, I's CLASSES OF
CLASSES, II's CLASSES OF CLASSES, COMMUNICATION, CHOICE.
We use variables x1,x2,... over I's objects.
We use variables y1,y2,... over II's objects.
We use variables A1,A2,... over the classes of objects according to I.
We use variables B1,B2,... over the classes of objects according to II.
We use variables A*1,A*2,... over the classes of classes of objects
according to I.
We use variables B*1,B*2,... over the classes of classes of objects
according to II.
We use the unary function symbol CHOICE which maps Ai's into xi's.
The object terms are the variables xi, and the constructs CHOICE(Ai).
The atomic formulas are of the following forms:
i. X = Y, where X,Y are class variables.
ii. X* = Y*, where X*,Y* are class of class variables.
iii. s = t, where s,t are object terms.
iv. s in X, where X is a class variable, and s is an object term.
v. X in X*, where X is a class variable and X* is a class of class variable.
We close under atomic formulas under connectives and quantifiers in the
usual way. We call this language L4. We use the standard 6 sorted predicate
calculus with equality appropriate for L4.
WARNING: We number these axioms with a 4 because the lanugage is L4. We did
not follow this numbering convention in posting #110.
4a. (therexists B*1)(A*1 = B*1), (therexists B1)(A1 = B1), (therexists
y1)(x1 = y1).
4b. B1 = B2 iff (forall y1)(y1 in B1 iff y1 in B2), B*1 = B*2 iff (forall
B1)(B1 in B*1 iff B1 in B*2).
4c. (therexists B1)(forall y1)(y1 in B1 iff phi), where phi is any formula
in L4 in which B1 is not free, (therexists B*1)(forall B1)(B1 in B*1 iff
phi), where phi is any formula in L4 in which B*1 is not free.
4d. (therexists A1)(forall x1)(x1 in A1 iff phi), where phi is any formula
in L4 in which A1 is not free, (therexists A*1)(forall A1)(A1 in A*1 iff
phi), where phi is any formula in L4 in which A*1 is not free.
4e. phi iff phi*, where phi is a formula of L4 whose only variables are
among x1,x2,...,A1,A2,...,A*1,A*2,..., and phi* is the result of replacing
each bound occurrence of each Ai by Bi, each bound occurrence of each A*i
by B*i, and each bound occurrence of each xi by yi.
4f. (therexists y1)(forall x1)(y1 notequal x1).
4g. x1 in A1 implies CHOICE(A1) in A1.
THEOREM 6.1. The system 4a-4g is equiconsistent with VB\P + "there exists a
nontrivial elementary embedding j:P(P((L(kappa))) into P(P((L(lambda))),
where P(L(lambda)) is a set".
In the above, we don't commit to P(P(L(lambda))) being a set.
COROLLARY 6.2. The system 4a-4g can be proved consistent in, and hence is
interpretable in, ZFC + "there exists a nontrivial elementary embedding
j:V(kappa + 2) into V(lambda + 2). The system 4a-4g proves the consistency
of, and hence interprets, ZFC + "there exists a measureable limit of
measureable cardinals". The results hold even if the use of CHOICE is
disallowed in 4e.
We now use choice at one higher type. We change the language so that CHOICE
now maps A*'s to x's. We replace 4g with
4g'. A1 in A*1 implies CHOICE(A*1) in A*1.
THEOREM 6.3. The system 4a-4f,4g' is equiconsistent with VB\P + "there
exists a nontrivial elementary embedding j:V(kappa + 2) into V(lambda + 2),
where V(lambda + 1) is a well ordered set".
In the above, we don't commit to V(lambda + 2) being a set.
COROLLARY 6.4. The system 4a-4f,4g' can be proved consistent in, and hence
is interpretable in, ZFC + "there exists a nontrivial elementary embedding
j:V(kappa + 2) into V(lambda + 2)". The system 4a-4f,4g' proves the
consistency of, and hence interprets, ZFC + "there exists a nontrivial
elementary embedding j:V(kappa + 1) into V(lambda + 1)". The results hold
even if the use of CHOICE is disallowed in 4e.
7. I's TYPE THEORY, II's TYPE THEORY, COMMUNICATION, CHOICE.
We use the usual impredicative simple theory of types, with objects,
classes of objects, classes of classes of objects, etcetera. We will not
use CHOICE, and instead use the standard formalization of the axiom of
choice at each type in the theory of types. The axioms 4a-4g are extended
to type theory in the obvious way, with 4g replaced by this standard type
theoretic axiom of choice.
THEOREM 7.1. This system is mutually interpretable with ZFC + {there exists
a nontrivial elementary embedding j:V(kappa + n) into V(lambda + n)}n.
Kunen's inconsistency of Reinhardt's axiom (using choice) yields a proof in
this system that II's objects are more numerous than I's objects, and even
that II's objects are more numerous than I's classes of each type.
**********************************************
I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 111th 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
35':Restatement 3/21/99 2:20PM
36:Adjacent Ramsey Theory 3/23/99 1:00AM
37:Adjacent Ramsey Theory/more 5:45AM 3/25/99
38:Existential Properties of Numerical Functions 3/26/99 2:21PM
39:Large Cardinals/synthesis 4/7/99 11:43AM
40:Enormous Integers in Algebraic Geometry 5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees 5/25/99 5:11PM
43:More Enormous Integers/AlgGeom 5/25/99 6:00PM
44:Indiscernible Primes 5/27/99 12:53 PM
45:Result #1/Program A 7/14/99 11:07AM
46:Tamism 7/14/99 11:25AM
47:Subalgebras/Reverse Math 7/14/99 11:36AM
48:Continuous Embeddings/Reverse Mathematics 7/15/99 12:24PM
49:Ulm Theory/Reverse Mathematics 7/17/99 3:21PM
50:Enormous Integers/Number Theory 7/17/99 11:39PN
51:Enormous Integers/Plane Geometry 7/18/99 3:16PM
52:Cardinals and Cones 7/18/99 3:33PM
53:Free Sets/Reverse Math 7/19/99 2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry 8/27/99 3:01PM
57:Fixpoints/Summation/Large Cardinals 9/10/99 3:47AM
57':Restatement 9/11/99 7:06AM
58:Program A/Conjectures 9/12/99 1:03AM
59:Restricted summation:Pi-0-1 sentences 9/17/99 10:41AM
60:Program A/Results 9/17/99 1:32PM
61:Finitist proofs of conservation 9/29/99 11:52AM
62:Approximate fixed points revisited 10/11/99 1:35AM
63:Disjoint Covers/Large Cardinals 10/11/99 1:36AM
64:Finite Posets/Large Cardinals 10/11/99 1:37AM
65:Simplicity of Axioms/Conjectures 10/19/99 9:54AM
66:PA/an approach 10/21/99 8:02PM
67:Nested Min Recursion/Large Cardinals 10/25/99 8:00AM
68:Bad to Worse/Conjectures 10/28/99 10:00PM
69:Baby Real Analysis 11/1/99 6:59AM
70:Efficient Formulas and Schemes 11/1/99 1:46PM
71:Ackerman/Algebraic Geometry/1 12/10/99 1:52PM
72:New finite forms/large cardinals 12/12/99 6:11AM
73:Hilbert's program wide open? 12/20/99 8:28PM
74:Reverse arithmetic beginnings 12/22/99 8:33AM
75:Finite Reverse Mathematics 12/28/99 1:21PM
76: Finite set theories 12/28/99 1:28PM
77:Missing axiom/atonement 1/4/00 3:51PM
78:Quadratic Axioms/Literature Conjectures 1/7/00 11:51AM
79:Axioms for geometry 1/10/00 12:08PM
80.Boolean Relation Theory 3/10/00 9:41AM
81:Finite Distribution 3/13/00 1:44AM
82:Simplified Boolean Relation Theory 3/15/00 9:23AM
83:Tame Boolean Relation Theory 3/20/00 2:19AM
84:BRT/First Major Classification 3/27/00 4:04AM
85:General Framework/BRT 3/29/00 12:58AM
86:Invariant Subspace Problem/fA not= U 3/29/00 9:37AM
87:Programs in Naturalism 5/15/00 2:57AM
88:Boolean Relation Theory 6/8/00 10:40AM
89:Model Theoretic Interpretations of Set Theory 6/14/00 10:28AM
90:Two Universes 6/23/00 1:34PM
91:Counting Theorems 6/24/00 8:22PM
92:Thin Set Theorem 6/25/00 5:42AM
93:Orderings on Formulas 9/18/00 3:46AM
94:Relative Completeness 9/19/00 4:20AM
95:Boolean Relation Theory III 12/19/00 7:29PM
96:Comments on BRT 12/20/00 9:20AM
97.Classification of Set Theories 12/22/00 7:55AM
98:Model Theoretic Interpretation of Large Cardinals 3/5/01 3:08PM
99:Boolean Relation Theory IV 3/8/01 6:08PM
100:Boolean Relation Theory IV corrected 3/21/01 11:29AM
101:Turing Degrees/1 4/2/01 3:32AM
102: 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
More information about the FOM
mailing list