Hofmann (2025): Anaphoric Accessibility with Flat Update

@cite{hofmann-2025}

Formalizes the core empirical and theoretical contributions of @cite{hofmann-2025}'s unified account of anaphoric accessibility.

Core Claim

Anaphoric accessibility is governed by veridicality — speaker commitments about discourse referents — not by structural scope. Indefinites under nonveridical operators introduce drefs globally (flat update), and constraints on anaphora emerge from two principles:

1. Local contextual entailment: a dref's referent must exist throughout the pronoun's local context.
2. Discourse consistency: the speaker's commitment set must remain non-empty after the update.

Phenomena Unified

The paper provides a single analysis for four previously disparate patterns of anaphora to negated antecedents:

• Double negation (@cite{krahmer-muskens-1995}): "It's not the case that there isn't a bathroom. It's upstairs."
• Bathroom disjunctions (@cite{roberts-1989}): "Either there isn't a bathroom, or it's upstairs."
• Disagreement (@cite{hofmann-2019}): A: "There isn't a bathroom." B: "It's upstairs."
• Modal subordination (@cite{frank-1996}, @cite{roberts-1989}): "There isn't a bathroom. It would be upstairs."

Theoretical Framework

The analysis is implemented in Intensional CDRT (ICDRT), extending @cite{muskens-1996}'s Compositional DRT with intensionality and propositional drefs, following @cite{stone-1999} and @cite{brasoveanu-2006}'s flat-update approach. Generic ICDRT infrastructure (assignments, updates, variable updates, dynamic conditions, predication, veridicality typology, multi-agent discourse contexts, maximization) lives in Dynamic/Core/Intensional.lean; this file owns Hofmann's Appendix C compositional fragment and the empirical applications.

Structure of this file

1. Empirical data (§1): AccessDatum entries with felicity judgments
2. Concrete model M₁ (§2): The 4-world model from the paper
3. End-to-end derivations (§3): Accessibility derived from ICDRT operators
4. Accessibility predictions (§4): The classification, verified against derivations
5. Per-datum verification (§5)
6. Compositional fragment (§6): Hofmann's Appendix C lexical entries
7. Comparison with Bilateral Update Semantics (§7): @cite{hofmann-2025} §5.1.1 — where ICDRT covers cases that bilateral accounts (BUS, @cite{krahmer-muskens-1995}, @cite{elliott-sudo-2025}) cannot.

def Hofmann2025.Examples.veridical_basic : Data.Examples.LinguisticExample

Equations

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

def Hofmann2025.Examples.negated_basic : Data.Examples.LinguisticExample

Equations

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

def Hofmann2025.Examples.double_negation : Data.Examples.LinguisticExample

Equations

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

def Hofmann2025.Examples.modal_subordination : Data.Examples.LinguisticExample

Equations

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

def Hofmann2025.Examples.counterfactual_modal : Data.Examples.LinguisticExample

Equations

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

def Hofmann2025.Examples.all : List Data.Examples.LinguisticExample

Equations

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

inductive Hofmann2025.DrefStatus : Type

Epistemic status of a discourse referent relative to a speaker.

• veridical : DrefStatus
• hypothetical : DrefStatus
• counterfactual : DrefStatus

@[implicit_reducible]

instance Hofmann2025.instDecidableEqDrefStatus : DecidableEq DrefStatus

Equations

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

def Hofmann2025.instReprDrefStatus.repr : DrefStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hofmann2025.instReprDrefStatus : Repr DrefStatus

Equations

• Hofmann2025.instReprDrefStatus = { reprPrec := Hofmann2025.instReprDrefStatus.repr }

inductive Hofmann2025.AnaphorContext : Type

Veridicality of the anaphor's embedding context.

• veridical : AnaphorContext
• nonveridical : AnaphorContext

@[implicit_reducible]

instance Hofmann2025.instDecidableEqAnaphorContext : DecidableEq AnaphorContext

Equations

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

@[implicit_reducible]

instance Hofmann2025.instReprAnaphorContext : Repr AnaphorContext

Equations

• Hofmann2025.instReprAnaphorContext = { reprPrec := Hofmann2025.instReprAnaphorContext.repr }

def Hofmann2025.instReprAnaphorContext.repr : AnaphorContext → ℕ → Std.Format

Equations

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

structure Hofmann2025.AccessDatum : Type

An empirical datum on anaphoric accessibility.

• label : String
• antecedentSentence : String
• anaphorSentence : String
• antecedentStatus : DrefStatus
• anaphorCtx : AnaphorContext
• felicitous : Bool
• source : String

def Hofmann2025.instReprAccessDatum.repr : AccessDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hofmann2025.instReprAccessDatum : Repr AccessDatum

Equations

• Hofmann2025.instReprAccessDatum = { reprPrec := Hofmann2025.instReprAccessDatum.repr }

def Hofmann2025.veridicalBasic : AccessDatum

(1a): "Mary owns a car. It is red." @cite{hofmann-2025}

Equations

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

def Hofmann2025.negatedBasic : AccessDatum

(1b): "Mary doesn't own a car. #It is red." @cite{hofmann-2025}

Equations

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

def Hofmann2025.doubleNegation : AccessDatum

(2a)/(42a): Double negation. @cite{krahmer-muskens-1995}

Equations

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

def Hofmann2025.bathroomDisjunction : AccessDatum

(2b)/(42b): Bathroom disjunction. @cite{roberts-1989}

Equations

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

def Hofmann2025.disagreement : AccessDatum

(2c)/(42c): Disagreement. @cite{hofmann-2019}

Equations

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

def Hofmann2025.modalSubordination : AccessDatum

(2d)/(42d): Modal subordination. @cite{frank-1996}

Equations

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

def Hofmann2025.negatedFactive : AccessDatum

(5a): Negated factive. @cite{karttunen-1976}

Equations

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

def Hofmann2025.negativeImplicative : AccessDatum

(5b): Negative implicative. @cite{karttunen-1976}

Equations

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

def Hofmann2025.counterfactualVeridical : AccessDatum

Equations

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

def Hofmann2025.counterfactualModal : AccessDatum

Equations

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

def Hofmann2025.counterfactualConcessive : AccessDatum

Equations

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

def Hofmann2025.wolfIndicative : AccessDatum

Equations

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

def Hofmann2025.wolfWould : AccessDatum

Equations

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

def Hofmann2025.negationBlocks : AccessDatum

Equations

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

def Hofmann2025.conjunctionBlocks : AccessDatum

Equations

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

def Hofmann2025.wrongOrderBathroom : AccessDatum

Equations

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

Model M₁

The paper works through all derivations on a concrete model M₁ with four possible worlds and a single bathroom entity b.

