Focus antecedents

The anaphoric source of the squiggle's contrast set ([Roo92]): what the preceding discourse supplies — a question, a prior assertion to correct, explicitly offered alternatives, or a parallel focus ([Uhm91]'s focus-control taxonomy, adopted by [HZ07] §1.2). Use classifies the shapes; felicity (Antecedent.Admits) is fip on the antecedent's contrast set, uniformly across uses — and use_not_factorsThrough_contrastSet shows the four-way split is invisible to the semantics.

SquiggleSet/SquiggleInd state the full presuppositions of [Roo92]'s operator (his (40), set and individual cases): Admits is only the first set-case clause, and the contrast clauses are what make anaphorically demanding — not_squiggleSet_unfeatured derives "the argument must contain a focus" from the unit focus value of focus-free phrases. Antecedent.Resolves routes each antecedent shape through the appropriate case.

Implementation notes

Payloads are flat Hamblin sets (PropFocusValue), keeping antecedents over finite models decide-friendly; the inquisitive layer plugs in via Antecedent.ofQuestion and Question.alt, with alt_which_singleton identifying the two Hamblin constructions. The assertion payload is a raw prior proposition; the Discourse.CommonGround.HasAssertion hookup (a correction/denial move) is deferred.

inductive Semantics.Focus.Use : Type

The four pragmatic uses of one semantic focus ([Uhm91]): the image of Antecedent.use.

• newInfo : Use
• corrective : Use
• selective : Use
• contrastive : Use

@[implicit_reducible]

instance Semantics.Focus.instDecidableEqUse : DecidableEq Use

Equations

• Semantics.Focus.instDecidableEqUse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Focus.instReprUse : Repr Use

Equations

• Semantics.Focus.instReprUse = { reprPrec := Semantics.Focus.instReprUse.repr }

def Semantics.Focus.instReprUse.repr : Use → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Focus.instInhabitedUse : Inhabited Use

Equations

• Semantics.Focus.instInhabitedUse = { default := Semantics.Focus.instInhabitedUse.default }

inductive Semantics.Focus.Antecedent (W : Type u_2) : Type u_2

A focus antecedent: the discourse object that supplies the squiggle's antecedent — a contrast set for [Roo92]'s set case, or a single contrasting ordinary value for the individual case.

• question {W : Type u_2} (q : Interpretation.PropFocusValue W) : Antecedent W

  A question with (flat Hamblin) denotation q.

• assertion {W : Type u_2} (p : Set W) (alts : Interpretation.PropFocusValue W) : Antecedent W

  A prior assertion p, corrected among alternatives alts.

• offer {W : Type u_2} (alts : Interpretation.PropFocusValue W) : Antecedent W

  Explicitly offered alternatives ('coffee or tea?').

• parallel {W : Type u_2} (alts : Interpretation.PropFocusValue W) : Antecedent W

  A parallel focus with focus value alts.

• phrase {W : Type u_2} (γ : Set W) : Antecedent W

  A contrasting phrase's ordinary value ([Roo92]'s individual case; the "contrasting phrases" rule).

def Semantics.Focus.Antecedent.contrastSet {W : Type u_1} : Antecedent W → Interpretation.PropFocusValue W

The contrast set Γ an antecedent supplies to the squiggle.

Equations

• (Semantics.Focus.Antecedent.question q).contrastSet = q
• (Semantics.Focus.Antecedent.assertion p alts).contrastSet = alts
• (Semantics.Focus.Antecedent.offer alts).contrastSet = alts
• (Semantics.Focus.Antecedent.parallel alts).contrastSet = alts
• (Semantics.Focus.Antecedent.phrase γ).contrastSet = {γ}

def Semantics.Focus.Antecedent.use {W : Type u_1} : Antecedent W → Use

The pragmatic use an antecedent shape licenses.

Equations

• (Semantics.Focus.Antecedent.question q).use = Semantics.Focus.Use.newInfo
• (Semantics.Focus.Antecedent.assertion p alts).use = Semantics.Focus.Use.corrective
• (Semantics.Focus.Antecedent.offer alts).use = Semantics.Focus.Use.selective
• (Semantics.Focus.Antecedent.parallel alts).use = Semantics.Focus.Use.contrastive
• (Semantics.Focus.Antecedent.phrase γ).use = Semantics.Focus.Use.contrastive

