FOM: 110:Communicating MInds I
Harvey Friedman
friedman at math.ohio-state.edu
Wed Dec 19 13:27:58 EST 2001
COMMUNICATING MINDS I
by
Harvey Friedman
December 19, 2001
We now start presenting results behind Communicating Minds 1, 5:58PM,
12/17/01. In this posting, we restrict attention to the situation where
both minds have the same objects, but different binary relations on the
objects. In this approach, we obtain roughly the level of Zermelo set
theory, ZFC, and a subtle cardinal.
We are working out details for the versions that give large cardinals
incompatible with V = L and even large large cardinals. Here we use higher
types - at least one higher type. Assuming all goes well, we will report on
this much stronger stuff shortly.
1. OBJECTS, RELATIONS.
We review one of the most fundamental of all formal systems.
We have variables x1,x2,... over objects, and variables R1,R2,... over
binary relations of objects. The atomic formulas are xi = xj, Ri = Rj, and
Ri(xj,xk).
We have the usual two sorted axioms for predicate calculus with equality.
We have the axiom of extensionality
R1 = R2 iff (forall x1,x2)(R1(x1,x2) iff R2(x1,x2)).
We have the full comprehension axiom scheme
(therexists R1)(forall x1,x2)(R1(x1,x2) iff phi)
where phi is any formula in the present language in which R1 is not free.
This in and of itself has no significant logical strength since it has an
obvious model with one object and two relations.
However, there are many ways to add simple axioms that create the strength
of Z2 (second order arithmetic). For instance, we can use the following
axiom of infinity:
(therexists R1)(R1 is a strict linear ordering on its field with a least
element and no greatest element).
THEOREM 1.1. This system is mutually interpretable with Z2.
2. OBJECTS, I's RELATIONS, II's RELATIONS, ENUMERATION.
We use variables x1,x2,... over objects.
We use variables R1,R2,... over the binary relations of objects according to I.
We use variables S1,S2,... over the binary relations of objects according
to II.
We use the constant R for a natural number system. R is of the same sort as
the Ri's.
We use a unary function symbol ENUM which maps Ri's into objects.
The object terms are the variables xi, and the constructs ENUM(Ri),ENUM(R).
The atomic formulas are of the following forms:
i. X = Y, where X,Y are relation variables or R.
ii. s = t, where s,t are object terms.
iii. X(s,t), where X is a relation variable or R, and s,t are object terms.
We close under atomic formulas under connectives and quantifiers in the
usual way. We call this language L1. We use the standard 3 sorted predicate
calculus with equality appropriate for L1.
We begin with extensionality, as in section 1.
a. X = Y iff (forall x1,x2)(X(x1,x2) iff Y(x1,x2)), where X,Y are relation
variables.
For mind II, we use the full comprehension axiom scheme for L1.
b. (therexists S1)(forall x1,x2)(S1(x1,x2) iff phi), where phi is any
formula of L1 in which S1 is not free.
For mind I, we have to be careful not to allow parameters representing II's
relations, and not to allow ENUM.
c. (therexists R1)(forall x1,x2)(R(x1,x2) iff phi), where phi is any
formula of L1 in which R1,S1,S2,... are not free in phi and ENUM is not in
phi.
We now have the axiom of infinity.
d. R is a strict linear ordering on its field with a least element and
where every element has an immediate successor, such that no proper initial
segment of R has these properties.
We now have the axioms of enumeration.
e. ENUM(R1) is in the field of R.
f. ENUM(R1) = ENUM(R2) iff R1 = R2.
The effect of axioms e,f is that I's relations are enumerated by ENUM, and
this enumeration is accessible only to II in the construction of relations
of II. This represents the domination of mind II over mind I which is such
that mind II understands the process whereby mind I obtains or grasps mind
I's relations.
THEOREM 2.1. The system a-f is mutually interpretable with ZFC\P + V(omega
+ omega) exists. In particular, Zermelo set theory with the axiom of choice
is interpretable in this system.
Here ZFC\P is ZFC without the power set axiom.
3. OBJECTS, I's RELATIONS, II's RELATIONS, ENUMERATION, COMMUNICATION.
We start with the weakest axiom of communication that we consider.
g. phi iff phi*, where phi is a sentence of L1 whose only variables are
among x1,x2,...,R1,R2,..., and ENUM does not appear in phi, and phi* is the
result of replacing each occurrence of each Ri by Si.
The idea is that minds I and II agree on the truth values of all sentences
from their respective standpoints. Thus mind II can still communicate with
mind I even though mind II is more powerful than mind I.
THEOREM 3.1. The system a-g is mutually interpretable with ZC + {V(omega x
n) exists}n.
Here ZC is Zermelo set theory with the axiom of choice.
Here is an intermediate axiom of communication.
h. phi iff phi*, where phi is a formula of L1 whose only variables are
among x1,x2,...,R1,R2,..., with no free relation variables, and ENUM does
not appear in phi, and phi* is the result of replacing each occurrence of
each Ri by Si.
THEROEM 3.2. The system a-f,h is interpretable in ZFC\P + V(omega_2)
exists, and interprets ZC + V(omega_1) exists.
Here is the strongest axiom of communication that we consider.
i. phi iff phi*, where phi is a formula of L1 whose only variables are
among x1,x2,...,R1,R2,..., and ENUM does not appear in phi, and phi* is the
result of replacing each bound occurrence of each Ri by Si.
THEOREM 3.3. The system a-f,i is mutually interpretable with ZFC.
It turns out that we don't need the constant symbol R and the axioms d,e,
if we use even the weakest axiom of communication, g. To be specific, we
now assume that the constant symbol R is dropped from the language. Assume
that b,c are formulated without use of the constant symbol R.
THEOREM 3.4. The system a-c,f,g is mutually interpretable with ZFC\P +
{V(omega + n) exists}n.
THEOREM 3.5. The system a-c,f,h is interpretable in ZFC\P + V(omega_2)
exists, and interprets ZC + V(omega_1) exists.
THEOREM 3.6. The system a-c,f,i is mutually interpretable with ZFC.
4. OBJECTS, I's RELATIONS, II's RELATIONS, ENUMERATION, COMMUNICATION,
RELATIONS.
We now add arbitrary relations on the objects. The idea is that I,II both
discuss the same objects and the same arbitrary relations on objects, but
have different notions of, say, "definable" relations on objects.
We do not use the constant R, as in the last part of section 3. We add
variables T1,T2,... over arbitrary binary relations over objects.
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. X(s,t), where X is a relation variable, and s,t are object terms.
We close under atomic formulas under connectives and quantifiers in the
usual way. We call this language L2. We use the standard 4 sorted predicate
calculus with equality appropriate for L2.
We consider the following axioms.
4a. (therexists T1)(T1 = R1) and (therexists T1)(T1 = S1).
4b. T1 = T2 iff (forall x1,x2)(T1(x1,x2) iff T2(x1,x2)).
4c. (therexists S1)(forall x1,x2)(S1(x1,x2) iff phi), where phi is any
formula of L2 in which S1,T1,T2,..., are not free.
4d. (therexists R1)(forall x1,x2)(R(x1,x2) iff phi), where phi is any
formula of L2 in which R1,S1,S2,...,T1,T2,..., are not free in phi and ENUM
is not in phi.
4e. (therexists T1)(forall x1,x2)(T1(x,y) iff phi), where phi is any
formula of L2 in which T1 is not free.
4f. ENUM(R1) = ENUM(R2) iff R1 = R2.
4g. phi iff phi*, where phi is a formula of L2 whose only variables are
among x1,x2,...,R1,R2,...,T1,T2,..., whose only free variables are among
R1,R2,..., and ENUM does not appear in phi, and phi* is the result of
replacing each bound occurrence of each Ri by Si.
THEOREM 4.1. The system 4a-4g is interpretable in ZFC + "there exists a
subtle cardinal" and interprets ZFC + "there exists an indescribable
cardinal".
**********************************************
I use http://www.mathpreprints.com/math/Preprint/show/ Type Harvey Friedman
in window.
This is the 110th 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
More information about the FOM
mailing list