• w_bu: bathroom exists AND is upstairs
• w_b: bathroom exists, NOT upstairs
• w_u: no bathroom, but "upstairs" is true (vacuously; no entity)
• w_0: no bathroom, "upstairs" is false

Entities: {b} (the bathroom). The universal falsifier ⋆ is modeled by Entity.star.

inductive Hofmann2025.BWorld : Type

Possible worlds in model M₁.

• w_bu : BWorld
• w_b : BWorld
• w_u : BWorld
• w_0 : BWorld

@[implicit_reducible]

instance Hofmann2025.instDecidableEqBWorld : DecidableEq BWorld

Equations

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

@[implicit_reducible]

instance Hofmann2025.instReprBWorld : Repr BWorld

Equations

• Hofmann2025.instReprBWorld = { reprPrec := Hofmann2025.instReprBWorld.repr }

def Hofmann2025.instReprBWorld.repr : BWorld → ℕ → Std.Format

Equations

• Hofmann2025.instReprBWorld.repr Hofmann2025.BWorld.w_bu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hofmann2025.BWorld.w_bu")).group prec✝
• Hofmann2025.instReprBWorld.repr Hofmann2025.BWorld.w_b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hofmann2025.BWorld.w_b")).group prec✝
• Hofmann2025.instReprBWorld.repr Hofmann2025.BWorld.w_u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hofmann2025.BWorld.w_u")).group prec✝
• Hofmann2025.instReprBWorld.repr Hofmann2025.BWorld.w_0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hofmann2025.BWorld.w_0")).group prec✝

inductive Hofmann2025.BEnt : Type

Entities in model M₁ (just the bathroom b).

• b : BEnt

@[implicit_reducible]

instance Hofmann2025.instDecidableEqBEnt : DecidableEq BEnt

Equations

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

@[implicit_reducible]

instance Hofmann2025.instReprBEnt : Repr BEnt

Equations

• Hofmann2025.instReprBEnt = { reprPrec := Hofmann2025.instReprBEnt.repr }

def Hofmann2025.instReprBEnt.repr : BEnt → ℕ → Std.Format

Equations

• Hofmann2025.instReprBEnt.repr Hofmann2025.BEnt.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hofmann2025.BEnt.b")).group prec✝

def Hofmann2025.isBathroom : BEnt → BWorld → Prop

b is a bathroom in w_bu and w_b.

Equations

• Hofmann2025.isBathroom Hofmann2025.BEnt.b Hofmann2025.BWorld.w_bu = True
• Hofmann2025.isBathroom Hofmann2025.BEnt.b Hofmann2025.BWorld.w_b = True
• Hofmann2025.isBathroom x✝¹ x✝ = False

def Hofmann2025.isUpstairs : BEnt → BWorld → Prop

b is upstairs in w_bu and w_u.

Equations

• Hofmann2025.isUpstairs Hofmann2025.BEnt.b Hofmann2025.BWorld.w_bu = True
• Hofmann2025.isUpstairs Hofmann2025.BEnt.b Hofmann2025.BWorld.w_u = True
• Hofmann2025.isUpstairs x✝¹ x✝ = False

def Hofmann2025.p1 : Semantics.Dynamic.Core.PVar

Equations

• Hofmann2025.p1 = { idx := 0 }

def Hofmann2025.p2 : Semantics.Dynamic.Core.PVar

Equations

• Hofmann2025.p2 = { idx := 1 }

def Hofmann2025.p3 : Semantics.Dynamic.Core.PVar

Equations

• Hofmann2025.p3 = { idx := 2 }

def Hofmann2025.p4 : Semantics.Dynamic.Core.PVar

Equations

• Hofmann2025.p4 = { idx := 3 }

def Hofmann2025.pDC_S : Semantics.Dynamic.Core.PVar

Equations

• Hofmann2025.pDC_S = { idx := 10 }

def Hofmann2025.pDC_A : Semantics.Dynamic.Core.PVar

Equations

• Hofmann2025.pDC_A = { idx := 11 }

def Hofmann2025.pDC_B : Semantics.Dynamic.Core.PVar

Equations

• Hofmann2025.pDC_B = { idx := 12 }

def Hofmann2025.v1 : Semantics.Dynamic.Core.IVar

Equations

• Hofmann2025.v1 = { idx := 0 }

def Hofmann2025.indivBathroom : Semantics.Dynamic.Core.IVar → BWorld → Semantics.Dynamic.Core.Entity BEnt

Individual dref assignment for the bathroom model: v₁ maps to b in bathroom worlds (w_bu, w_b), ⋆ elsewhere. All other variables map to ⋆.

Equations

• Hofmann2025.indivBathroom { idx := 0 } Hofmann2025.BWorld.w_bu = Semantics.Dynamic.Core.Entity.some Hofmann2025.BEnt.b
• Hofmann2025.indivBathroom { idx := 0 } Hofmann2025.BWorld.w_b = Semantics.Dynamic.Core.Entity.some Hofmann2025.BEnt.b
• Hofmann2025.indivBathroom x✝¹ x✝ = Semantics.Dynamic.Core.Entity.star

Derivations from ICDRT operators

Each derivation constructs the output assignment j from the paper's figures, defines the ICDRT update as a static relation (Definition 17), then proves the accessibility prediction follows from Definition 38: local contextual entailment + discourse consistency.

"There is a bathroom. It is upstairs." (§3.3, Figures 5–6)

After (19a) + (30):

• φ₁(j) = φ_{DC_S}(j) = {w_bu, w_b}
• φ₃(j) = {w_bu}
• v maps w_bu → b, w_b → b, else ⋆
• v is veridical, discourse consistent, v entailed in φ₃

def Hofmann2025.j_veridical : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEnt

Output assignment after "There is a bathroom. It is upstairs." (Figure 6)

Equations

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

def Hofmann2025.update_19a : Semantics.Dynamic.Core.ICDRTUpdate BWorld BEnt

The update (19a): [φ₁, φ₁ : v | φ_{DC_S} ∈ φ₁, bathroom_{φ₁}(v)]

Equations

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

def Hofmann2025.update_30 : Semantics.Dynamic.Core.ICDRTUpdate BWorld BEnt

The update (30): [φ₃ | φ_{DC_S} ∈ φ₃, upstairs_{φ₃}(v)]

Equations

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

theorem Hofmann2025.veridical_v_is_veridical : Semantics.Dynamic.Core.veridicalIndiv pDC_S v1 j_veridical

v₁ is veridical at j_veridical: exists in all φ_{DC_S}-worlds.

theorem Hofmann2025.veridical_consistent : j_veridical⟦pDC_S⟧ₚ.Nonempty

Discourse is consistent at j_veridical.

theorem Hofmann2025.veridical_entailed_in_p3 : Semantics.Dynamic.Core.localEntailment p3 v1 j_veridical

v₁ is locally entailed in φ₃ at j_veridical.

