[FOM] 327: Finite Independence/update
Harvey Friedman
friedman at math.ohio-state.edu
Fri Jan 16 19:05:15 EST 2009
On Dec 30, 2008, at 11:50 AM, Jeff Hirst wrote:
> ...
>
> Harvey Friedman has discovered a number of finite combinatorial
> statements that
> are provably equivalent to large cardinal hypotheses over ZFC. For
> example, see
> his "Finite functions and the necessary use of large cardinals,"
> Ann. of Math.
> (2) 148 (1998) no. 3, 803-893. A very brief exposition of the
> result (without
> any attempt at proof) appears in section 3.9 of "Combinatorics and
> Graph Theory,
> Second Edition" by Harris, Hirst, and Mossinghoff. (It's section
> 3.8 in the
> first edition.)
>
> ...
I thought that it would be useful at this time to give a brief update
on the state of the art regarding finite independence.
NOTE: I did find http://www.maths.bris.ac.uk/~maaib//independence/node2.html
I don't know the author and I don't think it is up to date. Does
anybody on FOM know if this is being maintained elsewhere?
FINITE INDEPENDENCE RESULTS AROUND PEANO ARITHMETIC: ordinal theoretic.
The earliest intelligible independence from PA is of course the
consistency of Peano Arithmetic (Goedel). However, there is a great
deal of interest in other forms of intelligibility.
The earliest numerically intelligible example is the termination of
Goodstein sequences.
Goodstein, R., On the restricted ordinal theorem, Journal of Symbolic
Logic, 9 (1944), 33-41.
Goodstein proved termination. Then Kirby and Paris proved that
termination is independent of PA and has the associated growth rate
properties.
Kirby, L. and Paris, J., Accessible independence results for Peano
arithmetic, Bull. London. Math. Soc., 14 (1982), 285-93.
Kirby and Paris also introduced the Hydra games, which amounts to a
combinatorial interpretation of Goodstein's work, and which avoids the
somewhat artificial numerical constructions involved in Goodstein
sequences.
My work with Kruskal's Theorem (1981, see the next section), does
gives PA level independence for the case of binary trees and much more.
FINITE INDEPENDENCE RESULTS AROUND PEANO ARITHMETIC: ramsey theoretic.
Along different lines, via Ramsey's theorem, there is, of course,
J. Paris and L. Harrington, A Mathematical Incompleteness in Peano
Arithmetic. In Handbook for Mathematical Logic (Ed. J. Barwise).
Amsterdam, Netherlands: North-Holland, 1977.
I have made a serious effort to come up with PA level independence
results that are more and more combinatorially natural and
interesting. An early move in this direction by others is
Kanamori, A., McAloon, K. (1987). On Gödel incompleteness and finite
combinatorics. Annals of Pure and Applied Logic, 33, pp. 23-41.
But much more can be done. Some published results about cardinalities
of images of functions on sets, is contained in an early part of
Friedman, H. (1998). Finite functions and the neccessary use of large
cardinals. Ann. Math. 148, pp. 803-893.
In late 2007, we discovered a very basic independent statement
involving x1, f(x2,...,xk+1), f(x1,...,xk).
H. Friedman, Thematic PA Incopleteness 3, 11/8/07, http://www.cs.nyu.edu/pipermail/fom/2007-November/012236.html
Early in 2008, we have found a new class of independent statements
(around PA) called SHIFT THEOREMS. This directly addresses
f(x1,...,xk) <= f(x2,...,xk+1), and f(x2,...,xk+1)-f(x1,...,xk).
H. Friedman, Shift Theorems, 1/24/08, http://www.cs.nyu.edu/pipermail/fom/2008-January/012582.html
(I have a detailed proof of the results in a m.s., but I haven't
polished it up for a submission for publication. I should be able to
find time to do this by the end of 2009).
We converted the statements in Shift Theorems above to the context of
polynomials over the integers:
H. Friedman, Polynomials and PA #2, 2/4/08, http://www.cs.nyu.edu/pipermail/fom/2008-February/012635.html
NOTE!! It looks like I can now give a totally new kind of polynomial
version of my Shift Theorems - which is far simpler and far more
fundamentally important than what is in the above 2/4/08 posting. This
seems to create a new standard for finite independence result.
See my forthcoming numbered posting #328: Polynomial Independence 1.
FINITE INDEPENDENCE RESULTS UP TO AROUND Pi11 COMPREHENSION.
These finite independence results I obtained connected with (J.B.)
Kruskal's tree theorem. These results originally involved finite
sequences of finite trees. Later I found new statements concerning the
internal structure of a single sufficiently large finite tree.
The principal reference, with detailed proofs, is:
H. Friedman, Internal finite tree embeddings, Reflections on the
Foundations of Mathematics: Essays in honor of Solomon Feferman, ed.
Sieg, Sommer, Talcott, Lecture Notes in Logic, volume 15, 62-93, 2002,
ASL.
This also discusses my Extended Kruskal Theorem, and published work
with Robertson and Seymour on the Graph Minor Theorem, showing its
unprovability in Pi-1-1-CA_0. See
Friedman, H., Robertson, N., Seymour, P. (1987). The metamathematics
of the graph minor theorem. Contemporary Mathematics, vol. 65, pp.
229-261.
Various aspects of these developments have been taken up by Bovykin (http://logic.pdmi.ras.ru/~andrey/research.html
), Carlucci (http://www.cis.udel.edu/~carlucci/research.html),
Weiermann (http://wwwmath.uni-muenster.de/logik/Personen/weiermann/).
There has been work on extending the Hydra game to get independence at
this level, and a bit higher. It does appear to be too complicated as
it stands - although unifying and simplifying ideas may be possible:
W. Buchholz, An Independent Result for (Pi-1-1-CA + BI) + BI, Annals
of Pure and Applied Logic, 33 (!987), 131-155.
LENGTHS OF PROOFS AND SPECIFIC INTEGERS.
Let (for all n)(therexists m)(P(n,m)) be a Pi-0-2 statement with
independence properties. We can hope that for very small n, the
resulting Sigma-0-1 sentence
(thereexists m)(P(n*,m))
also has independence properties. But what? The most basic answer is:
length of proof.
It is already striking to say that the Sigma-0-1 sentence has a proof
in 20 pages if we use a system way beyond PA, but if we insist on
proving it in PA, then we need at least some number like
2^[1000}
symbols, where there are 1000 2's. Of course, one can ask (and get)
bigger numbers here.
Our first results of this kind were reported in
R.L. Smith, Consistency Strenghts of some Finite Forms of the
Higman and Kruskal Theorems, in: Harvey Friedman's Research on the
Foundations of Mathematics, North-Holland, 1984, 119-136.
For a discussion of this on the FOM, see:
H. Friedman, length of proofs, FOM, 9/15/98, http://cs.nyu.edu/pipermail/fom/1998-September/002153.html
H. Friedman, Clarification of Smith Article, 3/22/06, http://www.cs.nyu.edu/pipermail/fom/2006-March/010244.html
We can also say that
the least number m such that P(n*,m) is absurdly large.
We have taken this to mean
any proof in, say, PA, that a given Turing machine halts at input 0,
where its output is in fact the least number m such that P(n*,m), must
have at least 2^[1000] symbols.
And we have this sort of result in many contexts, as well.
H. Friedman, Subcubic Graph Numbers (restated), 4/8/06, http://www.cs.nyu.edu/pipermail/fom/2006-April/010362.html
H. Friedman, Integer Thresholds in FFF, 6/6/06, http://www.cs.nyu.edu/pipermail/fom/2006-June/010627.html
FINITE INDEPENDENCE FROM ZF AND HIGHER.
The published reference for this is:
Friedman, H. (1998). Finite functions and the neccessary use of large
cardinals. Ann. Math. 148, pp. 803-893.
However, we have made considerable progress on this, including the
discovery of simpler, even Pi-0-1 sentences, equivalent to the
consistency of some large cardinals. These explicitly Pi-0-1 sentences
are presented in
H. Friedman, 10/22/08, Progress in Pi01 Incompleteness 1, http://www.cs.nyu.edu/pipermail/fom/2008-October/013161.html
H. Friedman, My Forty Years On His Shoulders, November 5, 2008, to
appear in the proceedings of the Goedel Centenary meeting in Vienna,
held in April, 2006, Horizons of Truth, 69 pages. Manuscript 58, http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html
**********************************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 327th 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected
from the original.
250. Extreme Cardinals/Pi01 7/31/05 8:34PM
251. Embedding Axioms 8/1/05 10:40AM
252. Pi01 Revisited 10/25/05 10:35PM
253. Pi01 Progress 10/26/05 6:32AM
254. Pi01 Progress/more 11/10/05 4:37AM
255. Controlling Pi01 11/12 5:10PM
256. NAME:finite inclusion theory 11/21/05 2:34AM
257. FIT/more 11/22/05 5:34AM
258. Pi01/Simplification/Restatement 11/27/05 2:12AM
259. Pi01 pointer 11/30/05 10:36AM
260. Pi01/simplification 12/3/05 3:11PM
261. Pi01/nicer 12/5/05 2:26AM
262. Correction/Restatement 12/9/05 10:13AM
263. Pi01/digraphs 1 1/13/06 1:11AM
264. Pi01/digraphs 2 1/27/06 11:34AM
265. Pi01/digraphs 2/more 1/28/06 2:46PM
266. Pi01/digraphs/unifying 2/4/06 5:27AM
267. Pi01/digraphs/progress 2/8/06 2:44AM
268. Finite to Infinite 1 2/22/06 9:01AM
269. Pi01,Pi00/digraphs 2/25/06 3:09AM
270. Finite to Infinite/Restatement 2/25/06 8:25PM
271. Clarification of Smith Article 3/22/06 5:58PM
272. Sigma01/optimal 3/24/06 1:45PM
273: Sigma01/optimal/size 3/28/06 12:57PM
274: Subcubic Graph Numbers 4/1/06 11:23AM
275: Kruskal Theorem/Impredicativity 4/2/06 12:16PM
276: Higman/Kruskal/impredicativity 4/4/06 6:31AM
277: Strict Predicativity 4/5/06 1:58PM
278: Ultra/Strict/Predicativity/Higman 4/8/06 1:33AM
279: Subcubic graph numbers/restated 4/8/06 3:14AN
280: Generating large caridnals/self embedding axioms 5/2/06 4:55AM
281: Linear Self Embedding Axioms 5/5/06 2:32AM
282: Adventures in Pi01 Independence 5/7/06
283: A theory of indiscernibles 5/7/06 6:42PM
284: Godel's Second 5/9/06 10:02AM
285: Godel's Second/more 5/10/06 5:55PM
286: Godel's Second/still more 5/11/06 2:05PM
287: More Pi01 adventures 5/18/06 9:19AM
288: Discrete ordered rings and large cardinals 6/1/06 11:28AM
289: Integer Thresholds in FFF 6/6/06 10:23PM
290: Independently Free Minds/Collectively Random Agents 6/12/06
11:01AM
291: Independently Free Minds/Collectively Random Agents (more) 6/13/06
5:01PM
292: Concept Calculus 1 6/17/06 5:26PM
293: Concept Calculus 2 6/20/06 6:27PM
294: Concept Calculus 3 6/25/06 5:15PM
295: Concept Calculus 4 7/3/06 2:34AM
296: Order Calculus 7/7/06 12:13PM
297: Order Calculus/restatement 7/11/06 12:16PM
298: Concept Calculus 5 7/14/06 5:40AM
299: Order Calculus/simplification 7/23/06 7:38PM
300: Exotic Prefix Theory 9/14/06 7:11AM
301: Exotic Prefix Theory (correction) 9/14/06 6:09PM
302: PA Completeness 10/29/06 2:38AM
303: PA Completeness (restatement) 10/30/06 11:53AM
304: PA Completeness/strategy 11/4/06 10:57AM
305: Proofs of Godel's Second 12/21/06 11:31AM
306: Godel's Second/more 12/23/06 7:39PM
307: Formalized Consistency Problem Solved 1/14/07 6:24PM
308: Large Large Cardinals 7/05/07 5:01AM
309: Thematic PA Incompleteness 10/22/07 10:56AM
310: Thematic PA Incompleteness 2 11/6/07 5:31AM
311: Thematic PA Incompleteness 3 11/8/07 8:35AM
312: Pi01 Incompleteness 11/13/07 3:11PM
313: Pi01 Incompleteness 12/19/07 8:00AM
314: Pi01 Incompleteness/Digraphs 12/22/07 4:12AM
315: Pi01 Incompleteness/Digraphs/#2 1/16/08 7:32AM
316: Shift Theorems 1/24/08 12:36PM
317: Polynomials and PA 1/29/08 10:29PM
318: Polynomials and PA #2 2/4/08 12:07AM
319: Pi01 Incompleteness/Digraphs/#3 2/12/08 9:21PM
320: Pi01 Incompleteness/#4 2/13/08 5:32PM
321: Pi01 Incompleteness/forward imaging 2/19/08 5:09PM
322: Pi01 Incompleteness/forward imaging 2 3/10/08 11:09PM
323: Pi01 Incompleteness/point deletion 3/17/08 2:18PM
324: Existential Comprehension 4/10/08 10:16PM
325: Single Quantifier Comprehension 4/14/08 11:07AM
326: Progress in Pi01 Incompleteness 1 10/22/08 11:58PM
Harvey Friedman
More information about the FOM
mailing list