@[simp]

theorem Semantics.Focus.contrastSet_question {W : Type u_1} (q : Interpretation.PropFocusValue W) : (Antecedent.question q).contrastSet = q

@[simp]

theorem Semantics.Focus.contrastSet_assertion {W : Type u_1} (p : Set W) (alts : Interpretation.PropFocusValue W) : (Antecedent.assertion p alts).contrastSet = alts

@[simp]

theorem Semantics.Focus.contrastSet_offer {W : Type u_1} (alts : Interpretation.PropFocusValue W) : (Antecedent.offer alts).contrastSet = alts

@[simp]

theorem Semantics.Focus.contrastSet_parallel {W : Type u_1} (alts : Interpretation.PropFocusValue W) : (Antecedent.parallel alts).contrastSet = alts

@[simp]

theorem Semantics.Focus.use_question {W : Type u_1} (q : Interpretation.PropFocusValue W) : (Antecedent.question q).use = Use.newInfo

@[simp]

theorem Semantics.Focus.use_assertion {W : Type u_1} (p : Set W) (alts : Interpretation.PropFocusValue W) : (Antecedent.assertion p alts).use = Use.corrective

@[simp]

theorem Semantics.Focus.use_offer {W : Type u_1} (alts : Interpretation.PropFocusValue W) : (Antecedent.offer alts).use = Use.selective

@[simp]

theorem Semantics.Focus.use_parallel {W : Type u_1} (alts : Interpretation.PropFocusValue W) : (Antecedent.parallel alts).use = Use.contrastive

@[simp]

theorem Semantics.Focus.contrastSet_phrase {W : Type u_1} (γ : Set W) : (Antecedent.phrase γ).contrastSet = {γ}

@[simp]

theorem Semantics.Focus.use_phrase {W : Type u_1} (γ : Set W) : (Antecedent.phrase γ).use = Use.contrastive

def Semantics.Focus.Use.model {W : Type u_1} (o a : Set W) : Use → Antecedent W

The canonical antecedent of each use over a designated ordinary-value/alternative pair (o, a): a question, an assertion of the alternative to be corrected, an offer, or a parallel focus — the minimal contentful model of the four controlling contexts.

Equations

• Semantics.Focus.Use.model o a Semantics.Focus.Use.newInfo = Semantics.Focus.Antecedent.question {o, a}
• Semantics.Focus.Use.model o a Semantics.Focus.Use.corrective = Semantics.Focus.Antecedent.assertion a {o, a}
• Semantics.Focus.Use.model o a Semantics.Focus.Use.selective = Semantics.Focus.Antecedent.offer {o, a}
• Semantics.Focus.Use.model o a Semantics.Focus.Use.contrastive = Semantics.Focus.Antecedent.parallel {o, a}

@[simp]

theorem Semantics.Focus.use_model {W : Type u_1} (o a : Set W) (u : Use) : (Use.model o a u).use = u

theorem Semantics.Focus.use_surjective {W : Type u_1} : Function.Surjective Antecedent.use

Every pragmatic use is realised by some antecedent shape.

def Semantics.Focus.Antecedent.Admits {W : Type u_1} (c : Antecedent W) (fv : Interpretation.PropFocusValue W) : Prop

Roothian felicity of a focus value against an antecedent: fip on the antecedent's contrast set.

Equations

• c.Admits fv = Semantics.Focus.Interpretation.fip c.contrastSet fv

theorem Semantics.Focus.question_admits_iff {W : Type u_1} (q fv : Interpretation.PropFocusValue W) : (Antecedent.question q).Admits fv ↔ Interpretation.qaCongruentWeak fv q

The question case is the substrate's Q-A congruence.

theorem Semantics.Focus.Antecedent.Admits.mono {W : Type u_1} {c : Antecedent W} {fv fv' : Interpretation.PropFocusValue W} (hc : c.Admits fv) (h : fv ⊆ fv') : c.Admits fv'

Admits is monotone in the focus value.

theorem Semantics.Focus.admits_inter_iff {W : Type u_1} {c : Antecedent W} {fv fv' : Interpretation.PropFocusValue W} : c.Admits (fv ∩ fv') ↔ c.Admits fv ∧ c.Admits fv'