theorem Hofmann2025.veridical_anaphor_accessible : Semantics.Dynamic.Core.accessible p3 v1 pDC_S j_veridical

Veridical anaphor is accessible (Definition 38).

"There isn't a bathroom. #It is upstairs." (§3.4, Figure 7)

After (19b):

• φ₂(j) = {w_bu, w_b}, φ₁(j) = {w_u, w_0} = φ̄₂
• φ_{DC_S}(j) = {w_u, w_0} ⊆ φ₁
• v maps w_bu → b, w_b → b, else ⋆
• v is counterfactual (⋆ in all DC worlds)

Attempting (30) requires φ₃ ⊆ φ₂ (subset requirement) AND φ_{DC_S} ⊆ φ₃ (DEC). But φ_{DC_S} ∩ φ₂ = ∅ → contradiction.

def Hofmann2025.j_counterfactual : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEnt

Output assignment after "There isn't a bathroom" (Figure 7).

Equations

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

theorem Hofmann2025.counterfactual_v_is_cf : Semantics.Dynamic.Core.counterfactualIndiv pDC_S v1 j_counterfactual

v₁ is counterfactual at j_counterfactual.

theorem Hofmann2025.counterfactual_complement : Semantics.Dynamic.Core.isComplement p1 p2 j_counterfactual

φ₁ is the complement of φ₂ at j_counterfactual (NOT condition).

theorem Hofmann2025.counterfactual_veridical_impossible (j : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEnt) (h_extends : ∀ (p : Semantics.Dynamic.Core.PVar), p ≠ p3 → j⟦p⟧ₚ = j_counterfactual⟦p⟧ₚ) (_h_indiv : j.indiv = j_counterfactual.indiv) (h_dec : Semantics.Dynamic.Core.decCondition pDC_S p3 j) (h_subset : Semantics.Dynamic.Core.subsetReq p3 p2 j) (_h_entailed : Semantics.Dynamic.Core.localEntailment p3 v1 j) : ¬j⟦pDC_S⟧ₚ.Nonempty

Veridical anaphor fails: no consistent, locally-entailing extension of j_counterfactual with φ₃ exists.

Any j extending j_counterfactual that satisfies both φ_{DC_S} ⊆ φ₃ (DEC) and φ₃ ⊆ φ₂ (subset requirement) must have φ_{DC_S} ⊆ φ₂, but φ_{DC_S} ∩ φ₂ = ∅.

Re-derived as a corollary of the typeclass theorem Semantics.Dynamic.Context.counterfactual_blocks_veridical: the only paper-specific work is the disjointness witness h_disjoint. The ICDRT-specific extension/DEC/subset structure is fully delegated to the abstract theorem via the HasPropDrefs (ICDRTAssignment BWorld BEnt) PVar BWorld instance.

"It's not the case that there isn't a bathroom." (§4.1, Figure 8)

DRS (43): DEC_S(NOT(NOT(there is [a bathroom]^v)))

Double complementation: φ₁ ≡ φ̄₂, φ₂ ≡ φ̄₃ ⟹ φ₁ = φ₃. The dref v is introduced relative to φ₃ = φ₁ = {w_bu, w_b}. Since φ_{DC_S} ⊆ φ₁ = φ₃, v is veridical.

def Hofmann2025.j_double_neg : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEnt

Output after double negation (Figure 8).

Equations

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

theorem Hofmann2025.double_neg_phi1_eq_phi3 : j_double_neg⟦p1⟧ₚ = j_double_neg⟦p3⟧ₚ

φ₁ = φ₃ via double complementation: the key structural result.

theorem Hofmann2025.double_neg_complement_conditions : Semantics.Dynamic.Core.isComplement p1 p2 j_double_neg ∧ Semantics.Dynamic.Core.isComplement p2 p3 j_double_neg

NOT conditions hold: φ₁ ≡ φ̄₂ and φ₂ ≡ φ̄₃.

theorem Hofmann2025.double_neg_v_veridical : Semantics.Dynamic.Core.veridicalIndiv pDC_S v1 j_double_neg

v₁ is veridical after double negation.

theorem Hofmann2025.double_neg_accessible : Semantics.Dynamic.Core.accessible p3 v1 pDC_S j_double_neg

Double negation: anaphora accessible.

"Either there isn't a bathroom, or it's upstairs." (§4.2, Figure 9)

DRS (44): φ₁ ≡ φ₂ ∪ φ₃ (disjunction). The second disjunct φ₃ = {w_bu} is the local context for the pronoun. v exists in φ₃ (v(w_bu) = b ≠ ⋆). Disjunction does NOT require overlap between disjunct propositions, so φ₃ ⊆ φ₄ (bathroom worlds) is compatible with φ₂ (no-bathroom worlds) being disjoint from φ₃.

def Hofmann2025.j_bathroom_disj : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEnt

Output after bathroom disjunction (Figure 9).

Equations

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

theorem Hofmann2025.bathroom_disj_union : j_bathroom_disj⟦p1⟧ₚ = j_bathroom_disj⟦p2⟧ₚ ∪ j_bathroom_disj⟦p3⟧ₚ

φ₁ = φ₂ ∪ φ₃ (disjunction condition).

theorem Hofmann2025.bathroom_disj_complement : Semantics.Dynamic.Core.isComplement p2 p4 j_bathroom_disj

φ₂ = φ̄₄ (negation in first disjunct).

theorem Hofmann2025.bathroom_disj_accessible : Semantics.Dynamic.Core.accessible p3 v1 pDC_S j_bathroom_disj

Bathroom disjunction: anaphora accessible. v₁ is locally entailed in φ₃ = {w_bu} and discourse is consistent.

A: "There isn't a bathroom." B: "It is upstairs." (§4.3, Figure 10)

This is the critical case that bilateral accounts (DN-DRT/BUS) CANNOT handle (§5.1.1). ICDRT handles it because different speakers have separate commitment sets.

(47) A's assertion: constrains φ_{DC_A}, introduces v counterfactually. (48) B's assertion: constrains φ_{DC_B}, v is locally entailed in φ₃. Both commitment sets nonempty → discourse consistent despite contradiction.

def Hofmann2025.j_disagreement : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEnt

Output after disagreement (Figure 10).

Equations

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

theorem Hofmann2025.disagreement_v_cf_for_A : Semantics.Dynamic.Core.counterfactualIndiv pDC_A v1 j_disagreement

v₁ is counterfactual for A.

theorem Hofmann2025.disagreement_v_veridical_for_B : Semantics.Dynamic.Core.veridicalIndiv pDC_B v1 j_disagreement

v₁ is veridical for B.

theorem Hofmann2025.disagreement_consistent : j_disagreement⟦pDC_A⟧ₚ.Nonempty ∧ j_disagreement⟦pDC_B⟧ₚ.Nonempty

Both commitment sets are nonempty → discourse is consistent.

theorem Hofmann2025.disagreement_accessible : Semantics.Dynamic.Core.accessible p3 v1 pDC_B j_disagreement

Disagreement: anaphora accessible for B. Impossible in bilateral accounts (§5.1.1) — they require a single negation swap, but here A and B have contradictory commitments.

"There isn't a bathroom. Sue believes it's upstairs." (§4.4)

(51a): DEC_S(NOT(there is [a bathroom]^v)) — v counterfactual for S (51b): DEC_S(Sue believes(it_v is upstairs)) — believe provides nonveridical local context φ₄ for the pronoun.

v is locally entailed in φ₄ ⊆ φ₂ (bathroom-worlds), which need not overlap with φ_{DC_S}. Discourse consistent: φ_{DC_S} ≠ ∅.

Simplification note: The paper's §4.4 uses a richer model M₃ with 8 worlds, entities {b, sue, S, ⋆}, and a believe predicate (Definition 50). We simplify to the 4-world M₁ model where the attitude's embedded content φ₄ = {w_bu} is stipulated directly rather than derived from Sue's doxastic state. This suffices to verify the accessibility prediction (which depends only on φ₄ ⊆ φ₂ and DC consistency, not on how φ₄ is computed). A faithful M₃ model would require adding BWSue (8 worlds), a believe relation, and deriving φ₄ from DOX(sue, φ₃).

def Hofmann2025.p4_modal : Semantics.Dynamic.Core.PVar

Propositional variable for the attitude's embedded content.

Equations

• Hofmann2025.p4_modal = { idx := 4 }

def Hofmann2025.j_modal_sub : Semantics.Dynamic.Core.ICDRTAssignment BWorld BEnt

Output after "There isn't a bathroom. Sue believes it's upstairs."

Equations

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

theorem Hofmann2025.modal_sub_v_cf : Semantics.Dynamic.Core.counterfactualIndiv pDC_S v1 j_modal_sub

v₁ is counterfactual for the speaker.

theorem Hofmann2025.modal_sub_entailed : Semantics.Dynamic.Core.localEntailment p4_modal v1 j_modal_sub

v₁ is locally entailed in the nonveridical context φ₄.

theorem Hofmann2025.modal_sub_accessible : Semantics.Dynamic.Core.accessible p4_modal v1 pDC_S j_modal_sub

Modal subordination: anaphora accessible in nonveridical context. The pronoun resolves in Sue's doxastic state, not the speaker's commitment set.

Accessibility generalization (7)

The paper's core empirical generalization (@cite{hofmann-2025}, (7)):

A dref is accessible iff it is veridical OR the anaphor occurs in a nonveridical context.

This is encoded directly as accessiblePred and verified against each phenomenon via ICDRT derivations with zero sorry:

• Veridical → accessible: veridical_anaphor_accessible (§3.1)
• Counterfactual + veridical → inaccessible: counterfactual_veridical_impossible (§3.2)
• Double negation → restores veridicality: double_neg_accessible (§3.3)
• Counterfactual + nonveridical → accessible: bathroom_disj_accessible (§3.4), disagreement_accessible (§3.5), modal_sub_accessible (§3.6)

def Hofmann2025.accessiblePred (status : DrefStatus) (ctx : AnaphorContext) : Bool

The accessibility generalization (@cite{hofmann-2025}, (7)): accessible iff veridical OR nonveridical anaphor context.

Equations

• Hofmann2025.accessiblePred Hofmann2025.DrefStatus.veridical ctx = true
• Hofmann2025.accessiblePred Hofmann2025.DrefStatus.hypothetical Hofmann2025.AnaphorContext.nonveridical = true
• Hofmann2025.accessiblePred Hofmann2025.DrefStatus.counterfactual Hofmann2025.AnaphorContext.nonveridical = true
• Hofmann2025.accessiblePred Hofmann2025.DrefStatus.hypothetical Hofmann2025.AnaphorContext.veridical = false
• Hofmann2025.accessiblePred Hofmann2025.DrefStatus.counterfactual Hofmann2025.AnaphorContext.veridical = false

theorem Hofmann2025.veridicalBasic_correct : accessiblePred veridicalBasic.antecedentStatus veridicalBasic.anaphorCtx = veridicalBasic.felicitous

theorem Hofmann2025.negatedBasic_correct : accessiblePred negatedBasic.antecedentStatus negatedBasic.anaphorCtx = negatedBasic.felicitous

theorem Hofmann2025.doubleNegation_correct : accessiblePred doubleNegation.antecedentStatus doubleNegation.anaphorCtx = doubleNegation.felicitous

theorem Hofmann2025.bathroomDisjunction_correct : accessiblePred bathroomDisjunction.antecedentStatus bathroomDisjunction.anaphorCtx = bathroomDisjunction.felicitous

theorem Hofmann2025.disagreement_correct : accessiblePred disagreement.antecedentStatus disagreement.anaphorCtx = disagreement.felicitous

theorem Hofmann2025.modalSubordination_correct : accessiblePred modalSubordination.antecedentStatus modalSubordination.anaphorCtx = modalSubordination.felicitous

theorem Hofmann2025.negatedFactive_correct : accessiblePred negatedFactive.antecedentStatus negatedFactive.anaphorCtx = negatedFactive.felicitous

theorem Hofmann2025.negativeImplicative_correct : accessiblePred negativeImplicative.antecedentStatus negativeImplicative.anaphorCtx = negativeImplicative.felicitous

theorem Hofmann2025.counterfactualVeridical_correct : accessiblePred counterfactualVeridical.antecedentStatus counterfactualVeridical.anaphorCtx = counterfactualVeridical.felicitous

theorem Hofmann2025.counterfactualModal_correct : accessiblePred counterfactualModal.antecedentStatus counterfactualModal.anaphorCtx = counterfactualModal.felicitous

theorem Hofmann2025.counterfactualConcessive_correct : accessiblePred counterfactualConcessive.antecedentStatus counterfactualConcessive.anaphorCtx = counterfactualConcessive.felicitous

theorem Hofmann2025.wolfIndicative_correct : accessiblePred wolfIndicative.antecedentStatus wolfIndicative.anaphorCtx = wolfIndicative.felicitous

theorem Hofmann2025.wolfWould_correct : accessiblePred wolfWould.antecedentStatus wolfWould.anaphorCtx = wolfWould.felicitous

theorem Hofmann2025.negationBlocks_correct : accessiblePred negationBlocks.antecedentStatus negationBlocks.anaphorCtx = negationBlocks.felicitous

theorem Hofmann2025.conjunctionBlocks_correct : accessiblePred conjunctionBlocks.antecedentStatus conjunctionBlocks.anaphorCtx = conjunctionBlocks.felicitous

