an inequality for natexp

Johan G. F. Belinfante
2006 November 30

SetDirectory["l:"];  << goedel87.30a; << tools.m

summary

The binomial theorem says that (((1  +  x))^n) = 1 + n x + ··· .  If all variables refer to natural numbers, the unwritten terms can only increase the sum on the right, and therefore  n x < (((1  +  x))^n). This basic inequality for exponentiation of natural numbers is derived in this notebook directly using induction, without reference to the binomial theorem.

simplification rules

Lemma.

Assoc[NATEXP, id[cart[omega, omega]], id[cart[V, omega]]] // 
      Reverse

composite[NATEXP, id[cart[V, omega]]] := NATEXP

Similarly:

Assoc[NATEXP, id[cart[omega, omega]], id[cart[omega, V]]] // 
      Reverse

composite[NATEXP, id[cart[omega, V]]] := NATEXP

An application needed below is this result:

Map[image[#, y] &, 
        SubstTest[fix, 
          composite[v, id[u]], {u -> cart[V, omega], 
            v -> composite[inverse[x], NATEXP]}]] // 
      InvertFix

intersection[omega, image[fix[composite[inverse[NATEXP], x_]], y_]] := 
      image[fix[composite[inverse[NATEXP], x]], y]

nonself-membership for natexp

SubstTest[or, not[member[z, omega]], not[member[z, z]], 
        z -> natexp[x, y]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

SubstTest[implies, equal[z, V], not[member[z, z]], 
        z -> natexp[x, y]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Map[not, 
      SubstTest[and, implies[p, q], 
        or[p, q], {p -> and[member[x, omega], member[y, omega]], 
          q -> not[member[natexp[x, y], natexp[x, y]]]}]]

member[natexp[x_, y_], natexp[x_, y_]] := False

a conditional rule for removing nat wrappers

implies[member[x, omega], equal[nat[U[x]], U[x]]]

nat[U[x_]] := U[x]  /;  member[x, omega]

an inequality for natexp:   n x < (((1  +  x))^n)

In the GOEDEL program, induction must be applied to an inductive class, not to a statement:

implies[INDUCTIVE[x], subclass[omega, x]]

The idea is to fix the base and use induction on the exponent.  The class to which induction must be applied is:

class[y, member[natmul[z, y], natexp[succ[z], y]]] /. 
      z -> nat[x]

The following lemma suffices for the base case:

member[pair[succ[nat[x]], 0], 
        fix[composite[inverse[NATEXP], 
            inverse[IMAGE[inverse[times[nat[x]]]]], E, SECOND]]] // 
      AssertTest

(% /. x -> x_) /. Equal -> SetDelayed

For the induction step, the following temporary lemma is needed to crack open the fixed point class.

member[pair[u, v], 
        fix[composite[inverse[NATEXP], 
            inverse[IMAGE[inverse[times[nat[x]]]]], E, SECOND]]] // 
      AssertTest

member[pair[u_, v_], 
        fix[composite[inverse[NATEXP], 
            inverse[IMAGE[inverse[times[nat[x_]]]]], E, SECOND]]] := 
      and[member[u, omega], member[v, omega], 
        member[natmul[v, nat[x]], natexp[u, v]]]

Lemma.

(SubstTest[implies, 
            and[subclass[nat[z], nat[s]], member[nat[s], nat[w]]], 
            member[nat[z], nat[w]], s -> natadd[nat[t], nat[z]]] // 
          Reverse) /. {w -> natmul[nat[x], nat[y]], 
        t -> natmul[nat[x], nat[z]]}

(% /. {x -> x_, y -> y_, z -> z_}) /. 
      Equal -> SetDelayed

Lemma.

SubstTest[succ, U[nat[u]], u -> natexp[succ[nat[x]], nat[y]]] // 
      Reverse

succ[U[natexp[succ[nat[x_]], nat[y_]]]] := 
      natexp[succ[nat[x]], nat[y]]

more

Lemma.

SubstTest[or, 
        member[natadd[nat[x], natmul[nat[x], nat[y]]], 
          natadd[succ[nat[t]], natmul[nat[x], succ[nat[t]]]]], 
        not[member[natmul[nat[x], nat[y]], succ[nat[t]]]], 
        t -> natexp[succ[nat[x]], nat[y]]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.

SubstTest[implies, equal[t, succ[nat[s]]], 
        or[member[natadd[nat[x], natmul[nat[x], nat[y]]], 
            natadd[t, natmul[t, nat[x]]]], 
          not[member[natmul[nat[x], nat[y]], t]]], {s -> 
            U[natexp[succ[nat[x]], nat[y]]], 
          t -> natexp[succ[nat[x]], nat[y]]}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

The nat wrapper on y needs to be removed prior to eliminating this variable.

SubstTest[implies, equal[y, nat[t]], 
        or[member[natadd[nat[x], natmul[nat[x], y]], 
            natadd[natexp[succ[nat[x]], y], 
              natmul[nat[x], natexp[succ[nat[x]], y]]]], 
          not[member[natmul[nat[x], y], natexp[succ[nat[x]], y]]]], 
        t -> y] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

The variable y can now be removed:

Map[equal[V, #] &, 
      SubstTest[class, y, 
        implies[and[member[y, omega], member[y, z]], member[succ[y], z]], 
        z -> image[
            fix[composite[inverse[NATEXP], 
                inverse[IMAGE[inverse[times[nat[x]]]]], E, SECOND]], 
            set[succ[nat[x]]]]]]

(% /. x -> x_) /. Equal -> SetDelayed

Applying induction, one obtains:

SubstTest[implies, INDUCTIVE[z], 
        subclass[omega, z], 
z -> 
          image[fix[
              composite[inverse[NATEXP], 
                inverse[IMAGE[inverse[times[nat[x]]]]], E, SECOND]], 
            set[succ[nat[x]]]]] // Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Restoring variables yields the result sought after:

SubstTest[implies, and[member[u, v], subclass[v, w]], 
        member[u, w], 
{u -> nat[y], v -> omega, 
          w -> 
            image[fix[
                composite[inverse[NATEXP], 
                  inverse[IMAGE[inverse[times[nat[x]]]]], E, SECOND]], 
              set[succ[nat[x]]]]}] // Reverse

member[natmul[nat[x_], nat[y_]], natexp[succ[nat[x_]], nat[y_]]] := 
      True

The nat wrappers can be removed:

SubstTest[implies, 
        and[equal[x, nat[s]], equal[y, nat[t]]], 
member[
          natmul[x, y], natexp[succ[x], y]], {s -> x, t -> y}] // 
      Reverse

or[member[natmul[x_, y_], natexp[succ[x_], y_]], 
        not[member[x_, omega]], not[member[y_, omega]]] := True

A variable-free formulation can be derived as follows:

fix[
        composite[inverse[E], IMAGE[inverse[NATMUL]], NATEXP, 
          cross[SUCC, Id]]] // RelnNormality

fix[
        composite[inverse[E], IMAGE[inverse[NATMUL]], NATEXP, 
          cross[SUCC, Id]]] := cart[omega, omega]