Question: When do a bunch of inferences comprise a proof of a proposition?
Answer: When that proposition can be derived by GMP from those inferences.

Today's lab works through an example to demonstrate this principle.


Recall the following C++ code for list concatenation:

vector<int> cat(vector<int> x, vector<int> y)
{
    if(x.empty())
        return y;
    if(! x.empty() )
        return cons(head(x),cat(tail(x),y));
}


In the absence of runtime errors (such as memory
overflow), the behavior of this code is characterized
by the following logic:


(c1)  cat([],y)=y
(c2) ~x=[] -> cat(x,y) = cons(head(x),cat(tail(x),y))

The following additional axioms characterize the behavior of
the primitive operations head, tail, and cons on lists, where x
ranges over lists of integers, and n ranges over integers.

(a1)   ~x=[] -> cons(head(x),tail(x)) = x
(a2)   tail(cons(n,x)) = x
(a3)   head(cons(n,x)) = n
(a4)   ~ cons(n,x) = []



Finally, we have the induction axiom which says that if P
is any property of lists (that is, a logical formula with
one free list variable x), and P holds for the empty list,
and P holds for any list whose tail satisfies P, then P
holds for all lists:

(a5) P([]) & (~x=[] ^ P(tail(x)) -> P(x) ) -> (for all x, P(x))

Now we state and prove:

Theorem: For any list x, cat(x,[]) = x.

Note this is not the trivial base case of cat because here
it is the 2nd argument that is [], rather than the first.

proof:

The proof is by list induction on the first argument of cat.
For the base case, consider the case where the 1st argument
is the empty list:


(1) cat([],[]) = []   (by c1).

For the induction step, suppose

(2) x is a nonempty list,
and
(3) cat(tail(x),[]) = tail(x).

Then

(4) cat(x,[]) = cons(head(x),cat(tail(x),[]))  (by 2,c2)
(5)           = cons(head(x),tail(x))          (by 3)
(6)           = x                              (by 2,a1)

So

(7) cat(x,[]) = x (by 4,5,6).

Now we have

(8) for any list x, cat(x,[]) = x. (by a5, 1, 2^3->7)

QED


The axioms and inferences assumed to be evident in this proof are as
follows:

A   c1
B   c1->1
C   c2
D   c2^2-> 4
E   3->5
F   a1
G   2^a1->6
H   4^5^6 -> 7
I   a5
J   a5^1^(2^3->7) -> 8

That is, these are the assumptions represented by the individual steps
of the argument. There is an additional implicit assumption: by purporting
to be a "proof" of 8,  the argument implicitly claims that these premises,
taken together, entail the conclusion 8. Today's lab exercise is to
derive 8 from the above by resolution, showing that this implicit
assumption is correct.

Here is a fully worked example to show what the answer may look
like:

Suppose some proof were to have inferences as follows:


A  1
B  1->2
C  3
D  3^4 -> 5
E  5 -> 6
F  2 ^ (4->6) -> 7

and purport to be a proof of 7. The following table shows
how 7 can be derived from propositions A through F. The first
column in the table is the name of the new derived proposition;
the second column is the formula for the new proposition, and the
third column is the pair of previous propositions resolved to
obtain the new proposition.


H  2          (A,B)
I  4->5       (C,D)
J  4 -> 6     (I,E)
K  (4->6)->7  (J,F)
L  7          (J,K)