"pull the rabbit out of the hat" via a simple presuppositions solver

[Darryl McAdams]

to extend my previous comments on presuppositions using fancy dependent types, I was thinking it might be possible to also handle sentences like "pull the rabbit out of the hat", and others like it by clever use of the presupposition solver mechanism I mentioned. before jumping to that, tho, it'd probably be good to talk about definites in general.

a first pass meaning for "the" might be something like this:

    the : (P : Entity → Prop) → {{x : Entity}} → {{px : P x}} → Entity

    the = λP. λ{{x}}. λ{{px}}. x

so the sentence

    John read the manual

would have a the meaning

    Read j (the Manual {{ ?0 }} {{ ?1 }})  =β=>  Read j ?0

after we fill in the holes for the presupposed components. the types for each hole being ofcourse

    ?0 : Entity

    ?1 : Manual ?0

now, if the discourse context is just this:

    b : Entity

    p : Manual b

then there is a unique solution for the holes: ?0 = b, ?1 = p. even if the context is this:

    b : Entity

    p : Manual b

    c : Entity

there is still a unique solution, because if we pick ?0 = c, there is no evidence that "Manual c" is true. however, if we add "p' : Book c" to the context, we're hosed: now there are two solutions -- two books in context -- so which do we pick? definites demand unique solutions.

Big Idea: maybe we need unique solutions _over all_? that is to say, for any set of holes, there must be only one possible substitution for it.

it might be possible to use the same mechanism to handle these rabbit sentences. if we consider just the imperative cases first, then it seems reasonable to say: because the sentence is imperative, the speaker is presupposing the possibility of performing the action. we might represent this as an operator with a possibility presupposition, perhaps something like this (using Poss in place of a diamond modality):

    IMP : (P : Prop) → {{p : Poss P}} → Command

then what we would have for the sentence will be something like

    IMP (PullOutOf addressee (the Rabbit {{?0}} {{?1}}) (the Hat {{?2}} {{?3}})) {{?4}}

    

    =β=> IMP (PullOutOf addressee ?0 ?2)

with the types

    ?0 : Entity

    ?1 : Rabbit ?0

    ?2 : Entity

    ?3 : Hat ?2

    ?4 : Poss (PullOutOf addressee ?0 ?2)

even if it turns out there are multiple solutions for ?0 and ?1 together, and maybe even fore ?2 and ?3 together (ie if there are multiple rabbits, and/or multiple hats), there will only be a unique solution for ?4 if there is exactly one rabbit in a hat. so: if it's necessary to have a unique solution for the collection of holes, then we can get these rabbit sentences to work. we can do something similar for "John pulled the rabbit out of the hat":

    DEC : (P : Prop) → {{p : P}} → Assertion

    DEC (PullOutOf j (the Rabbit {{?0}} {{?1}}) (the Hat {{?2}} {{?3}})) {{?4}}

    

    =β=> DEC (PullOutOf j ?0 ?2)

caution is required tho: this crucially depends on the idea that there is a difference between a proposition and a speech act. the P argument to DEC is necessarily a formal object (a type/prop in the type theoretic sense) that represents the idea in question. precisely as stated, the suggestion won't work, because Command and Assertion are presumably types/props too, but modifications to the logic could undoubtedly be make to distinguish linguistic propositions from type theoretic types/props. perhaps some sort of universe construction?