User:Magnap/Inquisitive Semantics Proposal
Inquisitive semantics provides a framework that we can use to give well-defined and reasonable semantics to questions (both direct and indirect) in Toaq.
Background
In inquisitive semantics, rather than being subsets of all possible worlds (of type ), propositions are taken to be nonempty sets of subsets of all possible worlds (of type ), downward closed under containment (meaning that, for some proposition , if , then for all , ). In other words, they are specially-structured sets of what we are used to thinking of as propositions. On the basis of this idea of a proposition, a semantics for first-order logic can be built, that, if we take truth for a proposition to be , is extensionally equivalent to classical predicate logic.
For an explanation of this semantics (which will unfortunately be necessary to understand this proposal unless or until I repeat some of the exposition here), see the book chapter "A first-order inquisitive semantics". An important thing to bear in mind about inquisitive semantics is that it does not give us a Boolean algebra, but only a Heyting algebra, meaning that is not guaranteed. In fact, the non-inquisitive projection operator is just . Note that this dramatically increases the number of distinct logical connectives (please don't be foreshadowing...).
TODO proposal broad strokes
Lift Toaq's current first-order truth-conditional semantics into first-order inquisitive semantics.
TODO proposal specifics
Show how and can be used to build a good semantics for questions, such as with and hí variants for exhaustivity. Do we end up needing the completeness operators? For embedded clauses only or also main clauses?