An intersection of focus values is admitted iff both are.

The squiggle presupposition

[Roo92]'s operator introduces the presuppositions of its (40), over an ordinary value o and focus value fv of any type: in the set case the resolved antecedent Γ is a subset of fv containing o and a distinct alternative; in the individual case the antecedent is a member of fv distinct from o. Admits is the first set-case clause; the contrast clauses are what make anaphorically demanding.

def Semantics.Focus.SquiggleSet {α : Type u_2} (o : α) (fv Γ : Set α) : Prop

The ~ presupposition, set case: Γ ⊆ fv, o ∈ Γ, and Γ contains an alternative distinct from o ([Roo92] (40)).

Equations

• Semantics.Focus.SquiggleSet o fv Γ = (Γ ⊆ fv ∧ o ∈ Γ ∧ ∃ x ∈ Γ, x ≠ o)

def Semantics.Focus.SquiggleInd {α : Type u_2} (o : α) (fv : Set α) (γ : α) : Prop

The ~ presupposition, individual case: the antecedent is a member of fv distinct from o ([Roo92] (40)); the contrasting-phrases rule is this with γ := ⟦β⟧ᵒ.

Equations

• Semantics.Focus.SquiggleInd o fv γ = (γ ∈ fv ∧ γ ≠ o)

theorem Semantics.Focus.SquiggleSet.subset {α : Type u_2} {o : α} {fv Γ : Set α} (h : SquiggleSet o fv Γ) : Γ ⊆ fv

The first set-case clause alone: the antecedent is a subset of the focus value (at the propositional level, exactly fip).

theorem Semantics.Focus.SquiggleSet.nontrivial {α : Type u_2} {o : α} {fv Γ : Set α} (h : SquiggleSet o fv Γ) : Γ.Nontrivial

A resolved antecedent is nontrivial: it contains the ordinary value and a distinct alternative.

theorem Semantics.Focus.not_squiggleSet_singleton {α : Type u_2} (o : α) (Γ : Set α) : ¬SquiggleSet o {o} Γ

A unit focus value defeats the contrast clause: nothing resolves against {o}.

theorem Semantics.Focus.not_squiggleInd_singleton {α : Type u_2} (o γ : α) : ¬SquiggleInd o {o} γ

theorem Semantics.Focus.not_squiggleSet_unfeatured {α : Type u_2} (x : α) (Γ : Set α) : ¬SquiggleSet (Alternatives.AltMeaning.unfeatured x).oValue (Alternatives.AltMeaning.unfeatured x).aSet Γ

"The argument must contain a focus": a focus-free phrase has a unit focus value, so no antecedent resolves against it ([Roo92] §10).

def Semantics.Focus.Antecedent.Resolves {W : Type u_1} : Antecedent W → Set W → Interpretation.PropFocusValue W → Prop

Full Roothian resolution of an antecedent against a two-dimensional meaning (o, fv): the set case for question / offer / parallel antecedents, the individual case for contrasting phrases — and for assertion antecedents additionally the correction clause: the resolved ordinary value replaces (differs from) the prior assertion.

Equations

• (Semantics.Focus.Antecedent.phrase γ).Resolves x✝¹ x✝ = Semantics.Focus.SquiggleInd x✝¹ x✝ γ
• (Semantics.Focus.Antecedent.assertion p alts).Resolves x✝¹ x✝ = (Semantics.Focus.SquiggleSet x✝¹ x✝ alts ∧ x✝¹ ≠ p)
• x✝².Resolves x✝¹ x✝ = Semantics.Focus.SquiggleSet x✝¹ x✝ x✝².contrastSet

theorem Semantics.Focus.Antecedent.Resolves.admits {W : Type u_1} {c : Antecedent W} {o : Set W} {fv : Interpretation.PropFocusValue W} (h : c.Resolves o fv) : c.Admits fv

Full resolution entails felicity: Admits is the set case's first clause, and a resolved contrasting phrase is a member of the focus value.

theorem Semantics.Focus.admits_factorsThrough_contrastSet {W : Type u_1} (fv : Interpretation.PropFocusValue W) : Function.FactorsThrough (fun (x : Antecedent W) => x.Admits fv) Antecedent.contrastSet

