11 views

Skip to first unread message

Dec 8, 2007, 7:42:19 AM12/8/07

to

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)

Thanks

Dec 8, 2007, 8:28:36 PM12/8/07

to

> 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?

>

> 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

Dec 9, 2007, 7:39:06 AM12/9/07

to

On Dec 9, 1:28 am, Jack Campin - bogus address

<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.

<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.

Can you elaborate a bit on this?

Dec 9, 2007, 9:48:01 AM12/9/07

to

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.

>> 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

Dec 9, 2007, 1:40:31 PM12/9/07

to

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

Dec 15, 2007, 7:39:17 PM12/15/07

to

>

> - 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.

Dec 16, 2007, 6:21:18 AM12/16/07

to

translogi schrieb:

> 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.

>>

> 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

>> 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.

>

> 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.

This one?

http://www3.unifi.it/dpfilo/upload/sub/Didattica/Minari/varexplaw.pdf

This reminds of the "unpacking the axiom scheme of class

comprehension" for NBG.

http://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory#Unpacking_the_axiom_scheme_of_Class_Comprehension

Not sure whether one arrives at a *proof theory* for

FOL, but rather only (sic!) variable less *formulas* for FOL

and set theory.

Crucial to have variable less formulas for FOL is to

have a projection operator. An operator that sends

"A(x,y)" to "exists x A(x,y)".

You might like the following paper (see page 8):

http://www.iam.unibe.ch/til/publications/submitted

G. Jäger: Operations, sets and classes

E(f) = t <-> exists x(fx = t).

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.

Best Regards

Dec 16, 2007, 3:43:12 PM12/16/07

to translogi

translogi schrieb:

> 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.

> 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.

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:

~: negation

&: Conjunction

exists x: Existential Quantification

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)))))

== (**)

(NEG (EXISTS (S ((B AND) Q) ((B NEG) P))))

Best Regards

(*)

http://cs.wwc.edu/~aabyan/LN/PL/book/node108.html#lc:ski

http://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis

(**)

http://cs.wwc.edu/~aabyan/LN/PL/book/node109.html#ski:optim

http://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B.2C_C

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu