; Copyright (C) 1995 by Ken Kunen.  All Rights Reserved.
; This script is hereby placed in the public domain, and therefore unlimited
; editing and redistribution is permitted.
; NO WARRANTY
; Ken Kunen PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS
; IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT
; NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
; PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
; SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
; ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
; IN NO EVENT WILL Ken Kunen BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
; PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
; ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
; LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
; BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
; DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

; This script is described in Section 4.2 of our paper,
; Non-Constructive Computational Mathematics.
; It includes three items
; ITEM 1: We show that induction on omega^2 is provable in PRA,
; even though there are non-primitive-recursive functions definable
; by recursion on omega^2
; ITEM 2: We use eval$ and v&c$, but not ordinal induction, and
; define the Ackermann function (and prove that the definition is correct).
; ITEM 3: We define a function (next-twin-prime x) and show that either there
; are no twin primes above x or next-twin-prime produces one.
; This is a simple demonstration of the non-constructiveness of eval$ and v&C$

Event: Start with the initial nqthm theory.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;                       ITEM 1                               ;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Represent ordinals below omega^2 as omega X omega, ordered lexically

; Elements of omega X omega are represented as pairs (m . n)

Definition: ordp (p) = (listp (p) ∧ (car (p) ∈ N) ∧ (cdr (p) ∈ N))

Definition: lexp (p1 , p2 ) = ((car (p1 ) < car (p2 ))

∨ ((car (p1 ) = car (p2 )) ∧ (cdr (p1 ) < cdr (p2 ))))

; now let Q be any property of pairs:

Event: Introduce the function symbol q of one argument.

; Assume Q is inductive -- that is:
; NOT Q(p)  --> EXISTS r < p NOT Q(r)
; Of course, to say this in the framework of PRA, we have to assume
; we have a function which gives us an r

Event: Introduce the function symbol g of one argument.

Axiom: q-induction (ordp (p) ∧ (¬ q (p))) → (ordp (g (p)) ∧ lexp (g (p), p) ∧ (¬ q (g (p))))

; Now,  we show Q is true everywhere :   (implies (ordp p) (Q p))
; by ordinary induction
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; First,  by ordinary induction on y (holding x fixed):
; Let fy = (fy x y) <= y be least such that (not (Q (x . fy)))
; fy = F if there is no such y

Definition: fy (x, y) = if y ∉ N then f

elseif y = 0

then if q (cons (x, y)) then f

else y endif elseif fy (x, y − 1) then fy (x, y − 1) elseif q (cons (x, y)) then f else y endif Theorem: q-fails-at-x-fy fy (x, y) → (¬ q (cons (x, fy (x, y))))

Theorem: fy-is-a-number fy (x, y) → (fy (x, y) ∈ N)

Theorem: fy-is-defined ((¬ q (cons (x, y))) ∧ (y ∈ N)) → fy (x, y)

Theorem: fy-leq fy (x, y) → (fy (x, y) ≤ y)

Theorem: fy-lessp (fy (x, y) ∧ q (cons (x, y))) → (fy (x, y) < y)

Theorem: q-below-undefined-fy ((¬ fy (x, y)) ∧ (y ∈ N) ∧ (y1 ∈ N) ∧ (y1 ≤ y)) → q (cons (x, y1 ))

Theorem: fy-is-first (fy (x, y) ∧ (y1 ∈ N) ∧ (y ∈ N) ∧ (y1 < fy (x, y))) → q (cons (x, y1 ))

; now, summarize what the Q-induction says for pairs:

Theorem: form-of-g ((x ∈ N) ∧ (y ∈ N) ∧ (¬ q (cons (x, y))) ∧ (x1 = car (g (cons (x, y)))) ∧ (y1 = cdr (g (cons (x, y))))) → ((x1 ∈ N) ∧ (y1 ∈ N) ∧ (g (cons (x, y)) = cons (x1 , y1 )))

Theorem: g-is-below ((x ∈ N) ∧ (y ∈ N) ∧ (¬ q (cons (x, y))) ∧ (x1 = car (g (cons (x, y)))) ∧ (y1 = cdr (g (cons (x, y))))) → ((x1 < x) ∨ ((x1 = x) ∧ (y1 < y)))

