TRC Basic Axioms

Below are the basic axioms of TRC [2].

list(usable).

a(k(x),y) = x.

a(p1,pair(x,y)) = x.
a(p2,pair(x,y)) = y.

a(pair(x,y),z) = pair(a(x,z),a(y,z)).

pair(a(p1,x),a(p2,x)) = x.

a(a(a(abst,x),y),z) = a(a(x,k(z)),a(y,z)).

x != y | a(eq,pair(x,y)) = p1.
x  = y | a(eq,pair(x,y)) = p2.

x = y | a(x,noteq(x,y)) != a(y,noteq(x,y)).

p1 != p2.

end_of_list.

The first clause says that for every object, there is a corresponding constant function. The next two assert the existence of a pairing function (which is not a combinator) and projections (which are combinators). The fourth clause describes how a pair behaves as a function. The fifth clause says that everything is a pair, and together with the fourth implies that pair(p1, p2) is an identity combinator, in fact the identity combinator if we also consider the axiom of extensionality below. The sixth clause defines the action of the combinator abst which provides stratified combinatory completeness. The seventh and eighth clauses postulate the existence of eq, the characteristic function of equality. The ninth clause uses a skolem function noteq to express the axiom of extensionality, which says that if two combinators represent the same function, that is, given identical inputs they always produce identical outputs, then they are equal. The last clause precludes a trivial universe consisting of a single combinator.

At the outset I added some redundant versions of some of the above axioms in the hope that they would help OTTER to find proofs. The following two clauses follow so immediately from the above that we do not bother including the one-line OTTER proofs.

list(usable).
p2 != p1.
a(eq,pair(x,x)) = p1.
end_of_list.

Because the pairing function is surjective, anything that can be said about pairs can be recast into an equivalent statement about the projections, and vice-versa. In the following two clauses, I restate the definition of eq in terms of projections.

list(usable).
a(p1,x) != a(p2,x) | a(eq,x) = p1.
end_of_list.

Proof of a(p1,x) != a(p2,x) | a(eq,x) = p1. | OTTER output file

list(usable).
a(p1,x) = a(p2,x) | a(eq,x) = p2.
end_of_list.

Proof of a(p1,x) = a(p2,x) | a(eq,x) = p2. | OTTER output file

up show outline