Hofmann (2025): Anaphoric Accessibility with Flat Update

Hofmann accounts for anaphora to negated indefinites in the intensional compositional DRT of Semantics/Dynamic/ICDRT.lean. An indefinite introduces its discourse referent globally, relative to the propositional referent of its local context, and a pronoun is acceptable when its referent exists throughout its own local context under a consistent assignment of speaker commitments. This file runs the fragment of the paper's Appendix C on its four-world model of the bathroom discourses.

Main statements

• veridicalIndiv_of_accessible, counterfactual_blocks_veridical: an accessible anaphor in a veridical context has a veridical antecedent, and a counterfactual antecedent admits no veridical anaphor.
• veridical_run, doubleNeg_run, bathDisj_run, disagree_run: the discourses of Figures 6, 8, 9 and 10 are outputs of the fragment, with their pronouns accessible.
• negated_run, counterfactual_veridical_impossible: a negated antecedent (Figure 7) makes its referent counterfactual, and no consistent extension admits a veridical continuation.

Implementation notes

• The operators of the fragment are CDRT's: a DRS [δ | C] is box {δ} C and max_φ is maxAt at a propositional dref.
• The maximization operators of App. C (18) and (19), and of the displayed updates (41), (43) and (44), apply to updates that leave the maximized dref unchanged, so under the definition (40) they are vacuous (maxAt_eq_of_fixes): the fragment as printed does not exclude the nonmaximal rows of Table 3 (negated_row4). Maximizing the prejacent's context over the whole assertion selects the paper's row (negated_max), and the commitment set of Figure 6 is the pragmatically maximal one of (35) (veridical_maximal).
• Commitment sets are introduced at the initial state and never changed by an update, as in (33) and Table 1, so a derivation starts from the initial state whose commitment set its output shows; Figure 6's is narrower than Figure 5's.
• The modal-subordination discourse of §4.4 needs the eight-world model with a doxastic state for Sue and is not run.

TODO

• The eight-world model of §4.4 and the attitude update (52).

References

• [Hof25]
• [Mus96]
• [Sto99]
• [Bra06]
• [KM95]
• [Rob89]
• [Kar76]

Commitment and veridicality ((16), (36), (37))

@[reducible, inline]

abbrev Hofmann2025.VeridicalIndiv {W : Type u_1} {E : Type u_2} (φ_DC : ICDRT.PVar) (v : ICDRT.IVar) (i : ICDRT.State W E) : Prop

An individual dref is veridical if it is entailed in the commitment set (36a), and hypothetical when it is not veridical (16b).

Equations

• Hofmann2025.VeridicalIndiv φ_DC v i = (i ∈ ICDRT.localEntailment φ_DC v)

def Hofmann2025.CounterfactualIndiv {W : Type u_1} {E : Type u_2} (φ_DC : ICDRT.PVar) (v : ICDRT.IVar) (i : ICDRT.State W E) : Prop

An individual dref is counterfactual if it has no referent throughout the commitment set (37a).

Equations

• Hofmann2025.CounterfactualIndiv φ_DC v i = ∀ w ∈ i.prop φ_DC, i.indiv v w = none

def Hofmann2025.CounterfactualProp {W : Type u_1} {E : Type u_2} (φ_DC δ : ICDRT.PVar) (i : ICDRT.State W E) : Prop

A propositional dref is counterfactual if it is disjoint from the commitment set (37b).

Equations

• Hofmann2025.CounterfactualProp φ_DC δ i = (i.prop φ_DC ∩ i.prop δ = ∅)

theorem Hofmann2025.CounterfactualIndiv.not_veridicalIndiv {W : Type u_1} {E : Type u_2} {φ_DC : ICDRT.PVar} {v : ICDRT.IVar} {i : ICDRT.State W E} (hc : CounterfactualIndiv φ_DC v i) (hDC : (i.prop φ_DC).Nonempty) : ¬VeridicalIndiv φ_DC v i

Under consistent commitments a counterfactual dref is not veridical, so it is hypothetical, "more specifically, counterfactual" (16).

