Raymond Smullyan's EFS and the Formalization of Combinatory Logic
Author Message
Raymond Smullyan's EFS and the Formalization of Combinatory Logic

Hello,

I have been rereading portions of Raymond Smullyan's beautiful
book "Diagonalization and Self-Reference". In particular, I reread
the chapter on Elementary Formal Systems (EFS) and also the chapter
on a formal system for Combinatory Logic. In the following, I have
come up with a representation (in EFS) of his formalization of
Combinatory Logic.

1) I would like feedback from the readers as to the correctness of
my EFS "program" to generate the theorems of Combinatory
Logic.

2) Also, how would a formalization of CL be represented using Horn
clauses?

--------------------------------------------------------------------

Alphabet = {(, ), S, K, =}

Predicate symbols = {Term, Axiom, Theorem}

-------

Term [S].
Term [K].
Term [x]->Term[y]->Term[(xy)].

Term[x]->Term[y]->Term[z]->Axiom[((Sx)y)z=(xy)(xz)].
Term[x]->Term[y]->Axiom[(Kx)y=x].
Term[x]->Axiom[x=x].

Axiom[x]->Theorem[x].
Theorem[x=y]->Theorem[y=x].
Theorem[x=y]->Theorem[y=z]->Theorem[x=z].
Theorem[x=y]->Term[z]->Theorem[xz=yz].
Theorem[x=y]->Term[z]->Theorem[zx=zy].

END

Regards,

Bill Halchin

Sent via Deja.com
http://www.*-*-*.com/

Tue, 17 Jun 2003 14:20:29 GMT
Raymond Smullyan's EFS and the Formalization of Combinatory Logic

Quote:

> Alphabet = {(, ), S, K, =}

> Predicate symbols = {Term, Axiom, Theorem}

> -------

> Term [S].
> Term [K].
> Term [x]->Term[y]->Term[(xy)].

> Term[x]->Term[y]->Term[z]->Axiom[((Sx)y)z=(xy)(xz)].
> Term[x]->Term[y]->Axiom[(Kx)y=x].
> Term[x]->Axiom[x=x].

> Axiom[x]->Theorem[x].
> Theorem[x=y]->Theorem[y=x].
> Theorem[x=y]->Theorem[y=z]->Theorem[x=z].
> Theorem[x=y]->Term[z]->Theorem[xz=yz].
> Theorem[x=y]->Term[z]->Theorem[zx=zy].

> END

I suppose I shouldn't complain since Prolog uses a ',' for seperating items
in a list and for conjunction, but what does '->' mean?

Geoff

Thu, 19 Jun 2003 01:35:50 GMT

 Page 1 of 1 [ 2 post ]

Relevant Pages