Felicity factors through the contrast set: the semantics sees Γ, never the use label.

theorem Semantics.Focus.use_not_factorsThrough_contrastSet {W : Type u_1} : ¬Function.FactorsThrough Antecedent.use Antecedent.contrastSet

Distinct uses can supply one and the same Γ (a question and an explicit offer, say), so the four-way split is invisible to the Roothian semantics — pragmatic, not semantic.

Hamblin antecedents

def Semantics.Focus.hamblin (D : Type u_2) : Interpretation.PropFocusValue D

The flat Hamblin set of complete answers over a domain.

Equations

• Semantics.Focus.hamblin D = Set.range fun (d : D) => {d}

def Semantics.Focus.whAntecedent (D : Type u_2) : Antecedent D

The wh-question antecedent over a whole domain.

Equations

• Semantics.Focus.whAntecedent D = Semantics.Focus.Antecedent.question (Semantics.Focus.hamblin D)

theorem Semantics.Focus.whAntecedent_admits (D : Type u_2) : (whAntecedent D).Admits (hamblin D)

theorem Semantics.Focus.whAntecedent_resolves {D : Type u_2} (d d' : D) (hne : d' ≠ d) : (whAntecedent D).Resolves {d} (hamblin D)

A wh-antecedent over a domain with two distinct elements fully resolves against the Hamblin focus value of any complete answer.

Composed answers over a pair

