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

[Fabian Neuhaus]

On Aug 26, 2005, at 2:43 PM, Chris Menzel wrote:

> On Fri, Aug 26, 2005 at 01:52:10PM -0400, Fabian Neuhaus wrote:
>>> I'm not sure why you're saying that, Pat, familiar as you are with 
>>> the
>>> Henkin stuff.  Seems to me that all we would need to do, initially,
>>> anyway, is add the usual "second-order" constraint that every formula
>>> defines an n-place relation:
>>>
>>>  (exists (F)
>>     (forall (x1 ... xn)
>>>      (iff (F x1 ... xn) A)
>>>
>>> where A is any formula
>>
>> Chris, are you sure that you can use _any_ formula? Would that not
>> lead to paradoxes?
>>
>> Obvious candidates are:
>> (a)
>>    (exists (F)
>>      (forall (x1 )
>>       (iff (F x1) (not (F x1)))
>>
>> and the classical Russell paradox
>> (b)
>>    (exists (F)
>>      (forall (x1 )
>>       (iff (F x1) (not (x1 x1)))
>
> Sorry, yes, of course, the standard restriction here is that "F" cannot
> occur free in A.
>
> As for the second example, I (inappropriately and inexplicably) had 
> only
> traditional second-order languages in mind in my response to Pat, but
> CL's wild west syntax requires further qualifications and restrictions
> still.   An obvious one is that none of the xi can occur free in
> predicate position in A.  But even this is not enough, as you can still
> get the following version of Russell in CL:
>
> (c)
>
>    (exists (F)
>      (forall (x)
>              (iff (F x)
>                   (exists (G) (and (= G x) (not (G x)))))))
>

Of course you could forbid to use x in predicate position AND forbid 
the use of identity in A. If I remember correctly,
Cocchiarella discusses this possibility. If one considers identity as 
an operator and not as binary relation, then one might argue that this 
solution is not completely arbitrary.  This way one  can avoid the 
paradox, however one still get something very ugly:
We just replace the identity by indiscernability.
    (exists (F)
      (forall (x)
              (iff (F x)
                   (exists (G)
			(and (not (G x)
				(forall (H)
					(iff (HF)(HG)) )))))))

(This looks like a paradox, but it is harmless, since Leibniz Law does 
not hold in CL.)

By the way,  if one embraces this formulation of the comprehension 
principle, then one cannot add an axiom of extensionality and the an 
axiom that postulates: If x has the property P, then P has the property 
of being a property of x.


> Equivalently, if we have lambda terms, we can get the following version
> of the Russell property:
>
>   [lambda (x) (exists (G) (and (= G x) (not (G x))))],
>
> and hence, with lambda conversion, essentially the same paradox.

Since John would like lamdas in CL (or rather an extension of CL) I see 
two possible solutions.
(A) Syntactical restriction: Take a restricted version  of the 
comprehension principle (like the one suggested above) as an addition 
axiom and allow lamda operators to apply only to formulas which meet 
the restriction. According to this solution [lambda (x) (exists (G) 
(and (= G x) (not (G x))))] is not well-formed.

(B) Semantic solution: Allow arbitrary lamda constructions, but some of 
these (like [lambda (x) (exists (G) (and (= G x) (not (G x))))]) do not 
refer. This would be a kind of free logic for lamda expressions. From a 
theoretical point of view this is the much more interesting solution, I 
always wanted to develop it. Unfortunately I cannot convince Barry that 
this kind of research is really important for biomedical ontologies. :)