859: Incompleteness by Effectivization/1

[Harvey Friedman]

In Finite Increasing Reducers/1,2 the independent statement headlined
wasn't done quite right, and besides there is a much better way to get
such an independence result. See section 4 below. IN FACT, we have
discovered a new general theme. I have known some special cases of
this over the years, but it is only NOW that I see the general theme
clearly, and some interesting new applications of it.

GENERAL THEME: EFFECTIVIZATION. Suppose we have a Pi11 independence
result. Then weakening the statement where the outermost universal
second order quantifier is restricted to EFFECTIVE functions (sets) is
a good candidate for an arithmetic independence result of roughly the
same strength. Generally, restricting to recursive gives
2-consistency, whereas restricting to primitive recursive or
elementary recursive gives the usual 1-consistency with the expected
growth rate, provably recursive, development.

CAUTION: In each special case, there may or may not be a better way of
finitizaing that is special to that particular statement. This is
clearest in 5 and 6 and 7. With 5 the best finitiazation is obviously
the usual Paris Harrington theorem. With 6, the best follows its
intended use in term rewriting. In 1-4 that has to be the introduction
of variables and quantifiers and some sort of estimate (even lifting
is an estimate in section 2). In 7, there are finitiazations involving
gaps and also termination of a specific interesting recursive
algorithm. Nevertheless, our Effectivization Method shows that we can
get strong Pi02 sentences by defining other well ordered subsets of
the rationals even before we find any associated gap or termination
statement. In fact, this has already occurred with section 4 below,
but not in anything like the specific generation process represented
by Fusible Numbers.

Let's apply EFFECTIVIZATION TO THESE Pi11 statements.

1. Kruskal's theorem.
2. Adjacent Lifting Theorem.
3. Graph Minor Theorem.
4. Increasing Dominator Theorem.
5. Infinite Paris Harrington Theorem.
6. Lexicographic Path Ordering Theorem
7. Fusible Well Ordering Theorem

1. KRUSKAL'S THEOREM

KT. In every infinite sequence of finite trees one is inf preserving
embedded in a later one.

EFFECTIVE KT. In every effective infinite sequence of finite trees one
is inf preserving embedded in a later one.

We can take effective to mean recursive, primitive recursive, or
elementary recursive (there are other possibilities).

KT is equivalent to "theta_Omega^omega(0) is well ordered, over RCA_0.
Recursive KT is equivalent to "theta_Omega^omega(0) is recursively
well ordered, over EFA, which is roughly equivalent to the
2-consistency of arithmetic transfinite induction on
"theta_Omega^omega(0)".
Primitive recursive, elementary recursive KT is equivalent to
"theta_Omega^omega(0) is primitive recursively, elementary
recursively, well ordered, over EFA", which is equivalent to the
1-consistency of arithmetic transfinite induction on
"theta_Omega^omega(0)".

Going from presentations of the primitive recursive or elementary
recursive function to the break point has the appropriate growth rates
and provably recursive properties.

In any case, we have gone far beyond Feferman's Predicativity. The
formal system corresponding to KT is Pi-1-2-TI_0 according to Rathjen
and Weierman.

I presented Effective KT at the Vienna meeting on Goedel in 2006.

2. ADJACENT LIFTING THEOREM

ALT. For all f:N^k into N^r there exists n_1 < ... < n_k+1 such that
f(n_1,...,n_k) <= f(n_2,...,n_k+1).

Here <= is <= coordinatewise.

ALT was introduced in

H. Friedman, Adjacent Ramsey Theory. Draft. Key proofs are given.
August 29, 2010, 17 pages. #65 at Downloadable Manuscripts page
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

under the name "adjacent Ramsey theorem". But the Ramseyness is not
apparent in the statement. It is far more rudimentary than Ramsey's
theorem, and so deserves a name all of its own.

ALT is provably equivalent to "epsilon_0 is well ordered' and a
standard kind of finite form in Pi02 form was given that does need
that the finite functions are limited. Limited means max(f(x)) <=
max(x).

Many of the results in the above manuscript were published, along with
additional insights, in the joint paper

Independence of Ramsey theorem variants using epsilon_0
Harvey Friedman† and Florian Pelupessy,
http://157.193.53.8/~pelupessy/ARPH.pdf, February 8, 2013
https://www.ams.org/journals/proc/2016-144-02/S0002-9939-2015-12759-1/
 June 26, 2015

EFFECTIVE ALT. For all effective f:N^k into N^r there exists n_1 < ...
< n_k+1 such that f(n_1,...,n_k) <= f(n_2,...,n_k+1).

ALT is equivalent to "epsilon_0 is well ordered" over RCA_0.
Recursive ALT is equivalent to "PA is 2-consistent" over EFA.
Primitive recursive, elementary recursive ALT is equivalent to "PA is
1-consistent" over EFA.
Going from presentations of the primitive recursive or elementary
recursive function to the break point has the appropriate growth rates
and provably recursive properties.

In my preprint and in the joint paper, see

FINITIZED ALT. For all k,r there exists t such that the following
holds. For all limited f:{0,...,t}^k into {0,...,t} there exists n_1 <
... < n_k+1 such that f(n_1,...,n_k) <= f(n_2,...,n_k+1).

