[FOM] 220:Unexpected Pi01 statements/more

Tue Jun 29 11:47:42 EDT 2004

We view this present version as arguably more natural.

UNEXPECTED Pi01 STATEMENTS
Harvey M. Friedman
June 29, 2004

We present a new explicitly Pi01 statement provable from Mahlo cardinals of
finite order but not from ZFC. We first state two infinite statements
(Theorems 1,2 and Proposition 3).

Let R containedin Nk x Nk = N2k. We can think of R as a binary relation on
Nk, or as a subset of N2k.

We say that R is strictly dominating if and only if R(x,y) implies max(x) <
max(y).

For A containedin Nk, we write RA for the image of R on A as a binary
relation on Nk, which is given by RA = {y: (there exists x in A)(R(x,y))}.

THEOREM 1. For all k >= 1 and strictly dominating R containedin N2k, there
exist
sets A = Nk\RA. Furthermore, A is unique.

The following adds a redundant clause in the conclusion, but serves to
motivate the
Pi01 statements below.

THEOREM 2. For all k >= 1, every strictly dominating R containedin N2k has
an antichain A that is equaled to Nk\RA. Furthermore, A is unique.

We say that R containedin Nk x Nk = N2k is order invariant if and only if
for all x,y in N2k of the same order type, x in R iff y in R.

Let x,y in Nk. We say that x,y are order/power equivalent if and only if the
infinite sequences (x,1,2,4,8,...) and (y,1,2,4,8,...) are of the same
order type.

Let A,B containedin Nk. We say that A,B are order/power equivalent if and
only if
every element of A is order/power equivalent to an element of B and every
element of
B is order/power equivalent to an element of A.

QUESTION: For all k >= 1, every strictly dominating R containedin N2k has
an antichain A containedin (N\{2^(8k^2) -1})k that is WHAT?

PROPOSITION 3. For all k >= 1, every strictly dominating order invariant R
containedin N2k has an antichain A containedin (N\{2^(8k^2) -1})k that is
order/power equivalent to Nk\RA.

NOTE: Proposition 3 is a trivial consequence of Theorem 2 if we remove
2^(8k^2) -1. This quantity is not meant to be tight, but just easy to
write down. I will look into just what can be used later.

In a slight abuse of notation, we we say that R containedin [1,n]k x
[1,n]k = [1,n]2k is order invariant if and only if for all x,y in
[1,n]2k of the same order type, x in R iff y in R.

PROPOSITION 4. For all k,n >= 1, every strictly dominating order invariant R
containedin [1,n]2k has an antichain A containedin ([1,n]\{2^(8k^2) -1})k
that is order/power equivalent to [1,n]k\RA.

THEOREM 5. Propositions 3,4 are provably equivalent, over ACA, to the
consistency of MAH = ZFC + {there exists a k-Mahlo cardinal}k. In
particular, Propositions 3,4 are provable in MAH+ = ZFC + "for all k there
exists a k-Mahlo cardinal", and cannot be proved in ZFC (provided ZFC is
consistent).

We now introduce a new parameter, p.

We say that x,y in Nk are order/power/p equivalent if and only if the
infinite
sequences (x,1,2,...,p,1,2,4,8,...) and (y,1,2,...,p,1,2,4,8,...) are of
the same
order type.

Let A,B containedin Nk. We say that A,B are order/power/p equivalent if and
only if every element of A is order/power/p equivalent to an element of B
and every
element of B is order/power/p equivalent to an element of A.

PROPOSITION 6. For all k,p >= 1, every strictly dominating order invariant R
containedin N2k has an antichain A containedin (N\{2^(8pk^2) -1})k that is
order/power equivalent to Nk\RA.

NOTE: The 2^(8pk^2) -1 is not meant to be tight, but just easy to write down.
I will look into just what can be used later.

PROPOSITION 7. For all k,n,p >= 1, every strictly dominating order
invariant R
containedin [1,n]2k has an antichain A containedin ([1,n]\{2^(8pk^2) -1})k
that is order/power equivalent to [1,n]k\RA.

THEOREM 8. Propositions 6,7 for any fixed k is provable in MAH. This is
false for ZFC together with any "there exists a k-Mahlo cardinal", k fixed.
Propositions 6,7 for k = 3 is not provable in ZFC (provided ZFC is
consistent).

These results are related to BRT = Boolean relation theory, but serve a
somewhat different purpose. BRT has a particularly strong thematic
character, with potential points of contact with perhaps all areas of
mathematics. These Propositions are simply the most mathematically natural
explicitly Pi01 statements independent of ZFC that we have been able to
find - yet.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 218th 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-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms 4/22/03  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM
186:Grand Unification 1  7/2/03  10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03  4:43AM
189:Some Model theoretic Pi-0-1 statements  9/25/03  11:04AM
190:Diagrammatic BRT 10/6/03  8:36PM
191:Boolean Roots 10/7/03  11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement  11/2/03  4:42PM
194:PL Statement/clarification  11/2/03  8:10PM
195:The axiom of choice  11/3/03  1:11PM
196:Quantifier complexity in set theory  11/6/03  3:18AM
197:PL and primes 11/12/03  7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM
203:Proof(?) of Church's Thesis - Restatement 1/13/04 12:23AM
204:Finite Extrapolation 1/18/04 8:18AM
205:First Order Extremal Clauses 1/18/04 2:25PM
206:On foundations of special relativistic kinematics 1 1/21/04 5:50PM
207:On foundations of special relativistic kinematics 2  1/26/04  12:18AM
208:On foundations of special relativistic kinematics 3  1/26/04  12:19AAM
209:Faithful Representation in Set Theory with Atoms 1/31/04 7:18AM
210:Coding in Reverse Mathematics 1  2/2/04  12:47AM
211:Coding in Reverse Mathematics 2  2/4/04  10:52AM
212:On foundations of special relativistic kinematics 4  2/7/04  6:28PM
213:On foundations of special relativistic kinematics 5  2/8/04  9:33PM
214:On foundations of special relativistic kinematics 6  2/14/04 9:43AM
215:Special Relativity Corrections  2/24/04 8:13PM
216:New Pi01 statements  6/6/04  6:33PM
217:New new Pi01 statements  6/13/04  9:59PM
218:Unexpected Pi01 statements  6/13/04  9:40PM
219:Typos in Unexpected Pi01 statements  6/15/04  1:38AM