theorem Hofmann2025.wrongOrderBathroom_correct : accessiblePred wrongOrderBathroom.antecedentStatus wrongOrderBathroom.anaphorCtx = wrongOrderBathroom.felicitous

theorem Hofmann2025.all_data_correct : accessiblePred veridicalBasic.antecedentStatus veridicalBasic.anaphorCtx = veridicalBasic.felicitous ∧ accessiblePred negatedBasic.antecedentStatus negatedBasic.anaphorCtx = negatedBasic.felicitous ∧ accessiblePred doubleNegation.antecedentStatus doubleNegation.anaphorCtx = doubleNegation.felicitous ∧ accessiblePred bathroomDisjunction.antecedentStatus bathroomDisjunction.anaphorCtx = bathroomDisjunction.felicitous ∧ accessiblePred disagreement.antecedentStatus disagreement.anaphorCtx = disagreement.felicitous ∧ accessiblePred modalSubordination.antecedentStatus modalSubordination.anaphorCtx = modalSubordination.felicitous ∧ accessiblePred negatedFactive.antecedentStatus negatedFactive.anaphorCtx = negatedFactive.felicitous ∧ accessiblePred negativeImplicative.antecedentStatus negativeImplicative.anaphorCtx = negativeImplicative.felicitous ∧ accessiblePred counterfactualVeridical.antecedentStatus counterfactualVeridical.anaphorCtx = counterfactualVeridical.felicitous ∧ accessiblePred counterfactualModal.antecedentStatus counterfactualModal.anaphorCtx = counterfactualModal.felicitous ∧ accessiblePred counterfactualConcessive.antecedentStatus counterfactualConcessive.anaphorCtx = counterfactualConcessive.felicitous ∧ accessiblePred wolfIndicative.antecedentStatus wolfIndicative.anaphorCtx = wolfIndicative.felicitous ∧ accessiblePred wolfWould.antecedentStatus wolfWould.anaphorCtx = wolfWould.felicitous ∧ accessiblePred negationBlocks.antecedentStatus negationBlocks.anaphorCtx = negationBlocks.felicitous ∧ accessiblePred conjunctionBlocks.antecedentStatus conjunctionBlocks.anaphorCtx = conjunctionBlocks.felicitous ∧ accessiblePred wrongOrderBathroom.antecedentStatus wrongOrderBathroom.anaphorCtx = wrongOrderBathroom.felicitous

All 16 data points match the accessibility prediction.

Lexical entries from Appendix C

Type-driven compositional semantics for ICDRT. Each lexical entry is a higher-order function over dynamic meta-types; composition is function application + sequential update. The resulting ICDRTUpdate values lift to distributive CCPs via Core/Intensional.lean's toDynProp_isDistributive.

Meta-types (Definition 13)

Paper	Lean	Interpretation
e	IVar	Individual dref name
w	PVar	Propositional dref name
t	ICDRTUpdate W E	Static update relation

Compositional types are functions between these: e(wt) = VP type, wt = sentence type, etc.

@[reducible, inline]