Here limited is important, and means max f(x) <= max(x). But if go
this Effectiviation route, no need for "limited".

3. GRAPH MINOR THEOREM

GMT. In any infinite sequence of finite graphs, one is minor included
in a later one.

GMT is due to Robertson and Seymour. See
https://en.wikipedia.org/wiki/Robertson–Seymour_theorem

EFFECTIVE GMT. In any effective infinite sequence of finite graphs,
one is minor included in a later one.

Interesting upper bounds on the logical strength of GMT are lacking.
For finite graphs of finite tree width, there is an exact match with
Pi-1-1-CA_0 and the proof theoretic ordinal "theta_Omega_omega(0)".
For full GMT, the proof uses more.

So we have the effective GMT is not provable in Pi-1-1-CA_0 even for
finite tree width. With recursive GMT we obtain 2-consistency of
Pi-1-1-CA_0 and with primitive recursive, elementary recursive GMT we
obtain 1-consistency of Pi-1-1-CA_0 with the usual growth rate and
provably recursive phenomena.

4. INCREASING DOMINATOR THEOREM

NOTE: I screwed up this topic in posting #656:Finite Increasing reducers/1.

DEFINITION 1. An increasing dominator is a function f::A^k into A, A
containedin Q, where for all x,y in A^k, max(x) <= f(x), and if x <= y
then f(x) <= f(y). f is generated by E containedin A if and only if
every element of A can be obtained by applying f zero or more times
using the elements of E.

NOTE: The situation with fusable numbers is not immediately covered
here because of the condition |a-b| < 1. However, we can take the fuse
of a,b to be max(a,b), in case |a-b| >= 1, and then it will be
covered.

INCREASING DOMINATOR THEOREM. The domain of every effective increasing
dominator omits some 1/n. In fact it is well ordered.

The above (both forms) is equivalent to the Kruskal ordinal being well
ordered. I.e., that theta_Omega^omega(0) is well ordered.

EFFECTIVE INCREASING DOMINATOR THEOREM. The domain of every effective
increasing dominator omits some 1/n. In fact it is effectively well
ordered.

If we use recursive in all places then we get the same as in KT. If we
use primitive recursive or elementary recursive in all places (we can
use different ones), then we also get the same as in KT.

5. PARIS HARRINGTON THEOREM

Although of great historical importance, PH (1977) is entirely
superseded by ALT (2010) of section 2 above, 33 years later., put in
Pi02 form as in the joint paper cited (already in my 2010 preprint).
Nevertheless it is worth noting how the theme here for generating
independence results by effectivization works for PH.

INFINITE PH. For all m, every f:[N]^k into {0,...,r} is constant over
a finite set of size at least m and its least element.

EFFECTIVE PH. For all m, every effective f:[N]^k into {0,...,r} is
constant over a finite set of size at least m and its least element.

With recursive we get 2-consistency of PA. With primitive recursive,
elementary recursive, we get 1-consistency of PA with the usual growth
and provably recursive phenomena.

OF COURSE, the (finite) PH is particularly simple from infinite Ramey
statements because cutting down a map from [N]^k into a finite set is
particularly simple. That is not the case with 1-4 above.

6. LEXICOGRAPHIC PATH ORDERING THEOREM

Nachum Dershowitz introduced a very natural and important and useful
set of orderings on terms called LPOs or Lexicographic Path Orderings.
They are defined relative to a language, i.e., the set of terms in a
signature. Dershowitz proved the following using Kruskal's theorem.

LPO THEOREM. Every LPO is a well quasi ordering of the terms in its language.

The "finitization" of the LPO theorem is given by Dershowtiz using it
in the context of TERM REWRITING for which he invented it.

Dershowitz wasn't concerned with any logical strength in the term
rewriting context, but rather its power and use for proving
termination. I got interested in it for establishing "the greatest
computational complexity naturally arising from an interesting
computer science context". In 2001 I wrote

19. Lecture notes on term rewriting and computational complexity,
November 7, 2001, 12 pages.
.in: https://u.osu.edu/friedman.8/foundational-adventures/downloadable-lecture-notes-2/
https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/TermRew110701-1b7ikdn.pdf

I proved there that LPO based term rewriting has computational
complexity <theta_Omega^omega(0) recursion, and that LPO based term
rewriting has the termination properties is equivalent to the same
Pi02 level as Kruska's theorem.

So the finitizations are conveniently provided through the
infrastructure of term rewriting. But in the interest of our theme, we
can go this route.

EFFECtIVE LPO THEOREM. in every effective sequence of terms from a
finite language, some term does not LPO reduce to the next.

We obtain the same phenomena that we had with Kruskal's theorem and
theta_Omega^omega(0).

7. FUSIBLE WELL ORDERING THEOREM

FUSIBLE WELL ORDERING THEOREM. The fusible numbers are a well ordered
set of rationals.

EFFECTIVE FUSIBLE WELL ORDERING THEOREM. In the fusible numbers every
effective sequence stops descending.

This will exhibit the usual Pi03, Pi02, PA, epsilaon_0 stuff provided
we have an elementary recursive map h from epeilson_0 into fusible
numbers such that alpha < beta implies h(alpha) < h(beta)), where this
is provable in EFA for some correct elementary recursive description
of h.

#######################################

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 859th 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

Harvey Friedman