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, the four contexts that control a focus in [HZ07c] §1.2, the notion of control being [Uhm91]'s. Use classifies the shapes; felicity (Antecedent.Admits) is containment of the antecedent's contrast set in the focus value, 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, Set (Set W), keeping antecedents over finite models decide-friendly; a Question supplies one through Question.alt. The assertion payload is a raw prior proposition; the HasAssertion hookup (a correction/denial move) is deferred.

inductive 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

@[instance_reducible]

instance Focus.instDecidableEqUse : DecidableEq Use

Equations

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

@[instance_reducible]

instance Focus.instReprUse : Repr Use

Equations

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

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

Equations

• Focus.instReprUse.repr Focus.Use.newInfo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Use.newInfo")).group prec✝
• Focus.instReprUse.repr Focus.Use.corrective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Use.corrective")).group prec✝
• Focus.instReprUse.repr Focus.Use.selective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Use.selective")).group prec✝
• Focus.instReprUse.repr Focus.Use.contrastive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Focus.Use.contrastive")).group prec✝

@[instance_reducible]

instance Focus.instInhabitedUse : Inhabited Use

Equations

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

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

A focus antecedent is 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 : Set (Set W)) : Antecedent W

  A question with (flat Hamblin) denotation q.

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

  A prior assertion p, corrected among alternatives alts.

• offer {W : Type u_2} (alts : Set (Set W)) : Antecedent W

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

• parallel {W : Type u_2} (alts : Set (Set 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 Focus.Antecedent.contrastSet {W : Type u_1} : Antecedent W → Set (Set W)

The contrast set Γ an antecedent supplies to the squiggle.

Equations

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

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

The pragmatic use an antecedent shape licenses.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def 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

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

@[simp]

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

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

Every pragmatic use is realised by some antecedent shape.

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

An antecedent admits a focus value when its contrast set lies inside the focus value, [Roo92]'s focus interpretation principle.

Equations

• c.Admits fv = (c.contrastSet ⊆ fv)

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

Admits is monotone in the focus value.

theorem Focus.admits_inter_iff {W : Type u_1} {c : Antecedent W} {fv fv' : Set (Set 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 Focus.SquiggleSet {α : Type u_2} (o : α) (fv Γ : Set α) : Prop

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

Equations

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

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

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

Equations

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

theorem 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, the focus interpretation principle).

theorem 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 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 Focus.not_squiggleInd_singleton {α : Type u_2} (o γ : α) : ¬SquiggleInd o {o} γ

theorem Focus.not_squiggleSet_unfeatured {α : Type u_2} (x : α) (Γ : Set α) : ¬SquiggleSet (WithAlternatives.unfeatured x).ordinary (WithAlternatives.unfeatured x).alternatives Γ

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

def Focus.Antecedent.Resolves {W : Type u_1} : Antecedent W → Set W → Set (Set 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

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

theorem Focus.Antecedent.Resolves.admits {W : Type u_1} {c : Antecedent W} {o : Set W} {fv : Set (Set 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 Focus.admits_factorsThrough_contrastSet {W : Type u_1} (fv : Set (Set 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 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.

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 Focus.pairAnswer {W : Type u_2} (d d' : W) : WithAlternatives (Set W)

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

Equations

• Focus.pairAnswer d d' = (fun (x : W) => {x}) <$> { ordinary := d, alternatives := {d, d'} }

@[simp]

theorem Focus.pairAnswer_ordinary {W : Type u_2} (d d' : W) : (pairAnswer d d').ordinary = {d}

@[simp]

theorem Focus.pairAnswer_alternatives {W : Type u_2} (d d' : W) : (pairAnswer d d').alternatives = {{d}, {d'}}

theorem 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').ordinary (pairAnswer d d').alternatives

Every canonical antecedent shape fully resolves, all squiggle clauses including the correction clause, against the composed answer over its pair, so the four pragmatic uses share one semantics.