theorem Hofmann2025.counterfactualProp_of_mem_eqCompl {W : Type u_1} {E : Type u_2} {φ_DC φ φ' : ICDRT.PVar} {i : ICDRT.State W E} (hc : i ∈ ICDRT.eqCompl φ φ') (hdec : i ∈ ICDRT.incl φ_DC φ) : CounterfactualProp φ_DC φ' i

Negation under assertion makes its prejacent counterfactual, since the commitments entail the negation's context (the condition of assertion, (20a)), the complement of the prejacent's.

Accessibility (38) and the subset requirement (39)

def Hofmann2025.Accessible {W : Type u_1} {E : Type u_2} (φ : ICDRT.PVar) (v : ICDRT.IVar) (φ_DC : ICDRT.PVar) (i : ICDRT.State W E) : Prop

A dref υ is accessible (38) if it is entailed in the anaphor's local context φ and the commitment set is consistent. The paper's consistency (31) covers every interlocutor; this is one interlocutor's.

Equations

• Hofmann2025.Accessible φ v φ_DC i = (i ∈ ICDRT.localEntailment φ v ∧ (i.prop φ_DC).Nonempty)

theorem Hofmann2025.veridicalIndiv_of_accessible {W : Type u_1} {E : Type u_2} {φ φ_DC : ICDRT.PVar} {v : ICDRT.IVar} {j : ICDRT.State W E} (hdec : j ∈ ICDRT.incl φ_DC φ) (h : Accessible φ v φ_DC j) : VeridicalIndiv φ_DC v j

In a veridical anaphor context, one the speaker's commitments entail, only a veridical dref is accessible.

theorem Hofmann2025.counterfactual_blocks_veridical {W : Type u_1} {E : Type u_2} (i j : ICDRT.State W E) (φ_DC φ_anaphor φ_neg : ICDRT.PVar) (h_extends_DC : j.prop φ_DC = i.prop φ_DC) (h_extends_neg : j.prop φ_neg = i.prop φ_neg) (h_disjoint : CounterfactualProp φ_DC φ_neg i) (h_dec : j ∈ ICDRT.incl φ_DC φ_anaphor) (h_subset : j ∈ ICDRT.incl φ_anaphor φ_neg) : ¬(j.prop φ_DC).Nonempty

A counterfactual antecedent admits no veridical anaphor (§3.4.2, (26)). An extension that keeps the commitment set and the antecedent's context, entails the anaphor's context in the commitments, and meets the subset requirement (39) empties the commitment set.

The fragment of Appendix C

Each operator is a DRS [δ | C] = box {δ} C (App. B (12)) followed by maximization max_φ (App. B (10b)), CDRT's maxAt at a propositional dref.

@[reducible, inline]

