running the kernel through Omega - first complete inductive proof in Llambda

38 views

Skip to first unread message

Mark Tarver

unread,

Jun 9, 2017, 11:16:17 AM6/9/17

to Shen

Just concluded the first completed inductive proof in Ll - the associativity of append in 63 steps. The new book records (page 66)

Step 1 [1]

>> [all A : type
    [all x : [list A]
      [all y : [list A]
        [all z : [list A] [[append x [append y z]]
                            = [append [append x y] z]]]]]]

> (omega append)

The first step is to draw into the proof the relevant axioms from K_{W .}There are two which relate to append. We use (omega append) to draw these axioms into the proof. The next step is to eliminate the quantifiers in the conclusion. We eliminate the outer quantifier by a step of allr.

Step 2 [1]

>> [all A : type
    [all x : [list A]
      [all y : [list A]
        [all z : [list A] [[append x [append y z]]
                            = [append [append x y] z]]]]]]

1. [all x : type [all y : [list x] [[append [] y] = y]]]
2. [all x : type
     [all y : [list x]
       [all z : [list x]
          [all x1 : x [[append [cons x1 z] y]
              = [cons x1 [append z y]]]]]]]

> (allr a)

and several pages later.

The result is a proposition of the form (x = x) which is solved by =r.

Step 63 [1]

>> [[cons &&y1 [append [append &&x &&y] &&z]]
      = [cons &&y1 [append [append &&x &&y] &&z]]]

1. [[append &&x [append &&y &&z]]
        = [append [append &&x &&y] &&z]]
2. [all z : [list &&a]
     [[append &&x [append &&y z]]
        = [append [append &&x &&y] z]]]
3. [&&y : [list &&a]]
4. [all y : [list &&a]
     [all z : [list &&a]
       [[append &&x [append y z]]
              = [append [append &&x y] z]]]]
5. [&&x : [list &&a]]
6. [&&y1 : &&a]
7. [&&a : type]
8. [&&z : [list &&a]]

> =r

K_{W .}is the set of Ll propositions derived by running the kernel definitions of key system functions through W. So far I've generated 29 axioms from the kernel though the final tally will be larger.