Theorem: q-fails-at-g-aux1 ((¬ q (g (cons (x, y)))) ∧ (g (cons (x, y)) = cons (x1 , y1 ))) → (¬ q (cons (x1 , y1 )))

Theorem: q-fails-at-g ((x ∈ N) ∧ (y ∈ N) ∧ (¬ q (cons (x, y))) ∧ (x1 = car (g (cons (x, y)))) ∧ (y1 = cdr (g (cons (x, y))))) → (¬ q (cons (x1 , y1 )))

Event: Disable q-fails-at-g-aux1.

; Now, if Q fails at x,y then Q fails at x,fy.  If we
; obtain x1,y1 from x,fy as above, we can't have
; (and (equal x1 x) (lessp y1 fy)), so we must have x1 < x

Theorem: smaller-x ((x ∈ N) ∧ (y ∈ N) ∧ (¬ q (cons (x, y))) ∧ (x1 = car (g (cons (x, fy (x, y))))) ∧ (y1 = cdr (g (cons (x, fy (x, y)))))) → ((x1 ∈ N) ∧ (y1 ∈ N) ∧ (x1 < x) ∧ (¬ q (cons (x1 , y1 ))))

; It is immediate from this that Q can never fail

Definition: q-holds-kludge (x, y) = if (x ∈ N)

∧ (y ∈ N)

∧ (¬ q (cons (x, y)))

∧ (car (g (cons (x, fy (x, y)))) ∈ N) ∧ (car (g (cons (x, fy (x, y)))) < x)

then q-holds-kludge (car (g (cons (x, fy (x, y)))), cdr (g (cons (x, fy (x, y))))) else 0 endif

Theorem: q-holds ((x ∈ N) ∧ (y ∈ N)) → q (cons (x, y))

; Finally, re-expressing this in terms of pairs:

Theorem: q-is-true ordp (p) → q (p)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;                       ITEM 2                               ;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 1. We define qval (quick valuation).  This is a version of v&c$ which
;    resets the cost to 0.  One problem with v&c$ is that it explicitly
;    keeps track of the cost.  That makes proving theorems about
;    v&c$ working correctly on specific terms needlessly complicated.
; 2. We re-state the recursive definition of v&c$ in terms of qval.
; 3. We show how to formalize double recursions, such as occur in the
;    definition of the Ackermann function.

; Since v&c$ uses the value of F to signify non-termination:

Definition: reset (x) = if x then cons (car (x), 0)

else f endif

Definition: qval (term, va) = reset (v&c$ (t, term, va))

; va (a "variable assignment") is an association list which
; assigns values to variables.
; qval returns (val . 0) if the computation halts in the normal
; way to return val; otherwise, qval returns F

Definition: qval-list (list-of-terms, va) = if list-of-terms ≃ nil then nil

else cons (qval (car (list-of-terms), va), qval-list (cdr (list-of-terms), va)) endif

; Now, unwind the v&c$ axioms so that they are statements about
; qval and qval-list, and then disable qval and qval-list
; first, the two cases for qval-list:

Theorem: qval-list-empty (lst ≃ nil) → (qval-list (lst, va) = nil)

Theorem: qval-list-non-empty listp (lst) → (qval-list (lst, va) = cons (qval (car (lst), va), qval-list (cdr (lst), va)))

; in proving the cases for qval, it will be useful to have:

Theorem: same-f-membership (f ∈ qval-list (lst, va)) ↔ (f ∈ v&c$ ('list, lst, va))

Theorem: same-strip-cars strip-cars (qval-list (lst, va)) = strip-cars (v&c$ ('list, lst, va))

Event: Disable qval-list.

; now, run down all the cases for qval:
; for a variable name, look up in assoc list

Theorem: qval-litatom litatom (term) → (qval (term, va) = cons (cdr (assoc (term, va)), 0))

; for a constant, return that constant value:

Theorem: qval-constant ((¬ litatom (term)) ∧ (term ≃ nil)) → (qval (term, va) = cons (term, 0))

; for a quoted expression, return the expression

Theorem: qval-quote qval (list ('quote, object), va) = cons (object, 0)

; evaluating an (if ...):

Theorem: qval-if qval (list ('if, test, thencase, elsecase), va) = if qval (test, va)

then if car (qval (test, va)) then qval (thencase, va)

else qval (elsecase, va) endif else f endif

; except for (if ...) and (quote ...) : if evaluation of some
; arg doesn't halt, then qval doesn't halt.

Theorem: qval-args-dont-halt-aux1 ((fn ≠ 'quote) ∧ (fn ≠ 'if) ∧ (f ∈ v&c$ ('list, args, va))) → (v&c$ (t, cons (fn, args), va) = f)

Theorem: qval-args-dont-halt ((fn ≠ 'quote) ∧ (fn ≠ 'if) ∧ (f ∈ qval-list (args, va))) → (qval (cons (fn, args), va) = f)

; for a SUBR (a basic built-in) other than "if": if evaluation of the args
; does halt, just use APPLY-SUBR on the value of args
; STRIP-CARS applied to ( (val1 . 0) (val2 . 0) ... ) returns (val1 val2 ...)

Theorem: qval-subr-aux1 ((f ∉ v&c$ ('list, args, va)) ∧ (fn ≠ 'if) ∧ subrp (fn)) → (v&c$ (t, cons (fn, args), va)

= cons (apply-subr (fn, strip-cars (v&c$ ('list, args, va))), 1 + sum-cdrs (v&c$ ('list, args, va))))

; the following auxiliary is trivial,
; but the prover hangs on it:

Theorem: qval-subr-aux2 ((vvv = cons (uu, anything)) ∧ a ∧ b ∧ c ∧ d ∧ e) → (car (vvv) = uu)

Theorem: qval-subr ((f ∉ qval-list (args, va)) ∧ (fn ≠ 'if) ∧ subrp (fn)) → (qval (cons (fn, args), va)

= cons (apply-subr (fn, strip-cars (qval-list (args, va))), 0))

Event: Disable qval-subr-aux2.

; for a non-SUBR (a basic built-in) other than "quote":
; if evaluation of the args does halt, just evaluate
; the BODY of the function on the
; FORMALS of the function, paired with the value of the args

Theorem: qval-non-subr-aux1 ((fn ≠ 'quote) ∧ (f ∉ v&c$ ('list, args, va)) ∧ (¬ subrp (fn))) → (v&c$ (t, cons (fn, args), va)

= fix-cost (v&c$ (t, body (fn), pairlist (formals (fn),

strip-cars (v&c$ ('list, args, va)))),

1 + sum-cdrs (v&c$ ('list, args, va))))

; again, the prover hangs on a trivial point

Theorem: qval-non-subr-aux2 (x1 ∧ (v1 = cons (w, x2 )) ∧ x3 ∧ x4 ∧ x5 ∧ x6 ∧ x7 ) → (car (v1 ) = w)

Theorem: qval-non-subr ((f ∉ qval-list (args, va)) ∧ (fn ≠ 'quote) ∧ (¬ subrp (fn))) → (qval (cons (fn, args), va)

= qval (body (fn), pairlist (formals (fn), strip-cars (qval-list (args, va)))))

Event: Disable qval-non-subr-aux2.

; from now on, we need only the properties of qval and qval-list,
; not how they were defined:

Event: Disable qval.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; We illustrate the method by showing how to justify a double
; recursion, such as the definition of the Ackermann function:

;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;   Values of Ackermann Function
;
;    ---------------------
;  3| 1   2   4  16  2^16
;   |---------------------
;  2| 1   2   4   8   16
;   |---------------------
;  1| 1   2   4   6   8
;   |---------------------
;  0| 1   2   4   5   6
;   |_____________________
;     0   1   2   3   4
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; We can think of row 0 as given.  Row n+1 is obtained by
; iterating the function on row n, starting with a 1 in column 0.

Definition: row0 (x)

= if x ≃ 0 then 1 elseif x = 1 then 2 else x + 2 endif

Definition: row1 (x) = if x ≃ 0 then 1

else row0 (row1 (x − 1)) endif

Definition: row2 (x) = if x ≃ 0 then 1

else row1 (row2 (x − 1)) endif

Definition: row3 (x) = if x ≃ 0 then 1

else row2 (row3 (x − 1)) endif

; GOAL: define a function, ACKERMANN, and prove
; (prove-lemma ackermann-works (rewrite) (equal (ackermann x y)
;  (if (zerop x) 1
;  (if (zerop y) (if (equal x 1) 2 (plus x 2))
;  (ackermann (ackermann (sub1 x) y) (sub1 y))  ))))
; Without using ordinals and ord-lessp, we can't just use this
; as a definition.  However, we can use EVAL$ to define
; function whose body looks like this.  To simplify the work, we
; phrase the defn of ack so that the body is as simple as possible

Definition: base (x, y) = ((x ≃ 0) ∨ (y ≃ 0))

Definition: base-fn (x, y) = if y ≃ 0 then row0 (x)

else 1 endif

; intended defn of ack is now:
;(defn ack (x y) (if (base x y) (base-fn x y)  (ack (ack (sub1 x) y) (sub1 y))))
; instead, use eval$ :

Definition: ack (x, y)

= eval$ (t,

         '(if
           (base x y)
           (base-fn x y)
           (ack (ack (sub1 x) y) (sub1 y))),

list (cons ('x, x), cons ('y, y)))

;;;;;;;;;;;;;;;;;;;;;;;  begin r-loop
; *(body 'ack)
;  '(IF (BASE X Y)
;       (BASE-FN X Y)
;       (ACK (ACK (SUB1 X) Y) (SUB1 Y)))
; *(formals 'ack)
;  '(X Y)
; *(ack 3 1)
;  6
; *(ack 2 3)
;  4
; *(ack 4 2)
;  16
; *(qval '(ack x y) '( (x . 4) (y . 2) ))
;  '(16 . 0)
;;;;;;;;;;;;;;;;;;;;;;;  end r-loop
; Now that we have arranged for ack to have the correct body and formals,
; we never use eval$ again.  We can define the official Ackermann function
; using qval, and then prove inductively that it works.
; Since the formals will always be '(x y), we can simplify
; some of the general notation:

Definition: assn (valx, valy) = list (cons ('x, valx), cons ('y, valy))

Definition: a (valx, valy) = qval ('(ack x y), assn (valx, valy))

Definition: ackermann (valx, valy) = car (a (valx, valy))

; Proving that ackermann works involves proving first that (A valx valy)
; holds (i.e., it is never F).
; First, since qval-list will always be operating on lists of terms of
; length two, let's concretely unwind that situation:

Theorem: qval-list-1 qval-list (list (term), va) = list (qval (term, va))

Theorem: qval-list-2 qval-list (list (term1 , term2 ), va) = list (qval (term1 , va), qval (term2 , va))

Event: Disable qval-list-non-empty.

; Now, analyze how qval works on sub-expressions of the body:
;   (if (base x y) (base-fn x y) (ack (ack (sub1 x) y) (sub1 y)))

Theorem: qval-on-x qval ('x, assn (valx, valy)) = cons (valx, 0)

Theorem: qval-on-y qval ('y, assn (valx, valy)) = cons (valy, 0)

Theorem: qval-on-sub1-x qval ('(sub1 x), assn (valx, valy)) = cons (valx − 1, 0)

Theorem: qval-on-sub1-y qval ('(sub1 y), assn (valx, valy)) = cons (valy − 1, 0)

Theorem: qval-on-base qval ('(base x y), assn (valx, valy)) = cons (base (valx, valy), 0)

Theorem: qval-on-base-fn qval ('(base-fn x y), assn (valx, valy)) = cons (base-fn (valx, valy), 0)

; on the whole body

Theorem: qval-on-body qval ('(if

       (base x y)
       (base-fn x y)
       (ack (ack (sub1 x) y) (sub1 y))),

assn (valx, valy)) = if base (valx, valy) then cons (base-fn (valx, valy), 0)

    else qval ('(ack (ack (sub1 x) y) (sub1 y)),

assn (valx, valy)) endif

; Now on the ack expressions, we need two things:
; 1. Unwind the (qval '(ack x y) (assn valx valy)) in
;    the defn of (A valx valy) so we can prove thms about A
; 2. Reduce qval of the two ack expressions in the body:

;      (ack (sub1 x) y)       (ack (ack (sub1 x) y) (sub1 y))
;    to a qval of (ack x y)
; towards (2):

Theorem: qval-of-ack-of-terms-aux1 (qval (term1 , va) ∧ qval (term2 , va)) → (qval (list ('ack, term1 , term2 ), va)

= qval ('(if

               (base x y)
               (base-fn x y)
               (ack (ack (sub1 x) y) (sub1 y))),

assn (car (qval (term1 , va)), car (qval (term2 , va)))))

; as a special case, for (ack x y):

Theorem: qval-of-ackxy-aux1 qval ('(ack x y), assn (valx, valy)) = qval ('(if

           (base x y)
           (base-fn x y)
           (ack (ack (sub1 x) y) (sub1 y))),

assn (valx, valy))

; we can unwind the if expr later -- first, let's reduce the
; (ack term1 term2).

Theorem: qval-of-ack-of-terms (qval (term1 , va) ∧ qval (term2 , va)) → (qval (list ('ack, term1 , term2 ), va)

     = qval ('(ack x y),

assn (car (qval (term1 , va)), car (qval (term2 , va)))))

Event: Disable qval-of-ack-of-terms-aux1.

; Now, unwinding the if expr:

Theorem: qval-of-ackxy qval ('(ack x y), assn (valx, valy)) = if base (valx, valy) then cons (base-fn (valx, valy), 0)

    else qval ('(ack (ack (sub1 x) y) (sub1 y)),

assn (valx, valy)) endif Event: Disable qval-of-ackxy-aux1.

; now, qval-of-ackxy would be simpler if we split it into
; the two cases base/non-base

Theorem: qval-of-ackxy-base base (valx, valy) → (qval ('(ack x y), assn (valx, valy)) = cons (base-fn (valx, valy), 0))

Theorem: qval-of-ackxy-non-base-aux1 (¬ base (valx, valy)) → (qval ('(ack x y), assn (valx, valy))

     = qval ('(ack (ack (sub1 x) y) (sub1 y)),

assn (valx, valy)))

; we have to analyze this further

Event: Disable qval-of-ackxy.

; Now, we have to reduce the two ack expressions in the body:
;      (ack (sub1 x) y)       (ack (ack (sub1 x) y) (sub1 y))
;         small                       big

Theorem: qval-of-ack-small qval ('(ack (sub1 x) y), assn (valx, valy)) = qval ('(ack x y), assn (valx − 1, valy))

Theorem: qval-of-ack-big qval ('(ack x y), assn (valx − 1, valy))

 → (qval ('(ack (ack (sub1 x) y) (sub1 y)), assn (valx, valy))
     = qval ('(ack x y),

assn (car (qval ('(ack (sub1 x) y), assn (valx, valy))), valy − 1)))

Event: Disable qval-of-ack-of-terms.

; we only need it for "small" and "big"
; using these, we can analyze the non-base case

Theorem: qval-of-ackxy-non-base ((¬ base (valx, valy)) ∧ qval ('(ack x y), assn (valx − 1, valy))) → (qval ('(ack x y), assn (valx, valy))

     = qval ('(ack x y),

assn (car (qval ('(ack x y), assn (valx − 1, valy))), valy − 1)))

Event: Disable qval-of-ackxy-non-base-aux1.

Event: Disable assn.

; this is no longer needed, and it really slows things
; down when assn is unwound
; Now, let's prove : (A valx valy) by induction on (valx valy).
; Then -- we can remove the (qval '(ack x y) ...) hypotheses

Theorem: a-is-true-aux1 base (valx, valy) → a (valx, valy)

; specifically, there is only a problem if valx or valy are non-zero

Theorem: a-is-true-aux2 (valx ≃ 0) → a (valx, valy)

Theorem: a-is-true-aux3 (valy ≃ 0) → a (valx, valy)

; let's give a name to the x-value called in qval-of-ackxy-non-base

Definition: prev (valx, valy) = car (qval ('(ack x y), assn (valx − 1, valy)))

; this will make the induction simpler

Theorem: a-is-true-aux4 ((¬ base (valx, valy)) ∧ a (valx − 1, valy) ∧ a (prev (valx, valy), valy − 1)) → a (valx, valy)

Event: Disable a.

; temporarily

Event: Disable prev.

; permanently
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; We have enough now to prove that (A valx valy) is true by double induction,
; as in ITEM 1, above.
; If (A valx valy) fails, then (A valx' valy') fails, where
; (valy' valx') is lexically earlier than (valy valx).
; First,  by ordinary induction on valx (holding valy fixed):
; if (not (A valx valy)), there is a first-value,
; fx = (fx valx valy), such that: (not (A fx valy)) but (A (sub1 fx) valy)

Definition: fx (valx, valy) = if valx ≃ 0 then f

elseif (¬ a (valx, valy)) ∧ a (valx − 1, valy) then valx else fx (valx − 1, valy) endif

Theorem: fx-is-first-1 (¬ a (valx, valy)) → (¬ a (fx (valx, valy), valy))

Theorem: fx-is-first-2 (¬ a (valx, valy)) → a (fx (valx, valy) − 1, valy)

; now, reexamine what A-is-true-aux4 says

Theorem: a-is-true-aux5 (¬ a (valx, valy)) → (¬ a (prev (fx (valx, valy), valy), valy − 1))

Definition: a-is-true-kludge (valx, valy) = if valy ≃ 0 then 0

else a-is-true-kludge (prev (fx (valx, valy), valy), valy − 1) endif

Theorem: a-is-true a (valx, valy)

Event: Disable a-is-true-aux1.

Event: Disable a-is-true-aux2.

Event: Disable a-is-true-aux3. Event: Disable a-is-true-aux4. Event: Disable a-is-true-aux5. Event: Disable fx. Event: Disable fx-is-first-1. Event: Disable fx-is-first-2. Event: Disable a-is-true-kludge.

; now, we do care what A is

Event: Enable a.

; while we rephrase  qval-of-ackxy-base and  qval-of-ackxy-non-base
; in terms of A, using the fact that A is true:

Theorem: a-base base (valx, valy) → (a (valx, valy) = cons (base-fn (valx, valy), 0)) Theorem: a-induction (¬ base (valx, valy)) → (a (valx, valy) = a (car (a (valx − 1, valy)), valy − 1))

; Now, we can forget how A was defined; its car satisfies
; the defn of the Ackermann function

Event: Disable a.

; GOAL:

Theorem: ackermann-works ackermann (x, y) = if x ≃ 0 then 1

elseif y ≃ 0 then if x = 1 then 2

else x + 2 endif else ackermann (ackermann (x − 1, y), y − 1) endif

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;                       ITEM 3                               ;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; GOAL:  define a function
; (next-twin-prime x) and prove, that for each x
; either:
;   1. (next-twin-prime x) is some y > x such that y, y+2 are both prime
; or
;   2. (next-twin-prime x) = F, and
;      for all y > x, it isn't true that y and y+2 are both prime
; First, define some primitive recursive functions
; a divisor of x between 2 and top (inclusively), or,  F if there is none :

Definition: divisor (x, top) = if top < 2 then f

elseif divisor (x, top − 1) then divisor (x, top − 1)

elseif (x mod top) ≃ 0 then top

else f endif

Definition: primep (x) = ((1 < x) ∧ (¬ divisor (x, x − 1)))

; y is the first part of a prime pair

Definition: fpp (y) = (primep (y) ∧ primep (1 + (1 + y)))

; intended -- by upwards recursion
; (defn next-twin-prime(x) (if (fpp (add1 x))
;  (add1 x)
;  (next-twin-prime (add1 x))))
; obviously, this won't be accepted, but in Nqthm, one can do this with eval$ :

Definition: ntp (x) = eval$ (t,

         '(if (fpp (add1 x)) (add1 x) (ntp (add1 x))),

list (cons ('x, x)))

;;;;;;;;;;;;;;;;;;;;;;;  begin r-loop
;
; *(formals 'ntp)
;  '(X)
; *(body 'ntp)
;  '(IF (FPP (ADD1 X))
;       (ADD1 X)
;       (NTP (ADD1 X)))
; *(ntp 8)
;  11
; *(ntp 19)
;  29
; *(formals 'fpp)
;  '(Y)
; *(body 'fpp)
;  '(AND (PRIMEP Y)
;        (PRIMEP (ADD1 (ADD1 Y))))
;
;;;;;;;;;;;;;;;;;;;;;;;  end r-loop
; Of course, this doesn't prove anything.
; We want to define next-twin-prime AND PROVE IT WORKS
; Using the same trick as with the Ackermann function:

Definition: n (valx) = qval ('(ntp x), list (cons ('x, valx)))

; Now, we have to analyze qval on the body of ntp
;  '(if (fpp (add1 x)) (add1 x) (ntp (add1 x)))
; Fortunately, for a pure primitive recursive function, such as fpp.
; the Nqthm built-ins REWRITE-V&C-APPLY$ and REWRITE-CAR-V&C-APPLY$
; easily prove that v&c$ does the right thing; so:

Theorem: qval-on-fpp qval (term, va) → (qval (list ('fpp, term), va) = cons (fpp (car (qval (term, va))), 0))

Event: Disable fpp.

; as with ack, we have to compare qval on an expression
; (ntp term) with qval on the basic (ntp x)

Theorem: qval-on-ntp-term qval (term, va) → (qval (list ('ntp, term), va)

= qval ('(ntp x), list (cons ('x, car (qval (term, va))))))

; we can rewrite this in terms of N

Theorem: qval-on-ntp-term-n qval (term, va) → (qval (list ('ntp, term), va) = n (car (qval (term, va))))

; Now, the relevant term in the body is just (add1 x), so:

Theorem: qval-on-ntp-add1 qval ('(ntp (add1 x)), list (cons ('x, valx))) = n (1 + valx)

; now, we unwind the defn of N:

Theorem: unwind-1 n (valx)

= qval ('(if (fpp (add1 x)) (add1 x) (ntp (add1 x))),

list (cons ('x, valx)))

Theorem: unwind-2 qval ('(fpp (add1 x)), va) = cons (fpp (1 + cdr (assoc ('x, va))), 0)

Theorem: unwind-3

qval ('(if (fpp (add1 x)) (add1 x) (ntp (add1 x))), va)

= if fpp (1 + cdr (assoc ('x, va))) then cons (1 + cdr (assoc ('x, va)), 0) else qval ('(ntp (add1 x)), va) endif

Theorem: unwind-4 n (valx) = if fpp (1 + valx) then cons (1 + valx, 0)

else qval ('(ntp (add1 x)), list (cons ('x, valx))) endif

Theorem: unwind-5 n (valx) = if fpp (1 + valx) then cons (1 + valx, 0)

else n (1 + valx) endif

Event: Disable unwind-1.

Event: Disable unwind-2.

Event: Disable unwind-3.

Event: Disable unwind-4.

Event: Disable unwind-5.

; now, we can justify the upward recursion:

Theorem: n-basis fpp (1 + x) → (n (x) = cons (1 + x, 0)) Theorem: n-induction (¬ fpp (1 + x)) → (n (x) = n (1 + x))

; it might be useful to know the form of N

Theorem: form-of-n n (x) → (n (x) = cons (car (n (x)), 0)) Theorem: n-of-zero (x ≃ 0) → (n (x) = '(3 . 0)) Definition: good (x) = (fpp (car (n (x))) ∧ (x < car (n (x))))

; so, the twin prime conjecture will imply that all x are good
; we don't need the defn of N any more:

Event: Disable n.

Theorem: n-of-fpp fpp (x) → (n (x − 1) = cons (x, 0)) Theorem: n-of-non-fpp ((¬ fpp (x)) ∧ (x ≄ 0)) → (n (x − 1) = n (x)) Theorem: zero-is-good (x ≃ 0) → good (x) Theorem: good-goes-down-aux1 fpp (x) → good (x − 1)

Theorem: good-goes-down-aux2 ((¬ fpp (x)) ∧ (x ≄ 0) ∧ good (x)) → good (x − 1)

Theorem: good-goes-down good (x) → good (x − 1)

; Next, we prove that (fpp y) and x < y implies (good x)

Definition: good-below-kludge (y, z) = if z ≃ 0 then 0

else good-below-kludge (y, z − 1) endif

Theorem: good-below-aux1 ((y − 1) − z) = ((y − z) − 1)

Theorem: good-below-aux2 fpp (y) → good (y − (1 + z))

Event: Disable good-below-aux1.

Event: Disable good-below-aux2.

Theorem: good-below-aux3 ((x < y) ∧ (x ∈ N)) → ((y − (1 + ((y − x) − 1))) = x)

Theorem: good-below (fpp (y) ∧ (x < y)) → good (x)

Event: Disable good-below-aux3.

; now, every x is either good or not good.
; if x is not good, there are no twin primes above x:

Theorem: properties-of-bad-aux1 ((¬ good (x)) ∧ (x < y)) → (¬ fpp (y))

; on the other hand, if x is good, then by the definition

Theorem: properties-of-good-aux1 good (x) → (fpp (car (n (x))) ∧ (x < car (n (x))))

; Now, we can define next-twin-prime as:

Definition: next-twin-prime (x) = if good (x) then car (n (x))

else f endif

Event: Disable good-below.

Event: Disable good.

; finally, GOAL:
; EITHER
;   1. (next-twin-prime x) is some y > x such that y, y+2 are both prime

Theorem: properties-of-good good (x) → (fpp (next-twin-prime (x)) ∧ (x < next-twin-prime (x)))

; OR
;   2. (next-twin-prime x) = F, and
;      for all y > x, it isn't true that y and y+2 are both prime

Theorem: properties-of-bad-1 (¬ good (x)) → (next-twin-prime (x) = f)

Theorem: properties-of-bad-2 ((¬ good (x)) ∧ (x < y)) → (¬ fpp (y))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;                       THE END                              ;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Index

a, 10, 14–16 a-base, 16 a-induction, 16 a-is-true, 15 a-is-true-aux1, 14 a-is-true-aux2, 14 a-is-true-aux3, 14 a-is-true-aux4, 14 a-is-true-aux5, 15 a-is-true-kludge, 15 ack, 9 ackermann, 10, 16, 17 ackermann-works, 16 assn, 10–14

base, 9, 11–14, 16 base-fn, 9, 11–13, 16

divisor, 17

form-of-g, 3 form-of-n, 20 fpp, 17–22 fx, 15 fx-is-first-1, 15 fx-is-first-2, 15 fy, 2–4 fy-is-a-number, 3 fy-is-defined, 3 fy-is-first, 3 fy-leq, 3 fy-lessp, 3

g, 2–4 g-is-below, 3 good, 20–22 good-below, 21 good-below-aux1, 21 good-below-aux2, 21 good-below-aux3, 21 good-below-kludge, 21 good-goes-down, 21 good-goes-down-aux1, 20 good-goes-down-aux2, 21

lexp, 2

n, 18–22 n-basis, 20 n-induction, 20 n-of-fpp, 20 n-of-non-fpp, 20 n-of-zero, 20 next-twin-prime, 22 ntp, 17

ordp, 2, 4

prev, 14, 15 primep, 17 properties-of-bad-1, 22 properties-of-bad-2, 22 properties-of-bad-aux1, 21 properties-of-good, 22 properties-of-good-aux1, 21

q, 2–4

q-below-undefined-fy, 3

q-fails-at-g, 4

q-fails-at-g-aux1, 3 q-fails-at-x-fy, 3 q-holds, 4 q-holds-kludge, 4 q-induction, 2 q-is-true, 4 qval, 5–8, 10–14, 18, 19 qval-args-dont-halt, 6 qval-args-dont-halt-aux1, 6 qval-constant, 6 qval-if, 6 qval-list, 5–8, 11 qval-list-1, 11 qval-list-2, 11 qval-list-empty, 5 qval-list-non-empty, 5 qval-litatom, 6 qval-non-subr, 8 qval-non-subr-aux1, 7 qval-non-subr-aux2, 7 qval-of-ack-big, 13 qval-of-ack-of-terms, 12 qval-of-ack-of-terms-aux1, 12 qval-of-ack-small, 13 qval-of-ackxy, 12 qval-of-ackxy-aux1, 12 qval-of-ackxy-base, 13 qval-of-ackxy-non-base, 14 qval-of-ackxy-non-base-aux1, 13 qval-on-base, 11 qval-on-base-fn, 11 qval-on-body, 11 qval-on-fpp, 18 qval-on-ntp-add1, 19 qval-on-ntp-term, 19 qval-on-ntp-term-n, 19 qval-on-sub1-x, 11 qval-on-sub1-y, 11 qval-on-x, 11 qval-on-y, 11 qval-quote, 6 qval-subr, 7 qval-subr-aux1, 7 qval-subr-aux2, 7

reset, 5 row0, 8, 9 row1, 9 row2, 9 row3, 9

same-f-membership, 6 same-strip-cars, 6 smaller-x, 4

unwind-1, 19 unwind-2, 19 unwind-3, 19 unwind-4, 19 unwind-5, 19

zero-is-good, 20