As for and:
You got your lambda term for and wrong. Either you mean coordination between subject DPs ("Mary and John sneeze") then your lambda term is λP[λx[λy[P(x)^P(y)]]]
, with just one predicate P (not Q). Or you mean a coordination between VPs ("Mary sneezes and coughs"), then your lambda term is λPλQ[λx[P(x)^Q(y)]]]
(with an abstraction for a second predicate Q but just one abstraction for an individual variable x). I assume you meant λP[λx[λy[P(x)^P(y)]]]
, which is of type ((e,t),(e,(e,t)))
: Put in a one-place predicate, then an individual, then another individual, get out a truth value.
Also, you got the sneezing wrong: The term is λx[sneeze(x)]
, not λx[sneeze](x)
; the application to x is part of the scope of the lambda abstraction, not outside of it.
To avoid confusion with the variable x
, we can (but don't have to) rename the bound variable x
to, say, u
, and get λu[sneeze(u)]
with the exact same meaning.
So for the sentence "John and Mary run", you simply apply your and term to each of the terms you abstract for:
and sneeze mary john
≡ (λP[λx[λy[P(x)^P(y)]]])(λu[sneeze(u)])(m) (j)
((e,t),(e,(e,t))) (e,t) (e) (e)
> (λx[λy[(λu[sneeze(u)])(x)^(λu[sneeze(u)])(y)]])(m)(j)
(e,(e,t)) (e)(e)
> (λx[λy[sneeze(x)^sneeze(y)]])(m)(j)
(e,(e,t)) (e)(e)
> (λy[sneeze(m)^sneeze(y)])(j)
(e,t) (e)
> sneeze(m)^sneeze(j)
(t)
Here I chose to first simplify the two redexes (λu[sneeze(u)])(x)
and (λu[sneeze(u)])(y)
to sneeze(x)
and sneeze(y)
before continuing with the applications to m
and j
, but one could do it the other way round as well and get the same result (In lambda calculus, the order in which you choose to perform your reductions never matters, eventually any two computation paths will yield the same end result):
and sneeze mary john
≡ (λP[λx[λy[P(x)^P(y)]]])(λu[sneeze(u)])(m) (j)
((e,t),(e,(e,t))) (e,t) (e) (e)
> (λx[λy[(λu[sneeze(u)])(x)^(λu[sneeze(u)])(y)]])(m)(j)
(e,(e,t)) (e)(e)
> (λy[(λu[sneeze(u)])(m)^(λu[sneeze(u)])(y)])(j)
(e,t) (e)
> (λu[sneeze(u)])(m)^(λu[sneeze(u)])(j)
(t)
> sneeze(m)^sneeze(j)
(t)
The lambda reduction for and between VPs works quite similarly:
and sneeze cough mary
≡ (λP[λQ[λx[P(x)^Q(x)]]])(λu[sneeze(u)])(λv[cough(v)])(m)
((e,t),((e,t),(e,t))) (e,t) (e,t) (e)
> ... (absorb sneeze for P)
> ... (absorb cough for Q)
> ... (absorb mary for x)
> ... (simplify)
> sneeze(m)^cough(m)
(t)
As for your proposal for the quantified DPs, I don't quite understand your notation λx[2x^COOKIE (et,t)
- how is 2x^something
defined? I assume you mean something like "Tgere are two x'es and these x'es are cookies", but this is not very nice:
For your individual variable x one individual goes in, and that's what your term will be applied to - one individual. By just prepending a "2" in front of the variable you don't magically duplicate the amount of entities involved - it's still just one individual that goes in, syntacically and semantically.
Furthermore, you missed the application to the variable x
in your predication: cookie(x)
- not just cookie
.
In general, quantifiers are always a bit difficult to formalize, so don't worry if you're struggling.
"All", "some", "no" etc., can be modeled via ∃ and ∀, but for absolute numbers it gets difficult.
"Exactly one" can be formalized as follows:
exactly one: λP[λQ[∃x[∀y[P(y) <-> y=x] ^ Q(x)]]]
For a quantifier like "at least two", you can simply do three existential quantifications, have a conjunction of predicates applying to all the elements separately and then making sure that the variables stand for distinct entities:
at least two: λP[λQ[∃x1∃x2[P(x1)^P(x2)^x1≠x2^Q(x1)^Q(x2)]]]
You already see that this can get quite annoying if you have higher numbers or something more complex like a combination with a VP.
You can then combine the two tricks to get something like "exactly two" - again, the formula blows up even more:
exactly two: λP[λQ[∃x1∃x2∀y1∀y2[P(y1)<->x1=y1 ^ P(y2)<->y2=x2 ^ x1≠x2 ^ Q(x1) ^ Q(x2)]]]
"At most" can be achieved by adding negated existential statements ("there are no 3 distinct entities such that P applies to all of them").
Anything else is even more difficult. In particular, quantifiers like more than or most can not be defined with a first-order formula at all. So you'd probably want a different mechanism anyway.
A possibility is to model generalized-quantifiers via comparison between sets:
no is a relation between to sets X and Y such that they have no elements in commen (their intersection is empty).
at least one is a relation between to sets X and Y such that they have at least one element in common (their intersection is non-empty, or has cardinality (= size) >=1). all is a relation between to sets X and Y such that all elements which are in X are also in Y, i.e., X is a subset of Y (X ⊆ Y).
two is a relation between two sets X and Y such that their intersection is of size 2.
So two could be defined as
two: λP[λQ[|P∩Q| = 2]].
It's now debatable whether sets (which is what goes in here) is the same as predicates (which is what you'd normally want for VPs and NPs). When taking P for "cookie" and Q for the predication about these cookies, what the quantifier expresses is "The intersection between the things that are cookies and the things that Daniel and Nina ate is two", i.o.w., "There are exactly two entities which were eaten by Daniel and Nina and are coookies". (You actually have a semantic ambiguity here - did Daniel and Nina eat two cookies each, or two in total? Each of the two readings would have a different representation.)
In any case, a quantifier will be of type ((e,t),((e,t),t))
:First a one-place predicates (or sets) go in; this will yield a quantified DP like "two cookies" of type ((e,t),t)
as desired, because this is the usual type for quantified DPs. When we then put in another predicate, we get out a sentence with a truth value.
The way this notation of "two" works means that you effecively quantifier-raise, because your topmost operation will be the quantification, which comes from the DP in object position.
The other proposal would be to type-shift the verb, which expects two inputs of type e
, to a different type such that it can absorb a quantified DP of type ((e,t),t)
:
eat: (e,(e,t)) --> (((e,t),t),(e,t))
This works well from a type-theoretic perspective, and can be represented in set notation, for example as outlined e.g. here and here. However, it is not clear what the resulting lambda term would look like, because you would have to allow the predicate eat
two take an argument which is not an indidual but some complex lambda term that represents a quantified DP, and this would simply be no longer predicate logic.
In conclusion: Quantifiers are difficult. Representing them as generalized quantifiers by set-theoretic means is the easiest; in this case, they will be relatiions between sets, i.e. lambda terms of the form λP[λQ[some relation between P and Q]]
and type ((e,t),((e,t),t))
.