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?
Am primarily interested how to "simulate" First order logic (predicate logic with relations / FOL) in this logic.
(smullyan at the end of his book goes into arithmetic but i am loking for FOL)
> 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.
============== j-c ====== @ ====== purr . demon . co . uk ============== Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760 <http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975 stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
<bo...@purr.demon.co.uk> wrote: > > 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.
thanks will have a look to that
> > Am primarily interested how to "simulate" First order logic (predicate > > logic with relations / FOL) in this logic.
> You can't.
I thought if it is strong enough for arithmetic it must be strong enough for Fol.
or is it only strong enough for nomadic Fol (for without relations) this is a bit ruining my plans.
>> 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?
> >> 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.
> On Dec 9, 2:48 pm, Jan Burse <janbu...@fastmail.fm> wrote:
> > 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 -
Did read
Variables Explained Away Willard V. Quine Proceedings of the American Philosophical Society, Vol. 104, No. 3. (Jun. 15, 1960), pp. 343-347.
And that does "full" FOL in combinatory logic. (First order Logic including relations)
But it is hopelessly complicated. and i am wondering about his major inversion Inv combinator.
> On Dec 9, 6:40 pm, translogi <wilem...@googlemail.com> wrote: >> On Dec 9, 2:48 pm, Jan Burse <janbu...@fastmail.fm> wrote: >>> 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.
>> 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 > Did read
> Variables Explained Away > Willard V. Quine > Proceedings of the American Philosophical Society, Vol. 104, No. 3. > (Jun. 15, 1960), pp. 343-347. > And that does "full" FOL in combinatory logic. (First order Logic > including relations) > But it is hopelessly complicated. > and i am wondering about his major inversion Inv combinator.
I am still confident that one can develop combinatorials for proofs of FOL, and this is what is more in the focus of my interest. Think this runs under the heading of *calculus of construction*, but I didn't find a reference right now. Maybe can provide you one in a next post.
Combinatorials for proofs will also turn the prime formulas into variable less formulas, and that is what I see manifest in the papers above. Maybe its better to direct this process in a special way by the quine/ bernays/jaeger approaches for set theory, instead of having a general FOL approach and then stepping into set theory.
I am not so sure about the advantages and disadvantages.
> Variables Explained Away > Willard V. Quine > Proceedings of the American Philosophical Society, Vol. 104, No. 3. > (Jun. 15, 1960), pp. 343-347.
> And that does "full" FOL in combinatory logic. (First order Logic > including relations)
> But it is hopelessly complicated. > and i am wondering about his major inversion Inv combinator.
If you do not involve set theory and when you are not interested in a proof theory, but only expressing formulas without variables. Then you can go along as follows:
The SKI conversion needs only be applied to expressions of the form lambda x.t.
Prime formulas do not have this form, so they stay as they are. Although they might include variables. These variables are later removed, when they are bound by quantifiers. The function symbols in the prime formulas are simply treated as new combinatorial constants and the variables as variables.
Example:
p(f(x),y) corresponds to (p (f x) y)
What remains are formulas which have the prime formulas in their leafs and conjunctions and quantifiers in the nodes. We should fix a set of junctions and quantifiers we would like to work with. Lets assume we restrict ourselfs to the following:
Now we introduce combinatorial constants for our set of junctions and quantifiers:
~A := (NEG A) A & B := (AND A B) exists x A := (EXISTS (lambda x.A))
The existential quatifier introduces a lambda abstraction which can be removed via the SKI combinatorials, which will also remove the x inside the quantified formula A.
Example:
forall y(q(y) -> p(y))
==
~exists y(q(y) & ~p(y))
==
(NEG (EXISTS (lambda y (AND (Q y) (NEG (P y))))))
== (*)
(NEG (EXISTS (S (S (K AND) (S (K Q) I)) (S (K NEG) (S (K P) I)))))
|
