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  
 
 [ 2 post ] 

 Relevant Pages 

1. HELP: Equational Logic & Combinatory Logic

2. Equational Logic & Combinatory Logic

3. Universal Algebra & Combinatory Logic

4. Universal Algebra, Model Theory & Combinatory Logic

5. Combinatory Logic

6. Combinatory Algebra/Logic

7. Illative combinatory logic

8. Reference to Eiffel GC in Eric Raymond's new book

9. Unix's Zoo of Languages (Eric Raymond)

10. Eric S. Raymond's newest writings

11. Formalization of object orientation

12. Logic Programming problems and 'benchmarks'

 

 
Powered by phpBB® Forum Software