abbrev Hofmann2025.SemE (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

VP / predicate type: e(wt) — takes individual dref and local context.

Equations

• Hofmann2025.SemE W E = (Semantics.Dynamic.Core.IVar → Semantics.Dynamic.Core.PVar → Semantics.Dynamic.Core.ICDRTUpdate W E)

@[reducible, inline]

abbrev Hofmann2025.SemW (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Sentence / clause type: wt — takes local context, returns update.

Equations

• Hofmann2025.SemW W E = (Semantics.Dynamic.Core.PVar → Semantics.Dynamic.Core.ICDRTUpdate W E)

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

Vacuous VP scope: identity predicate λv.λφ.idUp. Used when a sentence has no VP beyond the NP (e.g., "there is a bathroom").

Equations

• Hofmann2025.vacuousScope x✝¹ x✝ = Semantics.Dynamic.Core.ICDRTUpdate.idUp

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

(15) Common noun: bathroom ⟿ λv_e.λφ_w.[bathroom_φ(v)]. A test update: assignment unchanged, but R_φ(v) must hold at the output.

Equations

• Hofmann2025.commonNoun R v φ i j = (i = j ∧ Semantics.Dynamic.Core.dynPred R φ v j)

@[reducible, inline]

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

Intransitive VP: structurally identical to commonNoun.

Equations

• Hofmann2025.intransVP R = Hofmann2025.commonNoun R

def Hofmann2025.indefinite {W : Type u_1} {E : Type u_2} (v : Semantics.Dynamic.Core.IVar) (P P' : SemE W E) (φ : Semantics.Dynamic.Core.PVar) : Semantics.Dynamic.Core.ICDRTUpdate W E

(16) Indefinite: a^v ⟿ λP.λP'.λφ.[φ : v]; P(v)(φ); P'(v)(φ).

The biconditional in relVarUp ensures v has a referent exactly in the φ-worlds, preventing scope leakage.

Equations

• Hofmann2025.indefinite v P P' φ = (fun (i j : Semantics.Dynamic.Core.ICDRTAssignment W E) => Semantics.Dynamic.Core.relVarUp φ v i j) ⨟ P v φ ⨟ P' v φ

def Hofmann2025.pronoun {W : Type u_1} {E : Type u_2} (v : Semantics.Dynamic.Core.IVar) (P : SemE W E) (φ : Semantics.Dynamic.Core.PVar) : Semantics.Dynamic.Core.ICDRTUpdate W E

(17) Pronoun: it_v ⟿ λP.λφ.P(v)(φ). The pronoun contributes no update — it simply passes its index v to the predicate.

Equations

• Hofmann2025.pronoun v P φ = P v φ

def Hofmann2025.properName {W : Type u_1} {E : Type u_2} (name : E) (v : Semantics.Dynamic.Core.IVar) (P : SemE W E) (φ : Semantics.Dynamic.Core.PVar) : Semantics.Dynamic.Core.ICDRTUpdate W E

(14) Proper name: Mary ⟿ λP.λφ.[v | v ≡ Mary_e]; P(v)(φ).

Equations

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

def Hofmann2025.semNOT {W : Type u_1} {E : Type u_2} (φ' : Semantics.Dynamic.Core.PVar) (Sc : SemW W E) (φ : Semantics.Dynamic.Core.PVar) : Semantics.Dynamic.Core.ICDRTUpdate W E

(18a) Sentential negation: NOT^{φ'} ⟿ λSc.λφ.[φ' | φ ≡ φ̄']; max_{φ'}(Sc(φ')).

Static complementation over propositional drefs, NOT bilateral swap — the algebraic content of @cite{hofmann-2025}'s key insight (§5.1.1).

Equations

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

def Hofmann2025.semOR {W : Type u_1} {E : Type u_2} (φ' φ'' : Semantics.Dynamic.Core.PVar) (Sc' Sc'' : SemW W E) (φ : Semantics.Dynamic.Core.PVar) : Semantics.Dynamic.Core.ICDRTUpdate W E

(18b) Disjunction: OR^{φ',φ''} ⟿ λSc'.λSc''.λφ.[φ',φ'' | φ ≡ φ'⊎φ'']; max_{φ'}(Sc'(φ')); max_{φ''}(Sc''(φ'')).

The disjuncts' local contexts need NOT overlap — this is how bathroom disjunctions enable cross-disjunct anaphora.

Equations

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

def Hofmann2025.semIF {W : Type u_1} {E : Type u_2} (φ' φ'' : Semantics.Dynamic.Core.PVar) (Sc' Sc'' : SemW W E) (φ : Semantics.Dynamic.Core.PVar) : Semantics.Dynamic.Core.ICDRTUpdate W E

(18c) Conditional: IF^{φ',φ''} ⟿ λSc'.λSc''.λφ.[φ',φ'' | φ ≡ φ̄'⊎φ'']; max_{φ'}(Sc'(φ')); max_{φ''}(Sc''(φ'')).

Equations

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

def Hofmann2025.semAND {W : Type u_1} {E : Type u_2} (φ' φ'' : Semantics.Dynamic.Core.PVar) (Sc' Sc'' : SemW W E) (φ : Semantics.Dynamic.Core.PVar) : Semantics.Dynamic.Core.ICDRTUpdate W E

(18d) Conjunction: AND^{φ',φ''} ⟿ λSc'.λSc''.λφ. [φ' | φ'⊑φ]; max_{φ'}(Sc'(φ')); [φ'' | φ''⊑φ']; max_{φ''}(Sc''(φ'')).

Equations

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

def Hofmann2025.semBelieved {W : Type u_1} {E : Type u_2} (φ' : Semantics.Dynamic.Core.PVar) (dox : Semantics.Dynamic.Core.ICDRTAssignment W E → Set W) (Sc : SemW W E) (_φ : Semantics.Dynamic.Core.PVar) : Semantics.Dynamic.Core.ICDRTUpdate W E

(18e) Attitude verb: believed ⟿ λv.λSc.λφ.[φ' | believe_φ(v,φ')]; max_{φ'}(Sc(φ')).

Equations

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

def Hofmann2025.semDEC {W : Type u_1} {E : Type u_2} (φ_DC φ : Semantics.Dynamic.Core.PVar) (Sc : SemW W E) : Semantics.Dynamic.Core.ICDRTUpdate W E

(19) Declarative assertion: DEC_S^φ ⟿ λSc.[φ | φ_{DC_S}⊑φ]; max_φ(Sc(φ)).

Equations

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

theorem Hofmann2025.commonNoun_is_test {W : Type u_1} {E : Type u_2} (R : E → W → Prop) (v : Semantics.Dynamic.Core.IVar) (φ : Semantics.Dynamic.Core.PVar) (i j : Semantics.Dynamic.Core.ICDRTAssignment W E) (h : commonNoun R v φ i j) : i = j

A common noun is a test: it preserves the assignment.

theorem Hofmann2025.vacuousScope_is_test {W : Type u_1} {E : Type u_2} (v : Semantics.Dynamic.Core.IVar) (φ : Semantics.Dynamic.Core.PVar) (i j : Semantics.Dynamic.Core.ICDRTAssignment W E) (h : vacuousScope v φ i j) : i = j

vacuousScope is a test (identity).

theorem Hofmann2025.pronoun_transparent {W : Type u_1} {E : Type u_2} (v : Semantics.Dynamic.Core.IVar) (P : SemE W E) (φ : Semantics.Dynamic.Core.PVar) : pronoun v P φ = P v φ

pronoun v P φ is just P v φ — the pronoun is transparent.

theorem Hofmann2025.indefinite_test_entails {W : Type u_1} {E : Type u_2} (v : Semantics.Dynamic.Core.IVar) (P P' : SemE W E) (φ : Semantics.Dynamic.Core.PVar) (hP : ∀ (a b : Semantics.Dynamic.Core.ICDRTAssignment W E), P v φ a b → a = b) (hP' : ∀ (a b : Semantics.Dynamic.Core.ICDRTAssignment W E), P' v φ a b → a = b) (i j : Semantics.Dynamic.Core.ICDRTAssignment W E) (h : indefinite v P P' φ i j) : Semantics.Dynamic.Core.localEntailment φ v j

Indefinite introduction implies local entailment when restrictor and scope are tests (preserve the assignment). The KEY structural connection between composition and accessibility.

theorem Hofmann2025.semDEC_inclusion {W : Type u_1} {E : Type u_2} (φ_DC φ : Semantics.Dynamic.Core.PVar) (Sc : SemW W E) (i j : Semantics.Dynamic.Core.ICDRTAssignment W E) (h : semDEC φ_DC φ Sc i j) : ∃ (k : Semantics.Dynamic.Core.ICDRTAssignment W E), Semantics.Dynamic.Core.propVarUp φ i k ∧ Semantics.Dynamic.Core.decCondition φ_DC φ k ∧ Semantics.Dynamic.Core.propMaxOp φ (Sc φ) k j

DEC introduces the inclusion condition.

theorem Hofmann2025.semNOT_introduces_complement {W : Type u_1} {E : Type u_2} (φ' : Semantics.Dynamic.Core.PVar) (Sc : SemW W E) (φ : Semantics.Dynamic.Core.PVar) (i j : Semantics.Dynamic.Core.ICDRTAssignment W E) (h : semNOT φ' Sc φ i j) : ∃ (k : Semantics.Dynamic.Core.ICDRTAssignment W E), Semantics.Dynamic.Core.propVarUp φ' i k ∧ Semantics.Dynamic.Core.isComplement φ φ' k ∧ Semantics.Dynamic.Core.propMaxOp φ' (Sc φ') k j

NOT introduces the complement condition on the intermediate assignment.

theorem Hofmann2025.double_neg_complement {W : Type u_1} {E : Type u_2} (φ' φ'' φ : Semantics.Dynamic.Core.PVar) (k j : Semantics.Dynamic.Core.ICDRTAssignment W E) (h_outer : Semantics.Dynamic.Core.isComplement φ φ' k) (h_inner : Semantics.Dynamic.Core.isComplement φ' φ'' j) (h_prop_pres : j⟦φ⟧ₚ = k⟦φ⟧ₚ) (h_prop_pres' : j⟦φ'⟧ₚ = k⟦φ'⟧ₚ) : j⟦φ⟧ₚ = j⟦φ''⟧ₚ

Double negation restores the original local context via double complementation.

theorem Hofmann2025.comp_isDistributive {W : Type u_1} {E : Type u_2} (D : Semantics.Dynamic.Core.ICDRTUpdate W E) : Semantics.Dynamic.Core.IsDistributive D.toDynProp

Every compositional derivation lifts to a distributive CCP.

theorem Hofmann2025.comp_factorizes {W : Type u_1} {E : Type u_2} (D : Semantics.Dynamic.Core.ICDRTUpdate W E) : D.toDynProp = Semantics.Dynamic.Core.lift (Semantics.Dynamic.Core.fiberDRS D)

Every compositional derivation factors through fiberDRS.

theorem Hofmann2025.comp_seq_lifts {W : Type u_1} {E : Type u_2} (D₁ D₂ : Semantics.Dynamic.Core.ICDRTUpdate W E) (c : Semantics.Dynamic.Core.IContext W E) : (D₁ ⨟ D₂).toDynProp c = D₂.toDynProp (D₁.toDynProp c)

Sequential composition in the fragment lifts to CCP composition.

def Hofmann2025.thereIsABathroom : SemW BWorld BEnt

"There is a bathroom" — existential with restrictor bathroom and vacuous scope. a^{v₁}(bathroom)(vacuous) = λφ.[φ:v₁]; [bathroom_φ(v₁)]

Equations

• Hofmann2025.thereIsABathroom = Hofmann2025.indefinite Hofmann2025.v1 (Hofmann2025.commonNoun Hofmann2025.isBathroom) Hofmann2025.vacuousScope

def Hofmann2025.itIsUpstairs : SemW BWorld BEnt

"It is upstairs" — pronoun v₁ with VP predicate upstairs. it_{v₁}(upstairs) = λφ.[upstairs_φ(v₁)]

Equations

• Hofmann2025.itIsUpstairs = Hofmann2025.pronoun Hofmann2025.v1 (Hofmann2025.intransVP Hofmann2025.isUpstairs)

def Hofmann2025.veridical_comp : Semantics.Dynamic.Core.ICDRTUpdate BWorld BEnt

Veridical: "There is a bathroom. It is upstairs."

Equations

• Hofmann2025.veridical_comp = Hofmann2025.semDEC Hofmann2025.pDC_S Hofmann2025.p1 Hofmann2025.thereIsABathroom ⨟ Hofmann2025.semDEC Hofmann2025.pDC_S Hofmann2025.p3 Hofmann2025.itIsUpstairs

def Hofmann2025.negated_comp : Semantics.Dynamic.Core.ICDRTUpdate BWorld BEnt

Negated: "There isn't a bathroom."

Equations

• Hofmann2025.negated_comp = Hofmann2025.semDEC Hofmann2025.pDC_S Hofmann2025.p1 (Hofmann2025.semNOT Hofmann2025.p2 Hofmann2025.thereIsABathroom)

def Hofmann2025.doubleNeg_comp : Semantics.Dynamic.Core.ICDRTUpdate BWorld BEnt

Double negation: "It's not the case that there isn't a bathroom."

Equations

• Hofmann2025.doubleNeg_comp = Hofmann2025.semDEC Hofmann2025.pDC_S Hofmann2025.p1 (Hofmann2025.semNOT Hofmann2025.p2 (Hofmann2025.semNOT Hofmann2025.p3 Hofmann2025.thereIsABathroom))

def Hofmann2025.bathDisj_comp : Semantics.Dynamic.Core.ICDRTUpdate BWorld BEnt

Bathroom disjunction: "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.disagree_comp : Semantics.Dynamic.Core.ICDRTUpdate BWorld BEnt

Disagreement: A: "There isn't a bathroom." B: "It is upstairs." Different speakers have different commitment sets — what bilateral accounts CANNOT handle (§5.1.1).

Equations

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

def Hofmann2025.modalSub_comp : Semantics.Dynamic.Core.ICDRTUpdate BWorld BEnt

Modal subordination: "There isn't a bathroom. Sue believes it's upstairs."

Equations

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

theorem Hofmann2025.veridical_comp_distributive : Semantics.Dynamic.Core.IsDistributive veridical_comp.toDynProp

Every compositional derivation lifts to a distributive CCP.

theorem Hofmann2025.veridical_comp_factors (c : Semantics.Dynamic.Core.IContext BWorld BEnt) : veridical_comp.toDynProp c = (semDEC pDC_S p3 itIsUpstairs).toDynProp ((semDEC pDC_S p1 thereIsABathroom).toDynProp c)

Sequential composition lifts correctly.

ICDRT vs. BUS: where the multi-agent architecture pays for itself

@cite{hofmann-2025} §5.1.1 contrasts ICDRT with Bilateral Update Semantics (BUS, @cite{krahmer-muskens-1995}, @cite{elliott-sudo-2025}). BUS uses two update channels (positive/negative) and treats negation as a swap; ICDRT uses propositional drefs and per-speaker commitment sets.

Both solve the bathroom sentence. ICDRT additionally covers disagreement, modal subordination, and the three-way veridical/hypothetical/counterfactual classification — none of which BUS can express, because BUS has a single information state with no per-speaker structure.

Property	ICDRT	BUS
Negation	Static complementation	Dimension swap
DNE	double_complement_eq	Definitional (rfl)
Bathroom	disjunction_enables_anaphora	Swap feeds disjunct
Disagreement	Per-speaker DC (DiscContext)	✗ (single state)
Modal subordination	counterfactualIndiv + modal shift	✗
Veridicality	Three-way	✗
Truth conditions	dec_complement_counterfactual	✗ (no DC)
State type	ICDRTAssignment	InfoState

The root cause: BUS is a single-agent system; ICDRT is multi-agent by construction.

theorem Hofmann2025.icdrt_bathroom_anaphora {W : Type u_1} {E : Type u_2} (φ_disj2 φ_anaphor : Semantics.Dynamic.Core.PVar) (v : Semantics.Dynamic.Core.IVar) (i : Semantics.Dynamic.Core.ICDRTAssignment W E) (h_sub : i⟦φ_anaphor⟧ₚ ⊆ i⟦φ_disj2⟧ₚ) (h_ref : ∀ w ∈ i⟦φ_disj2⟧ₚ, (i⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star) : Semantics.Dynamic.Core.localEntailment φ_anaphor v i

ICDRT handles bathroom anaphora via disjunction + local entailment. If the second disjunct's context grants v a referent, and the anaphor's context is within it, the pronoun is resolved.

theorem Hofmann2025.icdrt_disagreement_possible {W : Type u_1} {E : Type u_2} (φ_DC_A φ_DC_B : Semantics.Dynamic.Core.PVar) (v : Semantics.Dynamic.Core.IVar) (i : Semantics.Dynamic.Core.ICDRTAssignment W E) (h_cf_A : Semantics.Dynamic.Core.counterfactualIndiv φ_DC_A v i) (h_ver_B : Semantics.Dynamic.Core.veridicalIndiv φ_DC_B v i) : (∀ w ∈ i⟦φ_DC_A⟧ₚ, (i⟦v⟧ᵢ) w = Semantics.Dynamic.Core.Entity.star) ∧ ∀ w ∈ i⟦φ_DC_B⟧ₚ, (i⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star

In ICDRT, two speakers can disagree about the same dref: v is counterfactual for A but veridical for B, simultaneously.

theorem Hofmann2025.icdrt_disagreement_consistent {W : Type u_1} {E : Type u_2} {Speaker : Type u_3} (ctx : Semantics.Dynamic.Core.DiscContext W E Speaker) (A B : Speaker) (h_consistent : ctx.consistent) (_v : Semantics.Dynamic.Core.IVar) (_h_cf_A : Semantics.Dynamic.Core.counterfactualIndiv (ctx.dcVar A) _v ctx.state) (_h_ver_B : Semantics.Dynamic.Core.veridicalIndiv (ctx.dcVar B) _v ctx.state) : ctx.state⟦ctx.dcVar A⟧ₚ.Nonempty ∧ ctx.state⟦ctx.dcVar B⟧ₚ.Nonempty

Disagreement is consistent: both speakers can have nonempty commitment sets while disagreeing about whether the bathroom exists.

theorem Hofmann2025.icdrt_disagreement_via_pragMaxDC {W : Type u_1} {E : Type u_2} {Speaker : Type u_3} (dcVar : Speaker → Semantics.Dynamic.Core.PVar) (D : Semantics.Dynamic.Core.ICDRTUpdate W E) (i j : Semantics.Dynamic.Core.ICDRTAssignment W E) (v : Semantics.Dynamic.Core.IVar) (A B : Speaker) (_h_max : Semantics.Dynamic.Core.pragMaxDC dcVar D i j) (h_cf_A : Semantics.Dynamic.Core.counterfactualIndiv (dcVar A) v j) (h_ver_B : Semantics.Dynamic.Core.veridicalIndiv (dcVar B) v j) : (∀ w ∈ j⟦dcVar A⟧ₚ, (j⟦v⟧ᵢ) w = Semantics.Dynamic.Core.Entity.star) ∧ ∀ w ∈ j⟦dcVar B⟧ₚ, (j⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star

After A asserts "there isn't a bathroom" and B responds "it is upstairs", pragMaxDC updates each speaker's commitment set independently — A's stays excluding bathroom-worlds, B's expands to include them. The same dref v has different veridicality per speaker.

theorem Hofmann2025.icdrt_modal_subordination {W : Type u_1} {E : Type u_2} (φ_DC φ_modal : Semantics.Dynamic.Core.PVar) (v : Semantics.Dynamic.Core.IVar) (i : Semantics.Dynamic.Core.ICDRTAssignment W E) (h_cf : Semantics.Dynamic.Core.counterfactualIndiv φ_DC v i) (h_ent : Semantics.Dynamic.Core.localEntailment φ_modal v i) (_h_disjoint : i⟦φ_modal⟧ₚ ∩ i⟦φ_DC⟧ₚ = ∅) : (∀ w ∈ i⟦φ_DC⟧ₚ, (i⟦v⟧ᵢ) w = Semantics.Dynamic.Core.Entity.star) ∧ ∀ w ∈ i⟦φ_modal⟧ₚ, (i⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star

In ICDRT, a counterfactual dref can still be locally entailed in a hypothetical context: v maps to ⋆ in DC worlds but has referents in the modal context's worlds.

theorem Hofmann2025.icdrt_modal_subset_satisfied {W : Type u_1} {E : Type u_2} (_φ_DC φ_antecedent φ_modal : Semantics.Dynamic.Core.PVar) (v : Semantics.Dynamic.Core.IVar) (i : Semantics.Dynamic.Core.ICDRTAssignment W E) (h_sub : Semantics.Dynamic.Core.subsetReq φ_modal φ_antecedent i) (h_rel : ∀ (w : W), w ∈ i⟦φ_antecedent⟧ₚ ↔ (i⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star) : Semantics.Dynamic.Core.localEntailment φ_modal v i

The subset requirement is satisfied when the modal context shifts to hypothetical worlds where the antecedent's binding holds.

theorem Hofmann2025.icdrt_veridicality_exhaustive {W : Type u_1} {E : Type u_2} (φ_DC : Semantics.Dynamic.Core.PVar) (v : Semantics.Dynamic.Core.IVar) (i : Semantics.Dynamic.Core.ICDRTAssignment W E) : Semantics.Dynamic.Core.veridicalIndiv φ_DC v i ∨ Semantics.Dynamic.Core.counterfactualIndiv φ_DC v i ∨ Semantics.Dynamic.Core.hypotheticalIndiv φ_DC v i

The three veridicality categories are exhaustive.

theorem Hofmann2025.icdrt_dne {W : Type u_1} {E : Type u_2} (φ₁ φ₂ φ₃ : Semantics.Dynamic.Core.PVar) (i : Semantics.Dynamic.Core.ICDRTAssignment W E) (h1 : Semantics.Dynamic.Core.isComplement φ₁ φ₂ i) (h2 : Semantics.Dynamic.Core.isComplement φ₃ φ₁ i) : i⟦φ₃⟧ₚ = i⟦φ₂⟧ₚ

ICDRT double negation: complementing twice recovers the original proposition. The static analog of BUS's definitional DNE.

theorem Hofmann2025.icdrt_negated_dref_persists {W : Type u_1} {E : Type u_2} (φ_inner φ_outer : Semantics.Dynamic.Core.PVar) (v : Semantics.Dynamic.Core.IVar) (i : Semantics.Dynamic.Core.ICDRTAssignment W E) (_h_not : Semantics.Dynamic.Core.isComplement φ_outer φ_inner i) (h_ent : Semantics.Dynamic.Core.localEntailment φ_inner v i) (w : W) : w ∈ i⟦φ_inner⟧ₚ → (i⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star

After ICDRT negation, the negated dref is still in the discourse state — it just maps to ⋆ in the speaker's DC worlds. This persistence is what enables disagreement and modal subordination.

theorem Hofmann2025.icdrt_neg_existential_truth {W : Type u_1} {E : Type u_2} (φ_DC φ_outer φ_inner : Semantics.Dynamic.Core.PVar) (i : Semantics.Dynamic.Core.ICDRTAssignment W E) (h_comp : Semantics.Dynamic.Core.isComplement φ_outer φ_inner i) (h_dec : φ_DC ∈ₚ φ_outer at i) : Semantics.Dynamic.Core.counterfactualProp φ_DC φ_inner i

ICDRT derives negated existential truth conditions from DEC + complementation: DC ⊆ assertion and assertion = complement of inner together imply the inner content is counterfactual relative to the speaker.