LC PROGRAM - THEOREM PROVING IN COMBINATORY LOGIC

Example : reflexivity axioms for I, K and S :
(You type "d 1 A = I I", the program displays "d 1: A = I I -> I = I.")

$ ./lc55
Demonstration de theoremes de logique combinatoire
d 1 A = I I
d 1: A = I I -> I = I.
d 2 A = K K
d 2: A = K K -> K = K.
d 3 A = S S
d 3: A = S S -> S = S.


Application of proof 2 to proof 1 : reflexivity for K I :

d 4 a 2 1
d 4: a 2 1 -> -KI = -KI ; (K I) = (K I).


Extensionality for a symbol x:

d 5 A = x x
d 5: A = x x -> x = x.


Application of axiom defining I to x

d 6 I 5
d 6: I 5 -> -Ix = x ; (I x) = x.


Apply symmetry to proof 6 :

d 7 s 6
d 7: s 6 -> x = -Ix ; x = (I x).


Apply x to itself :

d 8 a 5 5
d 8: a 5 5 -> -xx = -xx ; (x x) = (x x).


Reflexivity for y:

d 9 A = y y
d 9: A = y y -> y = y.


Substitution : (^x (x x)) y = y y :

d 10 ^ 5 8 9
d 10: ^ 5 8 9 -> ---^x-xxy = -yy ; (((^ x) (x x)) y) = (y y).


Reduce I x to x :

r -Ix
d 501: I 5 -> -Ix = x ; (I x) = x.


Reduce S K K x to x :

r ---SKKx
d 505: t 502 504 -> ---SKKx = x ; (((S K) K) x) = x.


Save the proofs to file test.lcs :

s test.lcs


Quit the program and see the produced proofs :

q
$ cat test.lcs
d 1: A = I I -> I = I.
d 2: A = K K -> K = K.
d 3: A = S S -> S = S.
d 4: a 2 1 -> -KI = -KI ; (K I) = (K I).
d 5: A = x x -> x = x.
d 6: I 5 -> -Ix = x ; (I x) = x.
d 7: s 6 -> x = -Ix ; x = (I x).
d 8: a 5 5 -> -xx = -xx ; (x x) = (x x).
d 9: A = y y -> y = y.
d 10: ^ 5 8 9 -> ---^x-xxy = -yy ; (((^ x) (x x)) y) = (y y).
d 501: I 5 -> -Ix = x ; (I x) = x.
d 502: S 2 2 5 -> ---SKKx = --Kx-Kx ; (((S K) K) x) = ((K x) (K x)).
d 503: a 2 5 -> -Kx = -Kx ; (K x) = (K x).
d 504: K 5 503 -> --Kx-Kx = x ; ((K x) (K x)) = x.
d 505: t 502 504 -> ---SKKx = x ; (((S K) K) x) = x.


You can put all the input commands in a file, for example test.lci :

$ cat test.lci
d 1 A = I I
d 2 A = K K
d 3 A = S S
d 4 a 2 1
d 5 A = x x
d 6 I 5
d 7 s 6
d 8 a 5 5
d 9 A = y y
d 10 ^ 5 8 9
r -Ix
r ---SKKx

... and load this file :

$ ./lc55
Demonstration de theoremes de logique combinatoire
l test.lci
d 1: A = I I -> I = I.
d 2: A = K K -> K = K.
d 3: A = S S -> S = S.
d 4: a 2 1 -> -KI = -KI ; (K I) = (K I).
d 5: A = x x -> x = x.
d 6: I 5 -> -Ix = x ; (I x) = x.
d 7: s 6 -> x = -Ix ; x = (I x).
d 8: a 5 5 -> -xx = -xx ; (x x) = (x x).
d 9: A = y y -> y = y.
d 10: ^ 5 8 9 -> ---^x-xxy = -yy ; (((^ x) (x x)) y) = (y y).
d 501: I 5 -> -Ix = x ; (I x) = x.
d 505: t 502 504 -> ---SKKx = x ; (((S K) K) x) = x.
q
$