structure Phenomena.Questions.WhComplement.ComplementPair : Type

A complement question pair: Q and its negated counterpart. Key observation: same partition, different required answers.

• positiveQ : String

  The positive question

• negativeQ : String

  The negative question

• domain : String

  Domain description

• satisfiers : List String

  Facts: who/what satisfies the predicate

• nonSatisfiers : List String

  Facts: who/what doesn't satisfy the predicate

• positiveAnswer : String

  Correct answer to positive question

• negativeAnswer : String

  Correct answer to negative question

• source : String

  Source citation

def Phenomena.Questions.WhComplement.instReprComplementPair.repr : ComplementPair → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.Questions.WhComplement.instReprComplementPair : Repr ComplementPair

Equations

• Phenomena.Questions.WhComplement.instReprComplementPair = { reprPrec := Phenomena.Questions.WhComplement.instReprComplementPair.repr }

def Phenomena.Questions.WhComplement.whoWalks : ComplementPair

Classic example from @cite{groenendijk-stokhof-1984}: "Who walks?" vs "Who doesn't walk?" Source: @cite{groenendijk-stokhof-1984}, p. 280

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.WhComplement.whichStudentsPassed : ComplementPair

"Which students passed?" vs "Which students didn't pass?"

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.WhComplement.whatDidJohnBuy : ComplementPair

"What did John buy?" vs "What didn't John buy?" (from a contextually salient set)

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.WhComplement.complementPairs : List ComplementPair

Equations

• One or more equations did not get rendered due to their size.

theorem Phenomena.Questions.WhComplement.complement_same_partition_claim : True

Key theoretical claim: complement questions induce the same partition.

Proof sketch (@cite{groenendijk-stokhof-1984}):

• ⟦Who walks?⟧ = λw.λv. [walk_w = walk_v]
• ⟦Who doesn't walk?⟧ = λw.λv. [¬walk_w = ¬walk_v]
• But ¬walk_w = ¬walk_v iff walk_w = walk_v (set complement is injective)
• Therefore the partitions are identical.

theorem Phenomena.Questions.WhComplement.answers_differ (cp : ComplementPair) (h : cp.positiveAnswer ≠ cp.negativeAnswer) : cp.positiveAnswer ≠ cp.negativeAnswer

The answers differ despite identical complements.

structure Phenomena.Questions.WhComplement.AnswerAppropriateness : Type

An answer is appropriate if it names the right set of individuals. For positive Q: name the satisfiers. For negative Q: name the non-satisfiers.

• question : String

  The question

• isPositive : Bool

  Is this the positive or negative form?

• answer : String

  The proposed answer

• appropriate : Bool

  Is this answer appropriate?

• explanation : String

  Explanation

instance Phenomena.Questions.WhComplement.instReprAnswerAppropriateness : Repr AnswerAppropriateness

Equations

• Phenomena.Questions.WhComplement.instReprAnswerAppropriateness = { reprPrec := Phenomena.Questions.WhComplement.instReprAnswerAppropriateness.repr }

def Phenomena.Questions.WhComplement.instReprAnswerAppropriateness.repr : AnswerAppropriateness → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.WhComplement.whoWalks_pos_correct : AnswerAppropriateness

"John and Mary" is appropriate for "Who walks?"

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.WhComplement.whoWalks_pos_incorrect : AnswerAppropriateness

"Bill" is INappropriate for "Who walks?"

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.WhComplement.whoWalks_neg_correct : AnswerAppropriateness

"Bill" is appropriate for "Who doesn't walk?"

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.WhComplement.whoWalks_neg_incorrect : AnswerAppropriateness

"John and Mary" is INappropriate for "Who doesn't walk?"

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.WhComplement.answerAppropriatenessExamples : List AnswerAppropriateness

Equations

• One or more equations did not get rendered due to their size.

structure Phenomena.Questions.WhComplement.PolarWhParallel : Type

The parallel between wh-complement and polar question polarity.

Polar Questions:

• PPQ "Is it raining?" → biased toward "yes"
• NPQ "Isn't it raining?" → biased toward "yes" (= "no, it's not raining")

Wh-Questions:

• "Who P?" → answer names satisfiers of P
• "Who doesn't P?" → answer names satisfiers of ¬P

In both cases, the FORM of the question (positive vs negative) determines which answer is "direct" even when the partition is the same.

• polarExample : String

  Polar question example

• whExample : String

  Corresponding wh-question example

• positiveAsksFor : String

  What the positive form asks for

• negativeAsksFor : String

  What the negative form asks for

def Phenomena.Questions.WhComplement.instReprPolarWhParallel.repr : PolarWhParallel → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.Questions.WhComplement.instReprPolarWhParallel : Repr PolarWhParallel

Equations

• Phenomena.Questions.WhComplement.instReprPolarWhParallel = { reprPrec := Phenomena.Questions.WhComplement.instReprPolarWhParallel.repr }

def Phenomena.Questions.WhComplement.polarWhParallels : List PolarWhParallel

Equations

• One or more equations did not get rendered due to their size.

inductive Phenomena.Questions.WhComplement.TheoreticalPosition : Type

Key observation: partition semantics alone cannot explain the asymmetry.

If ⟦Who walks?⟧ = ⟦Who doesn't walk?⟧ (as partitions), then partition semantics predicts they should have the same answers. But they don't.

Possible solutions:

1. Questions denote MORE than partitions (e.g., structured meanings)
2. Answer appropriateness is pragmatic, not purely semantic
3. The "focus" or "aboutness" of the question matters

• structuredMeanings : TheoreticalPosition
• pragmaticAnswerhood : TheoreticalPosition
• aboutnessFocus : TheoreticalPosition

instance Phenomena.Questions.WhComplement.instDecidableEqTheoreticalPosition : DecidableEq TheoreticalPosition

Equations

• Phenomena.Questions.WhComplement.instDecidableEqTheoreticalPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.WhComplement.instReprTheoreticalPosition.repr : TheoreticalPosition → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.Questions.WhComplement.instReprTheoreticalPosition : Repr TheoreticalPosition

Equations

• Phenomena.Questions.WhComplement.instReprTheoreticalPosition = { reprPrec := Phenomena.Questions.WhComplement.instReprTheoreticalPosition.repr }

def Phenomena.Questions.WhComplement.gsolution : String

G&S's own solution involves the DENOTATION DOMAIN. "Who walks?" asks about the extension of "walk". "Who doesn't walk?" asks about the extension of "not walk". These are different semantic objects even if they induce the same partition.

Equations

• Phenomena.Questions.WhComplement.gsolution = "The question asks about a specific predicate's extension; " ++ "negation changes which predicate we're asking about."