Questions/Hamblin.lean

@cite{hamblin-1973b} @cite{karttunen-1977} @cite{kratzer-shimoyama-2002b} @cite{partee-rooth-1983} @cite{kratzer-shimoyama-2002}

Hamblin Semantics for Questions.

The Hamblin View

Questions denote sets of propositions - their possible answers. A question Q has type <<s,t>,t>, i.e., (W → Bool) → Bool.

This contrasts with G&S partition semantics where questions are equivalence relations. The Hamblin view is:

• More directly compositional (questions are the same type as GQs)
• Naturally conjoinable (type ends in t)
• Foundation for alternative semantics

Coordination

Since <<s,t>,t> is conjoinable, we can directly apply Partee & Rooth's generalized conjunction:

• Q₁ ∧ Q₂ = λp. Q₁(p) ∧ Q₂(p)
• Q₁ ∨ Q₂ = λp. Q₁(p) ∨ Q₂(p)

@[reducible, inline]

abbrev Semantics.Questions.Hamblin.QuestionDen (W : Type u_1) : Type u_1

Hamblin question denotation: a set of propositions (possible answers).

A question Q is true of proposition p iff p is a possible answer to Q. Type: <<s,t>,t> in Montague notation.

Equations

• Semantics.Questions.Hamblin.QuestionDen W = ((W → Bool) → Bool)

def Semantics.Questions.Hamblin.fromAlternatives {W : Type u_1} [BEq W] (alts : List (W → Bool)) (worlds : List W) : QuestionDen W

Construct a Hamblin question from a list of alternative propositions. A proposition p is an answer iff it matches one of the alternatives.

Equations

• Semantics.Questions.Hamblin.fromAlternatives alts worlds p = alts.any fun (alt : W → Bool) => worlds.all fun (w : W) => p w == alt w

def Semantics.Questions.Hamblin.polar {W : Type u_1} [BEq W] (p : W → Bool) (worlds : List W) : QuestionDen W

A polar question has two alternatives: p and ¬p

Equations

• Semantics.Questions.Hamblin.polar p worlds ans = ((worlds.all fun (w : W) => ans w == p w) || worlds.all fun (w : W) => ans w == !p w)

def Semantics.Questions.Hamblin.which {W : Type u_1} {E : Type u_2} [BEq W] (domain : List E) (pred : E → W → Bool) (worlds : List W) : QuestionDen W

A wh-question over a domain: "which x satisfies P?"

Equations

• Semantics.Questions.Hamblin.which domain pred worlds ans = domain.any fun (e : E) => worlds.all fun (w : W) => ans w == pred e w

def Semantics.Questions.Hamblin.conj {W : Type u_1} (q1 q2 : QuestionDen W) : QuestionDen W

Conjoin two question denotations. (Q₁ ∧ Q₂)(P) = Q₁(P) ∧ Q₂(P)

Semantically: P answers (Q₁ ∧ Q₂) iff P answers both Q₁ and Q₂.

Equations

• Semantics.Questions.Hamblin.conj q1 q2 p = (q1 p && q2 p)

def Semantics.Questions.Hamblin.disj {W : Type u_1} (q1 q2 : QuestionDen W) : QuestionDen W

Disjoin two question denotations. (Q₁ ∨ Q₂)(P) = Q₁(P) ∨ Q₂(P)

Semantically: P answers (Q₁ ∨ Q₂) iff P answers Q₁ or P answers Q₂.

Equations

• Semantics.Questions.Hamblin.disj q1 q2 p = (q1 p || q2 p)

instance Semantics.Questions.Hamblin.instAddQuestionDen {W : Type u_1} : Add (QuestionDen W)

Equations

• Semantics.Questions.Hamblin.instAddQuestionDen = { add := Semantics.Questions.Hamblin.conj }

instance Semantics.Questions.Hamblin.instHAddQuestionDen {W : Type u_1} : HAdd (QuestionDen W) (QuestionDen W) (QuestionDen W)

Equations

• Semantics.Questions.Hamblin.instHAddQuestionDen = { hAdd := Semantics.Questions.Hamblin.conj }

theorem Semantics.Questions.Hamblin.conj_comm {W : Type u_1} (q1 q2 : QuestionDen W) (p : W → Bool) : conj q1 q2 p = conj q2 q1 p

Conjunction of questions is commutative.

theorem Semantics.Questions.Hamblin.disj_comm {W : Type u_1} (q1 q2 : QuestionDen W) (p : W → Bool) : disj q1 q2 p = disj q2 q1 p

Disjunction of questions is commutative.

theorem Semantics.Questions.Hamblin.conj_assoc {W : Type u_1} (q1 q2 q3 : QuestionDen W) (p : W → Bool) : conj (conj q1 q2) q3 p = conj q1 (conj q2 q3) p

Conjunction is associative.

theorem Semantics.Questions.Hamblin.disj_assoc {W : Type u_1} (q1 q2 q3 : QuestionDen W) (p : W → Bool) : disj (disj q1 q2) q3 p = disj q1 (disj q2 q3) p

Disjunction is associative.

def Semantics.Questions.Hamblin.isAnswer {W : Type u_1} (q : QuestionDen W) (p : W → Bool) : Bool

A proposition p is a complete answer to Q if Q(p) = true.

Equations

• Semantics.Questions.Hamblin.isAnswer q p = q p

def Semantics.Questions.Hamblin.tautology {W : Type u_1} : W → Bool

The tautology answers every question vacuously (if in the denotation).

Equations

• Semantics.Questions.Hamblin.tautology x✝ = true

def Semantics.Questions.Hamblin.contradiction {W : Type u_1} : W → Bool

The contradiction answers no question.

Equations

• Semantics.Questions.Hamblin.contradiction x✝ = false

Hamblin vs Partition Semantics

The two views are related but not equivalent:

Hamblin: Q = {p | p is a possible answer} Partition: Q = equivalence relation where w ~ v iff same answer

A Hamblin question can be converted to a partition by taking the equivalence relation induced by the alternatives. Conversely, a partition can be viewed as a Hamblin question whose answers are the characteristic functions of its cells.

See Partition.lean for the G&S partition semantics.