good book on combinatory logic - sci.logic

Message from discussion good book on combinatory logic

Jan Burse

View profile

More options Dec 16 2007, 12:21 am

Newsgroups: sci.logic

From: Jan Burse <janbu...@fastmail.fm>

Date: Sun, 16 Dec 2007 12:21:18 +0100

Local: Sun, Dec 16 2007 12:21 am

Subject: Re: good book on combinatory logic

  Forward
  | Print
  | View thread
  | Show original
  | Report this message
  | Find messages by this author
  

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.

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

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

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

Forward