[CL] "Lambdas changed my life," Barbara Partee

[Chris Menzel]

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

-chris