[FOM] 649: Necessary Irrelevance 2

Mon Dec 21 20:53:05 EST 2015

http://www.cs.nyu.edu/pipermail/fom/2015-December/019383.html dealt
with strong examples of Necessary Irrelevance within PA(prim) - see
Theorem 3 there.

We now take up a weak example of Necessary Irrelevance within PRA.

0,S, AND DOUBLING

We use D for doubling on N.

Recall from http://www.cs.nyu.edu/pipermail/fom/2015-December/019383.html
that 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,=.

We show that he PRA theorem

Dn = n implies n = 0

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

We use the structure M = (A,S,D), where

i. A is 0,1,2,... together with the c+n, where n is an integer. Thus
we are using an "infinite" element c.
ii. S(c+n) = c+(n+1).
iii. D(c+n) = c+(2n).

It suffices to show that M satisfies induction for all formulas in 0,S,D,=.

We first perform an elimination of quantifiers for M'. For this, we
need to expand the language of M as follows.M' = (0,S,P,D,H,H'). Here
a. P(n) = n-1 if n > 0; 0 otherwise.
b. P(c+n) = c+(n-1).
c. H(n) is the floor of n/2. H(c+n) = c+(floor of n/2).

We use x as a distinguished variable.

LEMMA 1. in M', every formula s = t, where x mentions x and t does
not, is equivalent to a propositional combination of atomic formulas
that either do not mention x, or are of the form x = t, where t does
not mention x.

Proof: Let t not mention x. Dx = t if and only if x = Ht = HSt. Hx = t
if and only if x = Dt or x = SDt, Sx = t if and only if x = Pt and t
not= 0. Px = t if and only if x = St or x = t = 0. QED

DEFINITION. A principal class in dom(M) is the symmetric difference of
a finite union of congruence classes in dom(M) modulo a power of 2
(i.e., 2,4,8,16,...), and a finite set.

LEMMA 2. In M', every formula s = t, where s,t both mention x, is
equivalent to a statement x in S, where S is a principal class.

Proof: First look at the D's and H's in s,t. If the aggregations for s
and for t are not the same, then s = t must fail except for x lying in
a definitely given finite set {0,...,m} union {c+i: i in {-m,...,m}}.
this reduces s = t to a propositional combination of evaluations of x.
If the aggregations for s and for t are the same, then s = t depends
only on the appropriate principal class of x, with exceptions from a
definitely given {0,...,m}. QED

LEMMA 3. M' admits elimination of quantifiers. Every subset of dom(M)
that is M' definable is a principal class.

Proof: We start with (there exists x)(phi_1 and ... and phi_k), where
the phi's are literals. Apply Lemmas 1,2, and obtain a propositional
combination of formulas

(there exists x)(x = s_1 and ... and x = s_p and x not= t_1 and ...
and x not= t_q and x in S)

where S is an almost congruence class, and  the s_i,t_j do not mention
x. If p >= 1 then eliminate the quantifier in the obvious way. Assume
p = 0. Then we get

     S has an element not among t_1,...,t_q.

There is an explicitly given standard integer r such that the above is
equivalent to

     S has an element among {t_1 - r,...,t_1 + r, t_2 - r,...,t_2 +
r,...,t_q - r,...,t_q + r} that is not among t_1,...,t_q.

We then use S,P,D,H to replace the use of principal classes in the above.

For the second claim, use the first claim and Lemmas 1,2. QED

THEOREM 4. Induction for the language of M' = (A,S,P,D,H) holds in M'.
PA(0,S,D) holds in M, yet in M, the equation Dx = x has a nonzero
solution.

Proof: From Lemma 3 and the obvious fact that any principal class in A
containing 0 and closed under successor is all of dom(M). 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 649th 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

Harvey Friedman