885: Effective Forms
Harvey Friedman
hmflogic at gmail.com
Sun May 16 01:47:47 EDT 2021
After I proved the independence of Kruskal's Theorem with no labels
from ATR, and more, 1981, I searched for Finite Forms. I came up with
the now well known one, and used it as a general method for obtaining
finite forms, or finite miniaturizations of many statements of the
shape of Kruskal's Theorem with no labels. This is old news, 1981-82,
and with the subsequent EKT (extended Kruskal's theorem), and Graph
Minor Theorem developments (with Robertson and Seymour), also with
finite forms of the same kind. This was taken up by A. Weiermann and
many others, and also led to Weiermann Threshold Phenomena in several
contexts and others following, with major interactions with analysis
and combinatorics, especially generating functions.
Nevertheless, there were some f.o.m. researchers who claimed at least
fo find these finite forms "unnatural" and also EKT "unnatural". Most
notable among those questioning the finite forms was Sol Feferman. He
had done some fine work in elucidating "predicativity" with his
ordinal Gamma_0 (I later showed that ATR_0 corresponded exactly to
Gamma_0), and definitely felt along with Weyl that impredicative
methods could not really be used to prove an interesting concrete
mathematical theorem of interest. So although KT was a threat to this
point of view, the finite forms of KT were a greater threat. By KT we
always mean here KT with no labels.
But there is another way one could look at my finite forms. Namely, go
back to the infinite form and put bounds on the trees:
GENERAL BOUNDED KT. Let T1,T2,... be an infinite sequence of finite
trees, where the i-th tree has at most f(i) vertices. Then one is inf
preserving embeddable in a later one.
SPECIFIC BOUNDED KT. Let T1,T2,... be an infinite sequence of finite
trees, where the i-th tree has at most c+i vertices. Then one is inf
preserving embeddable in a later one.
Now look at the second one. Its finite form occurs immediately to a
huge variety of mathematicians as a very familiar move. What has
happened is that in the original KT, the space of infinite sequences
of finite trees is NOT COMPACT. It is Baire space. It is very familiar
that by putting a bound on the terms, one gets a COMPACT SUBSPACE. And
once one has a compact space, a huge variety of mathematicians know
that one has basically FINITE INFORMATION, and you can get at this
finite information very easily by and uniformly and systematically by
putting EXACTLY THE BOUND that I used in my finite form.
So clearly COMPACT SUBSPACE and then the obvious finite form, is one
GENERAL METHOD for giving completely natural finite forms of certain
kinds of statements. This is the original.
But I now want to consider another kind of finitization of KT that is
less well known. And probably even more general. This is called
EFFECTIVIZATION.
RECURSIVE KT. In every recursive infinite sequence of finite trees,
some tree is inf preserving embeddable into a later one.
PRIMITIVE RECURSIVE KT. In every primitive recursive infinite sequence
of finite trees, some tree is inf preserving embeddable into a later
one.
ELEMENTARY RECURSIVE KT. In every elementary recursive infinite
sequence of finite trees, some tree is inf preserving embeddable into
a later one.
POLYNOMIAL TIME KT. In every polynomial time computable infinite
sequence of finite trees, some tree is inf preserving embeddable into
a later one.
Now there is no question but that these statements are perfectly
natural in an intellectual environment that includes looking at
immediate blatantly effective forms of infinite statements. Like
replacing "infinite blah blah blah" by "recursive infinite blah blah
blah" all over the place. These are provably equivalent, over EFA, to
2-consistency of ATR(<Theta(Omega^omega,0)), 1-consistency of
ATR(<Theta(Omega^omega,0)), 1-consistency of
ATR(<Theta(Omega^omega,0)), 1-consistency of
ATR(<Theta(Omega^omega,0)), respectively.
The same applies to EKT (KT with finitely many labels and the gap
condition). The gap condition turned out to be exactly what is needed
for the impedicative parts of the proof of the Graph Minor Theorem.
This effectivation method can also be applied elsewhere. For example,
to Paris/Harrington.
PARIS HARRINGTON. In every partition of the k element subsets of N
into finitely many cells, all of the k element subsets of some
relatively large >= r element subset of N lie in the same cell.
EFFECTIVE PARIS HARRINGTON. In every recursive (primitive recursive,
elementary recursive, polynomial time computable) partition of the k
element subsets of N into finitely many cells, all of the k element
subsets of some relatively large >= r element subset of N lie in the
same cell.
Also get the 2-consistency of ATR(<Theta(Omega^omega,0)),
1-consistency of ATR(<Theta(Omega^omega,0)), 1-consistency of
ATR(<Theta(Omega^omega,0)), 1-consistency of
ATR(<Theta(Omega^omega,0)), respectively.
So we see two PERFECTLY NATURAL finite form strategies for KT, and
they apply equally well to EKT and to Graph Minor THeorem. The
effective one applies equally well to Paris/Harrington.
##########################################
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 885th 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-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
800: Beyond Perfectly Natural/6 4/3/18 8:37PM
801: Big Foundational Issues/1 4/4/18 12:15AM
802: Systematic f.o.m./1 4/4/18 1:06AM
803: Perfectly Natural/7 4/11/18 1:02AM
804: Beyond Perfectly Natural/8 4/12/18 11:23PM
805: Beyond Perfectly Natural/9 4/20/18 10:47PM
806: Beyond Perfectly Natural/10 4/22/18 9:06PM
807: Beyond Perfectly Natural/11 4/29/18 9:19PM
808: Big Foundational Issues/2 5/1/18 12:24AM
809: Goedel's Second Reworked/1 5/20/18 3:47PM
810: Goedel's Second Reworked/2 5/23/18 10:59AM
811: Big Foundational Issues/3 5/23/18 10:06PM
812: Goedel's Second Reworked/3 5/24/18 9:57AM
813: Beyond Perfectly Natural/12 05/29/18 6:22AM
814: Beyond Perfectly Natural/13 6/3/18 2:05PM
815: Beyond Perfectly Natural/14 6/5/18 9:41PM
816: Beyond Perfectly Natural/15 6/8/18 1:20AM
817: Beyond Perfectly Natural/16 Jun 13 01:08:40
818: Beyond Perfectly Natural/17 6/13/18 4:16PM
819: Sugared ZFC Formalization/1 6/13/18 6:42PM
820: Sugared ZFC Formalization/2 6/14/18 6:45PM
821: Beyond Perfectly Natural/18 6/17/18 1:11AM
822: Tangible Incompleteness/1 7/14/18 10:56PM
823: Tangible Incompleteness/2 7/17/18 10:54PM
824: Tangible Incompleteness/3 7/18/18 11:13PM
825: Tangible Incompleteness/4 7/20/18 12:37AM
826: Tangible Incompleteness/5 7/26/18 11:37PM
827: Tangible Incompleteness Restarted/1 9/23/19 11:19PM
828: Tangible Incompleteness Restarted/2 9/23/19 11:19PM
829: Tangible Incompleteness Restarted/3 9/23/19 11:20PM
830: Tangible Incompleteness Restarted/4 9/26/19 1:17 PM
831: Tangible Incompleteness Restarted/5 9/29/19 2:54AM
832: Tangible Incompleteness Restarted/6 10/2/19 1:15PM
833: Tangible Incompleteness Restarted/7 10/5/19 2:34PM
834: Tangible Incompleteness Restarted/8 10/10/19 5:02PM
835: Tangible Incompleteness Restarted/9 10/13/19 4:50AM
836: Tangible Incompleteness Restarted/10 10/14/19 12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20 02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory 2/8/20 2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20 12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1: 5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1 5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1 6/19/20 1132PM :
860: Unary Regressive Growth/1 8/120 9:50PM
861: Simplified Axioms for Class Theory 9/16/20 9:17PM
862: Symmetric Semigroups 2/2/21 9:11 PM
863: Structural Mapping Theory/1 2/4/21 11:36PM
864: Structural Mapping Theory/2 2/7/21 1:07AM
865: Structural Mapping Theory/3 2/10/21 11:57PM
866: Structural Mapping Theory/4 2/13/21 12:47AM
867: Structural Mapping Theory/5 2/14/21 11:27PM
868: Structural Mapping Theory/6 2/15/21 9:45PM
869: Structural Proof Theory/1 2/24/21 12:10AM
870: Structural Proof Theory/2 2/28/21 1:18AM
871: Structural Proof Theory/3 2/28/21 9:27PM
872: Structural Proof Theory/4 2/28/21 10:38PM
873: Structural Proof Theory/5 3/1/21 12:58PM
874: Structural Proof Theory/6 3/1/21 6:52PM
875: Structural Proof Theory/7 3/2/21 4:07AM
876: Structural Proof Theory/8 3/2/21 7:27AM
877: Structural Proof Theory/9 3/3/21 7:46PM
878: Structural Proof Theory/10 3/3/21 8:53PM
879: Structural Proof Theory/11 3/4/21 4:22AM
880: Tangible Updates/1 4/15/21 1:46AM
881: Some Logical Thresholds 4/29/21 11:49PM
882: Logical Strength Comparability 5/8/21 5:49PM
883: Tangible Incompleteness Lecture Plans
884: Low Strength Zoo/1
Harvey Friedman
More information about the FOM
mailing list