[FOM] 650: Necessary Irrelevance 3

[Harvey Friedman]

We have made two postings on Necessary Irrelevance. Both contain
sketches of proofs.

http://www.cs.nyu.edu/pipermail/fom/2015-December/019383.html
http://www.cs.nyu.edu/pipermail/fom/2015-December/019385.html

Here we make what is proved in the first posting a bit clearer, and
just restate what is proved in the second posting. For proof sketches
see the original two postings.

The general idea here is as follows. Suppose phi is a theorem of the
usual Peano Arithmetic with primitive recursive function symbols. The
induction used to prove phi may use primitive recursive function
symbols that do not appear in phi. In fact, they may not even have
been used to build up (introduce) the function symbols appearing in
phi. Such a state of affairs may be necessary.

This may be required (see below). In this case, we have what may be
viewed as an irrelevancy - in fact, a necessary irrelevancy.

1. PA(prim)

PA(prim) is the usual full Peano Arithmetic with primitive recursive
function symbols. The language L(prim) is 0,S,=, together with all
primitive recursive function symbols. The axioms are

1. Successor axioms. Sx not= 0, Sx = Sy implies x = y.
2. Primitive recursion equations going back to Kleene.
3. Induction for all formulas in L(prim).

For each primitive recursive function symbol F, there is the obvious
language fragment L(F) of PA(prim) consisting of 0,S,= together with
all primitive recursive function symbols leading up to F, including F.
The axioms of PA(F) consist of the axioms of PA(prim) that lie in
L(F).

THEOREM 1.1. There is a unary primitive recursive function symbol F
such that the statement "F has no zero" is provable in PA(prim) but
not in PA(F).

Thus any proof in PA(prim) of "F has no zero" must necessarily use an
irrelevancy.

Here is a sharper form.

THEOREM 1.2. Let k >= 1. There is a unary primitive recursive function
symbol F such that the statement "F has no zero" is provable in
PA(prim) but not in the following system:
1. Successor axioms.
2. Defining equations for + and base 2 exponentiation.
3. Induction for all formulas using only 0,S,+,2^, and the functions
leading up to F, including F.
4. All induction axioms of PA(prim) that apply induction to Sigma-0-k formula.

Proof: See http://www.cs.nyu.edu/pipermail/fom/2015-December/019383.html . QED

2. 0,S,D.

Here D is doubling on N. PA(0,S,D) is

1. Successor axioms. Sn not= 0, Sn = Sm implies n = m.
2. D0 = 0, DSn = SSDn.
3. Induction for all formulas in 0,S,D,=.

THEOREM. The theorem (of primitive recursive arithmetic)

Dn = n implies n = 0

is not provable in PA(0,S,D).

Proof: See http://www.cs.nyu.edu/pipermail/fom/2015-December/019385.html . QED

Thus any proof in PA(prim) of "Dx = x implies x = 0" must necessarily
use an irrelevancy.

**********************************************************
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 650th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM
629: Boolean Algebra/Simplicity  10/3/15  9:41AM
630: Optimal Function Theory 8  10/3/15  6PM
631: Order Theoretic Optimization 1  10/1215  12:16AM
632: Rigorous Formalization of Mathematics 1  10/13/15  8:12PM
633: Constrained Function Theory 1  10/18/15 1AM
634: Fixed Point Minimization 1  10/20/15  11:47PM
635: Fixed Point Minimization 2  10/21/15  11:52PM
636: Fixed Point Minimization 3  10/22/15  5:49PM
637: Progress in Pi01 Incompleteness 1  10/25/15  8:45PM
638: Rigorous Formalization of Mathematics 2  10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2  10/27/15  10:38PM
640: Progress in Pi01 Incompleteness 3  10/30/15  2:30PM
641: Progress in Pi01 Incompleteness 4  10/31/15  8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1  11/3/15  11:57PM
644: Fixed Point Selectors 1  11/16/15  8:38AM
645: Fixed Point Minimizers #1  11/22/15  7:46PM
646: Philosophy of Incompleteness 1  Nov 24 17:19:46 EST 2015
647: General Incompleteness almost everywhere 1  11/30/15  6:52PM
648: Necessary Irrelevance 1  12/21/15  4:01AM
649: Necessary Irrelevance 2  12/21/15  8:53PM

Harvey Friedman