The minimal contentful scenario: a two-point answer domain {d, d'} with d the true answer. The answer is built by the composition engine — the singleton complete-answer predicate mapped over the F-marked argument — and every canonical antecedent shape fully resolves against it.

def Semantics.Focus.pairAnswer {W : Type u_2} (d d' : W) : Alternatives.AltMeaning (Set W)

The composed focused answer d over the pair {d, d'}.

Equations

• Semantics.Focus.pairAnswer d d' = (fun (x : W) => {x}) <$> { oValue := d, aValue := [d, d'] }

@[simp]

theorem Semantics.Focus.pairAnswer_oValue {W : Type u_2} (d d' : W) : (pairAnswer d d').oValue = {d}

@[simp]

theorem Semantics.Focus.pairAnswer_aSet {W : Type u_2} (d d' : W) : (pairAnswer d d').aSet = {{d}, {d'}}

theorem Semantics.Focus.use_model_resolves {W : Type u_2} {d d' : W} (hne : d' ≠ d) (u : Use) : (Use.model {d} {d'} u).Resolves (pairAnswer d d').oValue (pairAnswer d d').aSet

Uniform resolution across the four uses: every canonical antecedent shape fully resolves — all squiggle clauses, including the correction clause — against the composed answer over its pair. One semantics, four pragmatic uses.

Strong-theory only

[Roo92]'s official semantics: only quantifies over the resolved contrast variable C; the focus constraint C ⊆ ⟦·⟧f is supplied separately by the squiggle, "leaving room for a pragmatic process of constructing a domain of quantification". The operator has no lexical access to focus values — direct-association implementations carry an alternative list lexically instead, and the two provably diverge under domain restriction (Studies/Rooth1992.lean).

def Semantics.Focus.onlyVia {W : Type u_1} (C : Interpretation.PropFocusValue W) (prejacent : Set W) : Set W

The strong-theory only assertion, transposed to the propositional level: every true member of the resolved contrast set is the prejacent. The prejacent presupposition is carried separately.

Equations

• Semantics.Focus.onlyVia C prejacent = {w : W | ∀ q ∈ C, w ∈ q → q = prejacent}

@[simp]

theorem Semantics.Focus.mem_onlyVia {W : Type u_1} {C : Interpretation.PropFocusValue W} {p : Set W} {w : W} : w ∈ onlyVia C p ↔ ∀ q ∈ C, w ∈ q → q = p

theorem Semantics.Focus.not_mem_onlyVia {W : Type u_1} {C : Interpretation.PropFocusValue W} {p q : Set W} {w : W} (hq : q ∈ C) (hw : w ∈ q) (hne : q ≠ p) : w ∉ onlyVia C p

A true alternative distinct from the prejacent refutes only.

theorem Semantics.Focus.mem_onlyVia_of_forall_not_mem {W : Type u_1} {C : Interpretation.PropFocusValue W} {p : Set W} {w : W} (h : ∀ q ∈ C, q ≠ p → w ∉ q) : w ∈ onlyVia C p

Membership in only from refuting every distinct alternative.

def Semantics.Focus.Irredundant {W : Type u_1} {ι : Type u_2} (f : ι → Set W) : Prop

An irredundant family of alternatives: each member can hold while every other member fails — equivalently, no member is covered by the union of the rest (each alternative has a private world). Strictly weaker than the mutual exclusivity of partition semantics (irredundant_of_pairwise_disjoint) and than Boolean independence of the family. [UPSTREAM] candidate as the non-coveredness companion of iSupIndep (¬ t i ≤ ⨆ j ≠ i, t j): mathlib has the disjointness form and, at the module instance, the characterization linearIndependent_iff_notMem_span, but no lattice-level name — and SupIrred (join-irreducibility of an element) is a false friend.

Equations

• Semantics.Focus.Irredundant f = ∀ (i : ι), ∃ w ∈ f i, ∀ (j : ι), j ≠ i → w ∉ f j

theorem Semantics.Focus.irredundant_of_pairwise_disjoint {W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hd : Pairwise fun (i j : ι) => Disjoint (f i) (f j)) (hne : ∀ (i : ι), (f i).Nonempty) : Irredundant f

Pairwise-disjoint nonempty alternatives — the mutual-exclusivity assumption of partition semantics — are irredundant.

theorem Semantics.Focus.Irredundant.onlyVia_ne {W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hf : Irredundant f) {i₀ j : ι} {s₁ s₂ : Finset ι} (hj₂ : j ∈ s₂) (hj₁ : j ∉ s₁) (hji : j ≠ i₀) : onlyVia (f '' ↑s₁) (f i₀) ≠ onlyVia (f '' ↑s₂) (f i₀)

Over a separated family, resolving only to contrast sets that differ beyond the prejacent yields distinct readings: the alternative present in one resolution and absent from the other separates them.

theorem Semantics.Focus.Irredundant.onlyVia_injOn {W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hf : Irredundant f) (i₀ : ι) : Set.InjOn (fun (s : Finset ι) => onlyVia (f '' ↑s) (f i₀)) {s : Finset ι | i₀ ∈ s}

Over a separated family, only is injective in the resolved contrast set, on resolutions containing the prejacent.

theorem Semantics.Focus.onlyVia_antitone {W : Type u_1} {C C' : Interpretation.PropFocusValue W} (h : C ⊆ C') (p : Set W) : onlyVia C' p ⊆ onlyVia C p

Narrowing the domain weakens only — the pragmatic domain restriction that repairs the over-generation of a fixed full-focus domain.

theorem Semantics.Focus.onlyVia_excludes_of_squiggleSet {W : Type u_1} {o : Set W} {fv C : Interpretation.PropFocusValue W} (h : SquiggleSet o fv C) : ∃ q ∈ C, q ≠ o ∧ ∀ w ∈ onlyVia C o, w ∉ q

Against a squiggle-resolved contrast set, only genuinely excludes: the contrast clause supplies a distinct alternative that the assertion rules out wherever it holds.

def Semantics.Focus.Antecedent.ofQuestion {W : Type u_1} (q : Question W) : Antecedent W

A Question supplies its maximal alternatives as a question antecedent — the bridge from the inquisitive layer.

Equations

• Semantics.Focus.Antecedent.ofQuestion q = Semantics.Focus.Antecedent.question q.alt

theorem Semantics.Focus.alt_which_singleton (D : Type u_2) [Nonempty D] : (Question.which Set.univ fun (d : D) => {d}).alt = hamblin D

The maximal alternatives of the inquisitive wh-question over the singleton predicates are exactly the flat Hamblin set.

theorem Semantics.Focus.ofQuestion_which_eq_whAntecedent (D : Type u_2) [Nonempty D] : Antecedent.ofQuestion (Question.which Set.univ fun (d : D) => {d}) = whAntecedent D

The inquisitive wh-question and the flat Hamblin antecedent coincide.