abbrev Hofmann2025.SemE (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

A predicate, of type e(wt), takes an individual dref and a local context to an update.

Equations

• Hofmann2025.SemE W E = (ICDRT.IVar → ICDRT.PVar → DynamicSemantics.Update (ICDRT.State W E))

@[reducible, inline]

abbrev Hofmann2025.SemW (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

A clause, of type wt, takes a local context to an update.

Equations

• Hofmann2025.SemW W E = (ICDRT.PVar → DynamicSemantics.Update (ICDRT.State W E))

def Hofmann2025.vacuousScope {W : Type u_1} {E : Type u_2} : SemE W E

The vacuous scope of an existential is the identity update.

Equations

• Hofmann2025.vacuousScope x✝¹ x✝ = SetRel.id

def Hofmann2025.commonNoun {W : Type u_1} {E : Type u_2} (R : E → W → Prop) : SemE W E

A common noun is a test that its argument satisfies it in the local context (App. C (15)).

Equations

• Hofmann2025.commonNoun R v φ = DynamicSemantics.Update.test (ICDRT.pred R φ v)

@[reducible, inline]

abbrev Hofmann2025.intransVP {W : Type u_1} {E : Type u_2} (R : E → W → Prop) : SemE W E

An intransitive verb phrase, of the same shape as a common noun.

Equations

• Hofmann2025.intransVP R = Hofmann2025.commonNoun R

def Hofmann2025.indefinite {W : Type u_1} {E : Type u_2} (v : ICDRT.IVar) (P P' : SemE W E) (φ : ICDRT.PVar) : DynamicSemantics.Update (ICDRT.State W E)

The indefinite introduces its dref relative to the local context, then runs its restrictor and its scope (App. C (16)).

Equations

• Hofmann2025.indefinite v P P' φ = (SetRel.comp (ICDRT.relUpdate φ v) (P v φ)).comp (P' v φ)

def Hofmann2025.pronoun {W : Type u_1} {E : Type u_2} (v : ICDRT.IVar) (P : SemE W E) (φ : ICDRT.PVar) : DynamicSemantics.Update (ICDRT.State W E)

A pronoun passes its index to the predicate (App. C (17)).

Equations

• Hofmann2025.pronoun v P φ = P v φ

def Hofmann2025.properName {W : Type u_1} {E : Type u_2} (name : E) (v : ICDRT.IVar) (P : SemE W E) (φ : ICDRT.PVar) : DynamicSemantics.Update (ICDRT.State W E)

A proper name introduces a dref equal to its constant (App. C (14)).

Equations

• Hofmann2025.properName name v P φ = SetRel.comp (DynamicSemantics.Update.box {v} {j : ICDRT.State W E | ∀ (w : W), j.indiv v w = some name}) (P v φ)

def Hofmann2025.semNOT {W : Type u_1} {E : Type u_2} (φ' : ICDRT.PVar) (Sc : SemW W E) (φ : ICDRT.PVar) : DynamicSemantics.Update (ICDRT.State W E)

Negation introduces the complement of its context as the prejacent's context and maximizes it over the prejacent (App. C (18a)).

Equations

• Hofmann2025.semNOT φ' Sc φ = SetRel.comp (DynamicSemantics.Update.box {φ'} (ICDRT.eqCompl φ φ')) (DynamicSemantics.Update.maxAt φ' (Sc φ'))

def Hofmann2025.semOR {W : Type u_1} {E : Type u_2} (φ' φ'' : ICDRT.PVar) (Sc' Sc'' : SemW W E) (φ : ICDRT.PVar) : DynamicSemantics.Update (ICDRT.State W E)

Disjunction introduces a context for each disjunct, whose union is its own (App. C (18b)).

Equations

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

def Hofmann2025.semIF {W : Type u_1} {E : Type u_2} (φ' φ'' : ICDRT.PVar) (Sc' Sc'' : SemW W E) (φ : ICDRT.PVar) : DynamicSemantics.Update (ICDRT.State W E)

The conditional's context is the union of the antecedent's complement and the consequent's context (App. C (18c)).

Equations

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

def Hofmann2025.semAND {W : Type u_1} {E : Type u_2} (φ' φ'' : ICDRT.PVar) (Sc' Sc'' : SemW W E) (φ : ICDRT.PVar) : DynamicSemantics.Update (ICDRT.State W E)

Conjunction narrows the context through each conjunct in turn (App. C (18d)).

Equations

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

def Hofmann2025.semBelieved {W : Type u_1} {E : Type u_2} (φ' : ICDRT.PVar) (dox : ICDRT.State W E → Set W) (Sc : SemW W E) (_φ : ICDRT.PVar) : DynamicSemantics.Update (ICDRT.State W E)

An attitude verb introduces a context the subject's doxastic state dox entails (App. C (18e)).

Equations

• Hofmann2025.semBelieved φ' dox Sc _φ = SetRel.comp (DynamicSemantics.Update.box {φ'} {j : ICDRT.State W E | dox j ⊆ j.prop φ'}) (DynamicSemantics.Update.maxAt φ' (Sc φ'))

def Hofmann2025.semDEC {W : Type u_1} {E : Type u_2} (φ_DC φ : ICDRT.PVar) (Sc : SemW W E) : DynamicSemantics.Update (ICDRT.State W E)

The declarative introduces the assertion's context, which the speaker's commitments entail (20a), and maximizes it over the clause (App. C (19)).

Equations

• Hofmann2025.semDEC φ_DC φ Sc = SetRel.comp (DynamicSemantics.Update.box {φ} (ICDRT.incl φ_DC φ)) (DynamicSemantics.Update.maxAt φ (Sc φ))

Maximization of a dref an update leaves fixed

theorem Hofmann2025.commonNoun_fixes {W : Type u_1} {E : Type u_2} (φ : ICDRT.PVar) (R : E → W → Prop) (v : ICDRT.IVar) (φ' : ICDRT.PVar) : DynamicSemantics.Update.Fixes φ (commonNoun R v φ')

theorem Hofmann2025.vacuousScope_fixes {W : Type u_1} {E : Type u_2} (φ : ICDRT.PVar) (v : ICDRT.IVar) (φ' : ICDRT.PVar) : DynamicSemantics.Update.Fixes φ (vacuousScope v φ')

theorem Hofmann2025.indefinite_fixes {W : Type u_1} {E : Type u_2} (φ : ICDRT.PVar) {v : ICDRT.IVar} {P P' : SemE W E} {φ' : ICDRT.PVar} (hP : DynamicSemantics.Update.Fixes φ (P v φ')) (hP' : DynamicSemantics.Update.Fixes φ (P' v φ')) : DynamicSemantics.Update.Fixes φ (indefinite v P P' φ')

theorem Hofmann2025.pronoun_fixes {W : Type u_1} {E : Type u_2} (φ : ICDRT.PVar) {v : ICDRT.IVar} {P : SemE W E} {φ' : ICDRT.PVar} (h : DynamicSemantics.Update.Fixes φ (P v φ')) : DynamicSemantics.Update.Fixes φ (pronoun v P φ')

theorem Hofmann2025.semNOT_fixes {W : Type u_1} {E : Type u_2} (φ : ICDRT.PVar) {φ' : ICDRT.PVar} {Sc : SemW W E} {φ₀ : ICDRT.PVar} (h : φ' ≠ φ) (hSc : DynamicSemantics.Update.Fixes φ (Sc φ')) : DynamicSemantics.Update.Fixes φ (semNOT φ' Sc φ₀)

Negation fixes every dref other than the one it introduces that its prejacent fixes.

theorem Hofmann2025.semOR_fixes {W : Type u_1} {E : Type u_2} (φ : ICDRT.PVar) {φ' φ'' : ICDRT.PVar} {Sc' Sc'' : SemW W E} {φ₀ : ICDRT.PVar} (h₁ : φ ≠ φ') (h₂ : φ ≠ φ'') (h' : DynamicSemantics.Update.Fixes φ (Sc' φ')) (h'' : DynamicSemantics.Update.Fixes φ (Sc'' φ'')) : DynamicSemantics.Update.Fixes φ (semOR φ' φ'' Sc' Sc'' φ₀)

theorem Hofmann2025.semDEC_fixes {W : Type u_1} {E : Type u_2} (φ : ICDRT.PVar) {φ_DC φ' : ICDRT.PVar} {Sc : SemW W E} (h : φ' ≠ φ) (hSc : DynamicSemantics.Update.Fixes φ (Sc φ')) : DynamicSemantics.Update.Fixes φ (semDEC φ_DC φ' Sc)

The model M₁ (§3.3.2)

inductive Hofmann2025.World : Type

The four worlds have a bathroom that is upstairs, a bathroom that is not, no bathroom and something upstairs, and neither.

• w_bu : World
• w_b : World
• w_u : World
• w_0 : World

@[instance_reducible]

instance Hofmann2025.instDecidableEqWorld : DecidableEq World

Equations

• Hofmann2025.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Hofmann2025.Ent : Type

The one entity of the model, the bathroom.

• b : Ent

@[instance_reducible]

instance Hofmann2025.instDecidableEqEnt : DecidableEq Ent

Equations

• Hofmann2025.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hofmann2025.bathroom : Ent → World → Prop

b is a bathroom in the two bathroom worlds.

Equations

• Hofmann2025.bathroom Hofmann2025.Ent.b Hofmann2025.World.w_bu = True
• Hofmann2025.bathroom Hofmann2025.Ent.b Hofmann2025.World.w_b = True
• Hofmann2025.bathroom Hofmann2025.Ent.b x✝ = False

def Hofmann2025.upstairs : Ent → World → Prop

b is upstairs in the two upstairs worlds.

Equations

• Hofmann2025.upstairs Hofmann2025.Ent.b Hofmann2025.World.w_bu = True
• Hofmann2025.upstairs Hofmann2025.Ent.b Hofmann2025.World.w_u = True
• Hofmann2025.upstairs Hofmann2025.Ent.b x✝ = False

def Hofmann2025.bathroomRef : World → Option Ent

The individual dref of the bathroom, defined exactly in the bathroom worlds.

Equations

• Hofmann2025.bathroomRef Hofmann2025.World.w_bu = some Hofmann2025.Ent.b
• Hofmann2025.bathroomRef Hofmann2025.World.w_b = some Hofmann2025.Ent.b
• Hofmann2025.bathroomRef x✝ = none

def Hofmann2025.φ₁ : ICDRT.PVar

The propositional drefs of the derivations are the assertion's context and the contexts of embedded clauses.

Equations

• Hofmann2025.φ₁ = { idx := 1 }

def Hofmann2025.φ₂ : ICDRT.PVar

Equations

• Hofmann2025.φ₂ = { idx := 2 }

def Hofmann2025.φ₃ : ICDRT.PVar

Equations

• Hofmann2025.φ₃ = { idx := 3 }

def Hofmann2025.φ₄ : ICDRT.PVar

Equations

• Hofmann2025.φ₄ = { idx := 4 }

def Hofmann2025.φDC : ICDRT.PVar

The commitment set of the speaker S.

Equations

• Hofmann2025.φDC = { idx := 10 }

def Hofmann2025.φDCA : ICDRT.PVar

The commitment sets of the interlocutors A and B of §4.3.

Equations

• Hofmann2025.φDCA = { idx := 11 }

def Hofmann2025.φDCB : ICDRT.PVar

Equations

• Hofmann2025.φDCB = { idx := 12 }

def Hofmann2025.υ : ICDRT.IVar

The individual dref of the indefinite.

Equations

• Hofmann2025.υ = { idx := 0 }

def Hofmann2025.null : ICDRT.State World Ent

The null assignment (32) has no referents and no information.

Equations

• Hofmann2025.null = { indiv := fun (x : ICDRT.IVar) (x_1 : Hofmann2025.World) => none, prop := fun (x : ICDRT.PVar) => Set.univ }

def Hofmann2025.init (dc : Set World) : ICDRT.State World Ent

An initial state (33) of a single speaker whose commitment set is dc.

Equations

• Hofmann2025.init dc = Hofmann2025.null.updateProp Hofmann2025.φDC dc

def Hofmann2025.init₂ (dcA dcB : Set World) : ICDRT.State World Ent

An initial state of the two interlocutors of §4.3.

Equations

• Hofmann2025.init₂ dcA dcB = (Hofmann2025.null.updateProp Hofmann2025.φDCA dcA).updateProp Hofmann2025.φDCB dcB

def Hofmann2025.thereIsABathroom : SemW World Ent

There is a bathroom (24) is the indefinite with the noun as restrictor and a vacuous scope.

Equations

• Hofmann2025.thereIsABathroom = Hofmann2025.indefinite Hofmann2025.υ (Hofmann2025.commonNoun Hofmann2025.bathroom) Hofmann2025.vacuousScope

def Hofmann2025.itIsUpstairs : SemW World Ent

It is upstairs (30) is the pronoun with the verb phrase.

Equations

• Hofmann2025.itIsUpstairs = Hofmann2025.pronoun Hofmann2025.υ (Hofmann2025.intransVP Hofmann2025.upstairs)

theorem Hofmann2025.thereIsABathroom_fixes (φ φ' : ICDRT.PVar) : DynamicSemantics.Update.Fixes φ (thereIsABathroom φ')

theorem Hofmann2025.itIsUpstairs_fixes (φ φ' : ICDRT.PVar) : DynamicSemantics.Update.Fixes φ (itIsUpstairs φ')

theorem Hofmann2025.thereIsABathroom_output {φ : ICDRT.PVar} {k j : ICDRT.State World Ent} (h : (k, j) ∈ thereIsABathroom φ) : (∀ (w : World), w ∈ j.prop φ ↔ j.indiv υ w ≠ none) ∧ j.prop φ ⊆ {World.w_bu, World.w_b}

In the output of an assertion with thereIsABathroom as its clause, the dref is defined in the bathroom worlds of the context, and the context is in the bathroom worlds.

theorem Hofmann2025.itIsUpstairs_output {φ : ICDRT.PVar} {k j : ICDRT.State World Ent} (h : (k, j) ∈ itIsUpstairs φ) : k = j ∧ ∀ w ∈ j.prop φ, j.indiv υ w ≠ none ∧ w ∈ {World.w_bu, World.w_u}

In the output of an assertion with itIsUpstairs as its clause, the dref is defined and upstairs throughout the context.

The veridical discourse (19a) and (30), Figures 5 and 6

def Hofmann2025.veridical : DynamicSemantics.Update (ICDRT.State World Ent)

There is a bathroom. It is upstairs.

Equations

• Hofmann2025.veridical = SetRel.comp (Hofmann2025.semDEC Hofmann2025.φDC Hofmann2025.φ₁ Hofmann2025.thereIsABathroom) (Hofmann2025.semDEC Hofmann2025.φDC Hofmann2025.φ₃ Hofmann2025.itIsUpstairs)

def Hofmann2025.j₆ : ICDRT.State World Ent

The output of Figure 6.

Equations

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

theorem Hofmann2025.veridical_run : (init {World.w_bu}, j₆) ∈ veridical

Figure 6 is an output of the veridical discourse from the initial state whose commitment set it shows.

theorem Hofmann2025.veridical_veridicalIndiv : VeridicalIndiv φDC υ j₆

The dref is veridical, entailed in the speaker's commitment set.

theorem Hofmann2025.veridical_accessible : Accessible φ₃ υ φDC j₆

The veridical anaphor is accessible (Figure 6).

theorem Hofmann2025.veridical_maximal (dc : Set World) (h : ICDRT.State World Ent) (hrun : (init dc, h) ∈ veridical) : ¬j₆.prop φDC ⊂ h.prop φDC

Under pragmatic maximization (35) the commitment set of Figure 6 is maximal among the outputs of the discourse from any initial state, since every output commits the speaker to the bathroom being upstairs.

The negated antecedent (41), Figure 7

def Hofmann2025.negated : DynamicSemantics.Update (ICDRT.State World Ent)

There isn't a bathroom.

Equations

• Hofmann2025.negated = Hofmann2025.semDEC Hofmann2025.φDC Hofmann2025.φ₁ (Hofmann2025.semNOT Hofmann2025.φ₂ Hofmann2025.thereIsABathroom)

def Hofmann2025.j₇ : ICDRT.State World Ent

The output of Figure 7, the first row of Table 3.

Equations

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

theorem Hofmann2025.negated_run : (init {World.w_u, World.w_0}, j₇) ∈ negated

theorem Hofmann2025.negated_counterfactualIndiv : CounterfactualIndiv φDC υ j₇

The dref is counterfactual, undefined throughout the speaker's commitment set.

theorem Hofmann2025.negated_isComplement : j₇ ∈ ICDRT.eqCompl φ₁ φ₂

The assertion's context is the complement of the prejacent's.

theorem Hofmann2025.negated_counterfactualProp {i j : ICDRT.State World Ent} (h : (i, j) ∈ negated) : CounterfactualProp φDC φ₂ j

Every output of (41) makes the prejacent counterfactual, since the commitments entail the assertion's context, the complement of the prejacent's.

theorem Hofmann2025.counterfactual_veridical_impossible (j : ICDRT.State World Ent) (hDC : j.prop φDC = j₇.prop φDC) (hφ₂ : j.prop φ₂ = j₇.prop φ₂) (hdec : j ∈ ICDRT.incl φDC φ₃) (hsub : j ∈ ICDRT.incl φ₃ φ₂) : ¬(j.prop φDC).Nonempty

No consistent extension of Figure 7 admits the veridical anaphor (30), since a context the commitments entail that lies within the prejacent's context empties the commitment set (§3.4.2).

def Hofmann2025.jRow4 : ICDRT.State World Ent

The last row of Table 3, with the prejacent's context empty and the dref nowhere defined, is also an output of (41), since the printed maximization does not exclude it.

Equations

• Hofmann2025.jRow4 = ((Hofmann2025.init Set.univ).updateProp Hofmann2025.φ₁ Set.univ).updateProp Hofmann2025.φ₂ ∅

theorem Hofmann2025.negated_row4 : (init Set.univ, jRow4) ∈ negated

theorem Hofmann2025.negated_max : (init {World.w_u, World.w_0}, j₇) ∈ DynamicSemantics.Update.maxAt φ₂ negated

Maximizing the prejacent's context over the whole assertion selects Figure 7, since every output from the same initial state keeps that context within the bathroom worlds.

Double negation (43), Figure 8

def Hofmann2025.doubleNeg : DynamicSemantics.Update (ICDRT.State World Ent)

It's not the case that there isn't a bathroom.

Equations

• Hofmann2025.doubleNeg = Hofmann2025.semDEC Hofmann2025.φDC Hofmann2025.φ₁ (Hofmann2025.semNOT Hofmann2025.φ₂ (Hofmann2025.semNOT Hofmann2025.φ₃ Hofmann2025.thereIsABathroom))

def Hofmann2025.j₈ : ICDRT.State World Ent

The output of Figure 8.

Equations

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

theorem Hofmann2025.doubleNeg_run : (init {World.w_bu, World.w_b}, j₈) ∈ doubleNeg

theorem Hofmann2025.doubleNeg_prop_eq : j₈.prop φ₁ = j₈.prop φ₃

Double complementation returns the assertion's context to the innermost one.

theorem Hofmann2025.doubleNeg_veridicalIndiv : VeridicalIndiv φDC υ j₈

The doubly negated dref is veridical.

theorem Hofmann2025.doubleNeg_accessible : Accessible φ₃ υ φDC j₈

The veridical anaphor is accessible after double negation (§4.1).

The bathroom disjunction (44), Figure 9

def Hofmann2025.bathDisj : DynamicSemantics.Update (ICDRT.State World Ent)

Either there isn't a bathroom, or it's upstairs.

Equations

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

def Hofmann2025.j₉ : ICDRT.State World Ent

The output of Figure 9.

Equations

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

theorem Hofmann2025.bathDisj_run : (init {World.w_bu, World.w_u, World.w_0}, j₉) ∈ bathDisj

theorem Hofmann2025.bathDisj_union : j₉.prop φ₁ = j₉.prop φ₂ ∪ j₉.prop φ₃

The disjunction's context is the union of the disjuncts' contexts.

theorem Hofmann2025.bathDisj_accessible : Accessible φ₃ υ φDC j₉

The dref is counterfactual for the speaker yet accessible in the second disjunct (§4.2), since the disjuncts' contexts need not overlap the commitment set.

Disagreement (47) and (48), Figure 10

def Hofmann2025.disagree : DynamicSemantics.Update (ICDRT.State World Ent)

Speaker A says There isn't a bathroom and speaker B says It is upstairs.

Equations

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

def Hofmann2025.j₁₀ : ICDRT.State World Ent

The output of Figure 10.

Equations

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

theorem Hofmann2025.disagree_run : (init₂ {World.w_u, World.w_0} {World.w_bu}, j₁₀) ∈ disagree

theorem Hofmann2025.disagree_counterfactual_A : CounterfactualIndiv φDCA υ j₁₀

The dref is counterfactual for A.

theorem Hofmann2025.disagree_veridical_B : VeridicalIndiv φDCB υ j₁₀

The same dref is veridical for B.

theorem Hofmann2025.disagree_accessible : (j₁₀.prop φDCA).Nonempty ∧ Accessible φ₃ υ φDCB j₁₀

Both interlocutors keep consistent commitments although they contradict each other, and B's anaphor is accessible (§4.3).