Message-Id: <m0tLVLc-0000ZUC@xiron.pc.helsinki.fi>
Date:         Thu, 30 Nov 1995 18:34:33 -0800
Reply-To:     "John E. Clifford" <pcliffje@CRL.COM>
Sender:       Lojban list <LOJBAN@CUVMB.BITNET>
From:         "John E. Clifford" <pcliffje@CRL.COM>
Subject:      lambdas to the slaughter
To:           Veijo Vilva <veion@XIRON.PC.HELSINKI.FI>
Content-Length: 10554
Lines: 163

One (realllly big) reason for recommending McCawley was so *I* would not
have to write a piece about either lambda or abstractors, areas where I
feel my competence has waned markedly since the halcyon days with Montague
(et al) and Church and (via Hartmut Scharfe) Raghunatha Ciromani (Sanskrit
c, not Lojban but close). But I have just finally finished reading what I
can find of the lambda and related threads and it looks like the devil is
driving on that route.  (Before plunging in, I note that the discussion in
McCawley also has the most satisfying explanation -- in terms of ka and
anti-ka, as we shall say for now -- of how to deal with indirect
questions, another ancient blister.  I am, in keeping with my official
pose here -- do your homework before you come to class -- going to assume
that you have read, but been left more than partially puzzled by,
McCawley.)

First, lambdacation is totally general in logic: given any kind of
variable,x, and any kind of expression, P, you can make an expression
\x(P) (imagine the other leg of the lambda) which names a function
from things of the type of P.  In Lojban usage, we seem only to be using
the notion for functions where the variables are of type individual and
the expressions are of type sentence, giving lambda expressions of the
type predicate.  (Actually getting to that from what went before
involves some logical fancy footwork in which a predicate is actually a
function from an individual to a truth value, which is the referent of the
expression of type sentence.  To make matters worse, this function is
also identified with the extension of the predicate, set of things that
have the relevant property (as it were), i.e., for which the value of the
function is 1 or T (yes, fuzzy versions are possible).  All of this
simplifies the logic but makes connecting with real languages a bit of a
pain, since the things we most often talk about are just not there in
tangible form.)

In the strict form, lambda expressions are 1-place functions, so su'o-2-
place predicates have to be dealt with either by taking tuples as
arguments -- possible in logic and Lojban but requiring more complex
items in the various places -- or by admitting intermediate functions:
\x(\y(Fxy)) is a one-place function not to a truth value but to another
one-place function to a truth value (i.e., a function from an individual
to a predicate).  With a lot of care, we can however just write \xy(Fxy)
when we have right grouping strings and no intermediate applications
functions to arguments.  The arguments can then be written simply with
the same understanding: \xy(Fxy)(ab) is usually read as
(\x(\y(Fxy)(b)))(a), i.e., as Fab in these easy cases.  If Lojban were to
allow lambda expressions to be used freely (which it surely need not for
predicate types, since all that a lambda can do is more easily done with
various devices for constructing complex predicates, or just making
compound sentences, as the reduction above shows), we would
probably use the format a \xy(Fxy) b, again with the understanding that
the first insertable term goes in for the outermost variable and so on
rightward (other conventions are not unknown).  (The reason for having
something like a lambda expression for predicates, which always
comes out to be just the replacement version of the sentence inside, is
that lambda appeared first just as a device for figuring out what could
be substituted for the F's etc. in theorems of logic while preserving
theoremhood.  Other devices, simpler than lambdas, have since been
devised, though the original restrictions -- built into lambdas -- about
the order of replacement and the like have been preserved.  The trick of
using lambdas for moving around in the ramified theory of types, which
is what they are used for now, was an early discovery, more or less a
happy accident.)

In logic, all of this takes place within a single interpretation: list of
things there are, list of functions from things to truth values, assignment
of things to names -- a possible world in some very abstract sense,
which could be applied to a real world, a moment in our time, say. But
in logic there are lots of such interpretations.  For even minimal use for
dealing with natural languages we need at least one corresponding to
each moment of time and typically a lot more.  For simplicity(!) I
assume that we have all the interpretations that anyone can devise
available (in fact, I think we need more, since interpretations are
consistent and complete and that may cut off some things we want to
say, but we can fake across that bridge if the need arises).

