[CL] "Lambdas changed my life," Barbara Partee
cmenzel at tamu.edu
Fri Aug 26 19:29:34 CDT 2005
On Fri, Aug 26, 2005 at 05:12:21PM -0700, Pat Hayes wrote:
> >I'm not sure why you're saying that, Pat, ...
> But since CL is type-free (unlike Henkin's version), this 'any
> formula' is a much larger set of possibles. And if we add lambda to
> the language, then it gets larger still. So even if we have this
> constraint for all current CL sentences, its still not obvious to me
> that we get the equivalent of adding lambda to CL.
Right, as I mentioned after being corrected by Fabian, I wasn't
distinguising clearly between CL and traditional second-order languages
in my first response -- though I still think we could add lambdas with
the right (extensional) semantics with care. As you note, though, you
are more concerned with the serious implications for the proof theory.
> >adding lamdba terms (recursively) to the definition of terms/formulas
> >is equivalent to this. We know from Henkin that you can provide a
> >so-called "general" model theory for this that is still semantically
> Its not the model theory that is bothering me so much as the proof
> theory. You say "A is any formula" quite casually above, but there
> isn't any way to axiomatize this in CL, so this has to be given flesh
> as an inference rule, and so the proof theory has lambda abstraction
> in it. This really does change the logic. Im not saying it couldn't be
> done (though Im not yet convinced it can be) but it does give you a
> different logic, since this kind of abstraction is not CL-valid at
> present. So its a significant change to the logic, is the main point.
Right, point taken.
> >Yes, it would certainly add a *lot* of stuff that a lot of people won't
> >want or use if they become a mandatory part of the language. As for the
> >proof theory, I don't think the *basic* changes would be all that
> >profound; all you'd need is lambda conversion:
> ALL?? This is a LOT.
As noted, I'm out of my depth here...
> This totally screws all known mechanical reasoners, just for a start,
> since it makes unification impossible and makes all tableau reasoner
> search spaces explode uncontrollably.
Right, as acknowledged previously, that's serious.
More information about the CL