Math Forum / Mathematics / Mathematical Logic / December 2008

Somehow, I think that "ain't" was really wanted in your peroration.

--
hz

Jack Campin - bogus address schrieb:

If I remember well, Hindley & Seldin waste a lot of time
which some looping issues in reduction, which was meanwhile
solved in the prepositional case by Dragalin....

A nice, and I would say even introductory book, is the following:
    Sorensen & Urzyczyn: Lectures on the Curry-Howard
    Isomorphism, Studies in Logic, Volume 149, 2006

Did not yet get hold of this one.

Bye

Jan Burse schrieb:

Oops, no there is some trick with a new operator H,
to avoid that. Oki Doki.

But anyway. We should recall church hypothesis, which
says that partial recursive, turning machines and
lambda calculus have the same strength!

So when somebody comes and tells you that combinatory
logic can do more ... I wouldn't buy that ...

The reasons for combinatory logic should be found
somewhere else. Here is my penny of thought, which
follows directly from the Howard-Curry Isomorphism:

   - They are attractive because they offer a
     medium to represent propositions
     and proofs (sic!).

Bye

You're Just Wrong.  It completely settles the issue.

It proves it for ALL generalizations that are relevant.
Please!
You need to think of this as analogous to the Universal Generalization
inference rule.  It essentiall proves it for AN ARBITRARY system.
Yes, in PA, you have to use the Chinese Remainder theorem, but
THAT IS NOT the point!  The point IS that the result NECESSARILY
holds FOR ANY system IN WHICH YOU CAN DO ARITHMETIC,
i.e., IN WHICH YOU CAN REPRESENT the system's own provablilty
predicate!

ANYthing worthy of the name of "logic" would HAVE to fall
within them.  YES, OBVIOUSLY, IF you can reprsent ANY lambda-
definable function, THEN OF COURSE you can represent the proof-
predicate; proof-predicates ARE PRIMITIVE-recursive!

And you (worse) said "fall within" as though you were trying to LIMIT
the power of the system!  It is precisely systems that Are MORE
powerful
than Peano Arithmetic that MUST (in virtue of that EXTRA power) be
incomplete!  It is systems that are LESS powerful that might THEREfore
hope to be complete (in the sense of being able to decide all their
sentences).
So what you MEANT to say was that you were not sure whether
combinatory
logic WAS ADEQUATE to those generalizations, whether it LIVED UP TO
those generalizations, NOT whether it "Fell within" them!

Combinators ARE NOT logic in any standard sense ANYway -- they are
TERM-REWRITING and reduction -- they are all about TERMS AS OPPOSED
to predicates or statements.   Even creating a SENTENCE (even an
EQUATION!)
out of combinators AT ALL is HARD and UNnatural!  What NATURALLY
happens
with combinators is reduction or evaluation, and THAT tragically
happens in
a language BEYOND that of combinators:
Kxy reduces to x, but "reduces to" is NOT a combinator!
More to the point, what is ACTUALLY MEANT here (in standard classical
FOL) is
Axy[ ((Kx)y)=x ], and "=" is NOT a combinator either, and Axy[ ] is
NOT a combinator
EITHER!
Finally, since you have to write the axiom "Sxyz reduces to xz(yz)"
WITH embedded
parentheses, you face the problem that "(" IS NOT A COMBINATOR EITHER.

This whole paradigm is so completely different from the standard
classical one
that even TRYING to bridge the gap is a waste of time.  But that does
NOT change
ANYthing about Godel's Theorem.  Godel's Theorem is VERY absolute.
It is a property of things with a certain POWER, a certain STRENGTH,
in the
realm of definability.  So it ABSOLUTELY NEVER matters whether the
system is
made of terms, predicates, combinators, sets, graphs, fool's gold,
green cheese,
or flying pigs: ALL that matters is HOW STRONG its powers of
definition are.
If they are strong enough then Godel's Theorem PROVES that  they are
not
complete.  If you can say "I am not provable" in the system, then NO
MATTER WHAT
it's made of, Godel's Theorem MUST apply.

The proof that Godel's theorem applies to combinators is actually the
so-called
"paradoxical combinator" or (less pejoratively) "fixed-point
combinator", usually
defined Y, which can return a fixed-point for ANY function,
(Yf=f(Yf) for all f),  INCLUDING both negation and unprovability,
which
is obviously inconsistent if you have completeness.  It is also
relevant for proving
that you can have recursive function definitions, which essentially
means
TM-equivalent power.

Here is a reference that I am sorry I could not quote:
http://books.google.com/books?id=7QQ5u-4tRUkC&pg=PA70&lpg=PA70&dq=%22paradoxical
+combinator%22+fixed+point+Y+incompleteness&source=bl&ots=PmeSeIe69q&sig=sUUtObB
2tfc97MU6YOe-RIEtIYQ&hl=en&sa=X&oi=book_result&resnum=2&ct=result#PPA71,M1