So, an expression -- say the predicate F -- means/ refers to \xFx in each
interpretation, but what is that, i.e., what ordered pairs (set theoretical
definitions) or what mapping of things into {0,1} (or even [0,1]) is that
in a given world.  The answer is given by appeal to the property which
F means/designates, F's sense, not its extension in a particular world.
This is an intensional notion, but western logic treats it in an
extensional way (again depriving us of the thing we were looking for by
giving us something that does its work): the intension of F is another
function, this one from interpretations (worlds) onto the set of functions
in that world (things cross truth values, for predicates).  So, as
expected, knowing the sense of F allows us to pick out the Fs in any
world (provided we know what world we are in, at least), though the
logic version does not provide the usual kind of explanation of why it
works (i.e., no definitions, lists of essential properties, or whatever).
(This is successful but wrongheaded reconstruction with a vengeance,
but it does keep the kinds of entitites down: all abstractions are the
same sorts of thngs, sets -- or, strictly, functions -- so the usually
distinct notions, betwen abstract extensional entities, like numbers and
sets, and abstract intensional ones like properties is removed -- or
cleverly papered over.)

So the referent of "in\xFx" (or "^\xFx," "intension of "or "cap of" or "up
of" -- I prefer the last) is a function on worlds (its intention is a
constant function, since the sense of an expression does not depend upon
what world it is checked in).  That sounds like a thing and so, in Lojban,
we would expect to be repesented by a sumti, as is everything else except
predicates predicating, i.e., \xFx itself.  But, the nearest thing
directly to up in Lojban is _ka_, which forms predicates from lambda
predicate expressions (though not until now expressed as such), predicates
which yield true only for up of the enclosed predicate.  As predicates
they are pretty useless (as And -- I think it was (the nested quotes get
hard to follow) -- noted), since the only safe claim is that the _lo_ form
of this predicate has the property.  Or they could be used for claiming
that some other _lo ka_ was also the sense of the enclosed predicate,
though identity almost always seems more normal for this.  The direct
correlate of up is the derived sumti, _lo ka_ (note, despite our habit,
not _le ka_, veridicality is essential and selection is never an issue --
oh, well, I guess we could use _le_ for wild stabs not guaranteed to be
right).

The other side of up is, of course, down (cup, extension exP or vP -- I
mean an inverted caret -- for intensional P).  For this we have the not
surprising  rule that v^P = P, in particular, that v^\xFx is just \xFx.  The
down of an intensional object in any world is just the value of that
intensional object (= function on worlds) for that world, whence the
above principle follows.  So, for the (lo) ka's of Lojban, the down
would get back to the embedded lambda expression.  I am not sure
whether  Lojban has a down as such, nor what it would be like.  What it
does have is a complex, the application of the down to appropriate
arguments, this obtained by using ckaji.  That is, a ckaji lo ka \xFx
translates to (v^ \xFx)(a) (some obvious parentheses omitted), i.e., to
(\xFx)(a), so Fa.  But nothing in here corresponds directly to v^\xFx,
nor does there seem to be any need for it when dealing with properties
(and what would we get: another sumti or a predicate? presumably the
latter as we do not have a sumti form for \xFx, which is what we get
down to.)  And, by the way, for the ka sort of intentional objects, P, ^vP
= P.

But up (whether _ka_ or not) works for anything, so that we can: we
can up a sumti or a sentence as well as a predicate, to find out what the
sumti refers to in each world or whether the sentence is true, individual
concepts (haeceities? vishecas(? -viceshas?)) and propositions (sumti
and sentences are both  zero-place functions -- constants, with idivudals
or truth values as values).  And there are other intensional objects that
are not the intensions of obvious sorts of expressions, but still pick out
interesting things world by world. One of these is the suggested indirect
questions, which picks out the right answer or at least the right
proposition in each world. So the referent, it is said, of "whether Bill is
coming" in worlds where he is is the proposition that Bill is coming and
in worlds where he is not is the contradictory propositions, that he is
not coming.  So, to know whether Bill is coming is just to either know
that he is coming (if he is) or that he is not coming (if he is not).  Right
result, surely.  But notice that, for this W, vW is one or the other of the
propositions ^Bill is coming or ^Bill is not coming, either of whose up
is just a constant function which gives that proposition in all worlds, so
^vW is not the same as W.  (The consequences of this for Lojban are
obscure: kau seems to be some sort of intensional operator remotely
related to up -- but definable by lambda in its full force.)
Events (and inviduals -- as opposed to individual segments, to please
xorxes) are also intensional at least in the sense that they strictly
involve things from different worlds assembled for inspection at once. I
don't quite know how to work the details out (I haven't spent much time
on it, nor have others that I can get my hands on).  Strict Buddhist  and
Humeans would say, of course, that there is no individual, only down of
the individual concept in each world, and it does seem we could do
anything we wanted to do with individuals using just that.  Events seem
harder, since event their slices are not readily perceived in all this.
Remember that this is all a model to calculate how things work, it is not
the way the
world is.
pc>|83