> > Jack Campin - bogus address schrieb:

> > >> Does anybody know a simple book on combinatory logic?

> > >> I read Smullyans "how to mock a mockingbird" is interesting but is a
> > >> bit to much about combinators and not a lot about where it is good for
> > >> or how you can use it.

> > >> Or is the subject matter just to difficult for an simple book?

> > > Hindley and Seldin, Introduction to Combinators and {\lambda}-calculus,
> > > Cambridge 1986.

> > >> Am primarily interested how to "simulate" First order logic (predicate
> > >> logic with relations / FOL) in this logic.

> > > You can't.

> > Strictly speaking I would confirm, you can't.

> > But because combinatory logic corresponds to propositional
> > hilbert style proofs with some axioms (Watch out this
> > is not the usual curry howard isomorphism which is between
> > typed lambda calculus and intuitionistic logic. We
> > are not dealing with typed lambda calculus here, but
> > with untyped combinatory logic).

> > And because choosing the right axioms, and thus the
> > right combinators, yields classical logic. I would
> > say combinatory logic yields at least propositional
> > logic. The question is now how we could make the step
> > to predicate logic, that is replace propositional
> > variables by prime formulas, and allow quantifiers.

> > What FOL rules would you like to give a combinatorial
> > term? If you tell us what FOL rules you are interested
> > in, then maybe we can give you further hints. Will
> > you stick to hilbert style proofs?

> > Best Regards

> Thanks it is allready getting to complicated for me here.

> In Smullyans book i read that you can do arithmetic in Combinatory
> logic
> In schonfinkel;s article that you could do first order logic in it
> (article in from frege to Godel) the article does not go beyond
> nomadic FOL.
> found a reference to an article from Quine about it (but havent read
> that one yet)

> that is about how far i am.

> don't have the faintest idea what you mean by:
>  curry howard isomorphism
> typed lambda calculus
> untyped combinatory logic

> am also not  good in Hilbert style proofs

> Think i must look for another subject for an essay.

> I was thinking that you just could replace FOL with Combinatory logic
> to get rid of the distibnction between variables and predicates. and
> only have combinators.

> thanks anyway- Hide quoted text -

> - Show quoted text -