[Yan23]: Monotonicity under desire as a neglect-zero effect

Chapter 4 of [Yan23] defends an upward-monotonic semantics for desire verbs against three classical puzzles — Ross's paradox under want ([Ros44]; the desiderative version is due to [Crn11]), Asher's puzzle (reported in [Hei92]) and Heim's own teach-on-Tuesdays example ([Hei92]) — by reducing all three to free-choice inferences in QBSML ([AvO23]): the monotonic step is semantically valid on the NE-free fragment, the paradoxical "ok with the unwanted alternative" inference is pragmatically valid only for the enriched conclusion, and the enriched conclusion is not derivable from the premise. The dissertation calls the general effect — semantic weakening licensing pragmatic neglect-zero consequences — the weakening effect triggered by monotonicity (WEM); this chapter is its desire-verb case study. Where no overt disjunction occurs (Asher, Heim), the paper's one new formal object — the reinterpretation function ∥·∥_P (Definition 32) — supplies it: a predicate Q with a contextually salient sub-predicate P is reinterpreted as (P ∧ Q) ∨ (¬P ∧ Q), licensed because the two are classically equivalent (eval_reinterpret_iff) yet pragmatically distinct under [·]⁺.

This file derives the chapter's account from the QBSML substrate (Core/Logic/Modal/QBSML/FreeChoice.lean): the □-FC fact it invokes (Fact 13) is boxFC_Q; the quantified variant needed for Asher and Heim is boxExiFC_Q; the semantic validity of the monotonic steps is support_disj_inl / support_nec_mono. The verbs want / it is ok are the Hintikka-style □/◇ over a bouletic accessibility relation, exactly as in the paper (§4.4.1; the positive semantics of want itself is deferred to the dissertation's Chapter 5).

Main declarations

• reinterpret — Yan's reinterpretation function ∥·∥_P (Definition 32), an instance of QBSMLFormula.mapAtoms.
• reinterpret_isNEFree, eval_reinterpret_iff — reinterpretation stays NE-free and is bilaterally equivalent to the original (substitution salva veritate; the classical equivalence of Qx and (Px ∧ Qx) ∨ (¬Px ∧ Qx) lifted to team semantics).
• ross_monotone, ross_fc, ross_premise, ross_blocked — Ross's paradox: monotonicity is semantically valid, FC pragmatically valid, and the enriched disjunctive premise underivable (the paper's Figure 4.2).
• asher_monotone, asher_fc, asher_premise, asher_blocked, asher_concl_enriched — Asher's puzzle via reinterpretation of TRIP by FREE (the paper's Figure 4.3), with the non-vacuity of reinterpretation under [·]⁺ witnessed at the same state, and the denotational side condition FREE ⊊ TRIP realised globally (asherModel_free_ssubset_trip).
• heim_fc — Heim's example via reinterpretation of TEACH by TUESDAY (the paper omits the rest of the derivation as parallel to Asher's; so do we).

The reinterpretation function

def Yan2023.reinterpret {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} (sub : Pred → Pred → Prop) [DecidableRel sub] (P : Pred) : Core.Logic.Modal.QBSML.QBSMLFormula Var Const Pred → Core.Logic.Modal.QBSML.QBSMLFormula Var Const Pred

Reinterpretation ∥·∥_P ([Yan23] Definition 32): rewrite each atom Q t whose predicate has P as a (contextually salient) sub-predicate as the disjunction (P t ∧ Q t) ∨ (¬P t ∧ Q t), and commute with every connective (QBSMLFormula.mapAtoms).

sub P Q plays the paper's side condition P ⊂ Q. That condition is denotational there (the denotation of P a proper subset of Q's), but the paper leaves open against which model it is checked — in the agent's own desire-state denotations it must fail for blocking to arise, so it is only sensible against a common-ground/global model (realised by the two-world asherModel below, asherModel_free_ssubset_trip). sub therefore stays an unconstrained contextual parameter, which eval_reinterpret_iff shows is truth-conditionally harmless; the salience requirement is likewise contextual and not part of the function.

The paper's language L_D (its Definition 24) has primitive □, derived ◇, and no ∀, so Definition 32 has no ◇/∀ clauses: the .poss clause here recovers its derived-◇ behaviour definitionally, and .univ extends the function to the full QBSMLFormula language. The .ne clause is a totality filler — the paper defines ∥·∥ on the NE-free fragment only.

Equations

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

theorem Yan2023.reinterpret_pred {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} (sub : Pred → Pred → Prop) [DecidableRel sub] (P Q : Pred) (x : Var) : reinterpret sub P (Core.Logic.Modal.QBSML.QBSMLFormula.pred Q x) = if sub P Q then ((Core.Logic.Modal.QBSML.QBSMLFormula.pred P x).conj (Core.Logic.Modal.QBSML.QBSMLFormula.pred Q x)).disj ((Core.Logic.Modal.QBSML.QBSMLFormula.pred P x).neg.conj (Core.Logic.Modal.QBSML.QBSMLFormula.pred Q x)) else Core.Logic.Modal.QBSML.QBSMLFormula.pred Q x

Equation lemma: reinterpretation at a variable atom. Not @[simp] — unfolding is opt-in.

theorem Yan2023.reinterpret_predc {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} (sub : Pred → Pred → Prop) [DecidableRel sub] (P Q : Pred) (c : Const) : reinterpret sub P (Core.Logic.Modal.QBSML.QBSMLFormula.predc Q c) = if sub P Q then ((Core.Logic.Modal.QBSML.QBSMLFormula.predc P c).conj (Core.Logic.Modal.QBSML.QBSMLFormula.predc Q c)).disj ((Core.Logic.Modal.QBSML.QBSMLFormula.predc P c).neg.conj (Core.Logic.Modal.QBSML.QBSMLFormula.predc Q c)) else Core.Logic.Modal.QBSML.QBSMLFormula.predc Q c

Equation lemma: reinterpretation at a constant atom.

theorem Yan2023.reinterpret_isNEFree {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} (sub : Pred → Pred → Prop) [DecidableRel sub] (P : Pred) {φ : Core.Logic.Modal.QBSML.QBSMLFormula Var Const Pred} (h : φ.IsNEFree) : (reinterpret sub P φ).IsNEFree

Reinterpretation preserves NE-freeness.

Substitution salva veritate

The classical equivalence of Qx and (Px ∧ Qx) ∨ (¬Px ∧ Qx) justifying reinterpretation ([Yan23] §4.3.2) holds bilaterally in team semantics — for unenriched formulas. Under [·]⁺ the two sides diverge, which is the entire point: the enriched reinterpreted formula carries free-choice commitments the original does not.

theorem Yan2023.eval_reinterpret_iff {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Const Pred) (sub : Pred → Pred → Prop) [DecidableRel sub] (P : Pred) (φ : Core.Logic.Modal.QBSML.QBSMLFormula Var Const Pred) (b : Bool) (s : Finset (Core.Logic.Modal.QBSML.Index W Var Domain)) : Core.Logic.Modal.QBSML.eval M b (reinterpret sub P φ) s ↔ Core.Logic.Modal.QBSML.eval M b φ s

Substitution salva veritate ([Yan23] §4.3.2): reinterpretation is bilaterally equivalent to the original — ∥φ∥_P and φ are supported and anti-supported by exactly the same states. This is the team-semantic form of the classical equivalence ∀x Qx ≡ ∀x((Qx ∧ Px) ∨ (Qx ∧ ¬Px)) the paper invokes to license reinterpretation. Holds for any sub and any formula (the paper's conditions on sub — sub-predicatehood, salience — govern felicity, not truth); eval_mapAtoms_iff reduces it to the two atom equivalences.

theorem Yan2023.support_reinterpret_iff {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Const Pred) (sub : Pred → Pred → Prop) [DecidableRel sub] (P : Pred) (φ : Core.Logic.Modal.QBSML.QBSMLFormula Var Const Pred) (s : Finset (Core.Logic.Modal.QBSML.Index W Var Domain)) : Core.Logic.Modal.QBSML.support M (reinterpret sub P φ) s ↔ Core.Logic.Modal.QBSML.support M φ s

Support is invariant under reinterpretation.

theorem Yan2023.antiSupport_reinterpret_iff {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Const : Type u_4} {Pred : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Const Pred) (sub : Pred → Pred → Prop) [DecidableRel sub] (P : Pred) (φ : Core.Logic.Modal.QBSML.QBSMLFormula Var Const Pred) (s : Finset (Core.Logic.Modal.QBSML.Index W Var Domain)) : Core.Logic.Modal.QBSML.antiSupport M (reinterpret sub P φ) s ↔ Core.Logic.Modal.QBSML.antiSupport M φ s

Anti-support is invariant under reinterpretation.

Ross's paradox under desire

"John wants to send the letter. ⇒ John wants to send the letter or burn it." ([Yan23] §4.1.3, after [Crn11]; deontic original [Ros44].) The monotonic step is semantically valid (ross_monotone, the [Want]A ⇒ [Want](A ∨ B) mode of [Yan23] Table 4.1, classified semantically valid in §4.4.3); the paradoxical "ok to burn" follows by □-FC only from the enriched disjunctive premise (ross_fc), which the agent's actual desire state supports the premise of (ross_premise) but not the enriched conclusion (ross_blocked) — the paper's Figure 4.2. Enrichment placement follows Fact 13's official wide form [□(· ∨ ·)]⁺ rather than the figures' elliptical □[· ∨ ·]⁺.

inductive Yan2023.RossPred : Type

Ross-paradox predicates: sending and burning the letter.

• send : RossPred
• burn : RossPred

@[implicit_reducible]

instance Yan2023.instDecidableEqRossPred : DecidableEq RossPred

Equations

• Yan2023.instDecidableEqRossPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Yan2023.instReprRossPred : Repr RossPred

Equations

• Yan2023.instReprRossPred = { reprPrec := Yan2023.instReprRossPred.repr }

def Yan2023.instReprRossPred.repr : RossPred → ℕ → Std.Format

Equations

• Yan2023.instReprRossPred.repr Yan2023.RossPred.send prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yan2023.RossPred.send")).group prec✝
• Yan2023.instReprRossPred.repr Yan2023.RossPred.burn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yan2023.RossPred.burn")).group prec✝

def Yan2023.sendL : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit RossPred

SEND a: the letter is sent (constant atom; a is the letter).

Equations

• Yan2023.sendL = Core.Logic.Modal.QBSML.QBSMLFormula.predc Yan2023.RossPred.send ()

def Yan2023.burnL : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit RossPred

BURN a: the letter is burnt.

Equations

• Yan2023.burnL = Core.Logic.Modal.QBSML.QBSMLFormula.predc Yan2023.RossPred.burn ()

theorem Yan2023.sendL_isNEFree : sendL.IsNEFree

theorem Yan2023.burnL_isNEFree : burnL.IsNEFree

def Yan2023.rossModel : Core.Logic.Modal.QBSML.QBSMLModel Unit Unit Unit RossPred

John's bouletic state: a single desire-world where the letter is sent and not burnt, reflexively accessible.

Equations

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

def Yan2023.rossState : Finset (Core.Logic.Modal.QBSML.Index Unit Core.Logic.Modal.BSML.QVar Unit)

The Ross evaluation state: the single desire-world with the empty assignment.

Equations

• Yan2023.rossState = {((), fun (x : Core.Logic.Modal.BSML.QVar) => none)}

theorem Yan2023.ross_monotone {s : Finset (Core.Logic.Modal.QBSML.Index Unit Core.Logic.Modal.BSML.QVar Unit)} (h : Core.Logic.Modal.QBSML.support rossModel sendL.nec s) : Core.Logic.Modal.QBSML.support rossModel (sendL.disj burnL).nec s

Semantic validity of the monotonic step: □SEND a ⊨ □(SEND a ∨ BURN a) — disjunction introduction under the bouletic □ (support_disj_inl + support_nec_mono).

theorem Yan2023.ross_fc {s : Finset (Core.Logic.Modal.QBSML.Index Unit Core.Logic.Modal.BSML.QVar Unit)} (h : Core.Logic.Modal.QBSML.support rossModel (sendL.disj burnL).nec.enrich s) : Core.Logic.Modal.QBSML.support rossModel sendL.poss s ∧ Core.Logic.Modal.QBSML.support rossModel burnL.poss s

Pragmatic validity of the FC step ([Yan23] (26), instance of Fact 13): [□(SEND a ∨ BURN a)]⁺ ⊨ ◇SEND a ∧ ◇BURN a — from the enriched disjunctive want, both "it is ok to send" and the paradoxical "it is ok to burn". Direct instance of boxFC_Q.

theorem Yan2023.ross_premise : Core.Logic.Modal.QBSML.support rossModel sendL.nec.enrich rossState

The premise is assertable: John's desire state supports the enriched [□SEND a]⁺.

theorem Yan2023.ross_blocked : ¬Core.Logic.Modal.QBSML.support rossModel (sendL.disj burnL).nec.enrich rossState

The block ([Yan23] Figure 4.2): John's desire state does not support the enriched disjunctive want [□(SEND a ∨ BURN a)]⁺ — were it assertable, □-FC would force an accessible burn-world, and there is none. The paradox dissolves: ◇BURN a is licensed only by a premise the discourse never grants.

Asher's puzzle

"Nicholas wants a free trip on the Concorde. ⇒ Nicholas wants a trip on the Concorde." ([Hei92], reported from Asher; [Yan23] §4.3.2.) No overt disjunction — the FC trigger is supplied by reinterpreting TRIP by its salient sub-predicate FREE-TRIP: ∥TRIP x∥ = (F ∧ T)x ∨ (¬F ∧ T)x. The premise is □∃x(Fx ∧ Tx) — the paper's ◻∃xFREEx unabbreviated, per its footnote treating the generalization as conjunction elimination (TRIP(x) ∧ FREE(x) ⇒ TRIP(x)) and its §4.5 gloss [Want](FREE ∧ TRIP) ⇒ [Want]TRIP; the unabbreviated form is also what makes the monotonic step QBSML-valid without a lexical meaning postulate. The paper's (27) displays use FREE elliptically for the subscripted FREE_TRIP form, so its conclusion ◊∃x¬FREEx is our ◇∃x(¬Fx ∧ Tx).

inductive Yan2023.AsherPred : Type

Asher-puzzle predicates: being free and being a trip (on the Concorde).

• free : AsherPred
• trip : AsherPred

@[implicit_reducible]

instance Yan2023.instDecidableEqAsherPred : DecidableEq AsherPred

Equations

• Yan2023.instDecidableEqAsherPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Yan2023.instReprAsherPred : Repr AsherPred

Equations

• Yan2023.instReprAsherPred = { reprPrec := Yan2023.instReprAsherPred.repr }

def Yan2023.instReprAsherPred.repr : AsherPred → ℕ → Std.Format

Equations

• Yan2023.instReprAsherPred.repr Yan2023.AsherPred.free prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yan2023.AsherPred.free")).group prec✝
• Yan2023.instReprAsherPred.repr Yan2023.AsherPred.trip prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yan2023.AsherPred.trip")).group prec✝

def Yan2023.subFree : AsherPred → AsherPred → Prop

FREE is the contextually salient sub-predicate of TRIP.

Equations

• Yan2023.subFree Yan2023.AsherPred.free Yan2023.AsherPred.trip = True
• Yan2023.subFree x✝¹ x✝ = False

@[implicit_reducible]

instance Yan2023.instDecidableRelAsherPredSubFree : DecidableRel subFree

Equations

• Yan2023.instDecidableRelAsherPredSubFree Yan2023.AsherPred.free Yan2023.AsherPred.trip = isTrue trivial
• Yan2023.instDecidableRelAsherPredSubFree Yan2023.AsherPred.free Yan2023.AsherPred.free = isFalse Yan2023.instDecidableRelAsherPredSubFree._proof_1
• Yan2023.instDecidableRelAsherPredSubFree Yan2023.AsherPred.trip Yan2023.AsherPred.free = isFalse Yan2023.instDecidableRelAsherPredSubFree._proof_2
• Yan2023.instDecidableRelAsherPredSubFree Yan2023.AsherPred.trip Yan2023.AsherPred.trip = isFalse Yan2023.instDecidableRelAsherPredSubFree._proof_3

def Yan2023.freeTrip : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit AsherPred

Fx ∧ Tx: a free trip.

Equations

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

def Yan2023.nonFreeTrip : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit AsherPred

¬Fx ∧ Tx: a non-free trip — the unwanted disjunct reinterpretation introduces.

Equations

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

theorem Yan2023.freeTrip_isNEFree : freeTrip.IsNEFree

theorem Yan2023.nonFreeTrip_isNEFree : nonFreeTrip.IsNEFree

def Yan2023.asherPremise : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit AsherPred

The premise □∃x(Fx ∧ Tx): Nicholas wants a free trip.

Equations

• Yan2023.asherPremise = (Core.Logic.Modal.QBSML.QBSMLFormula.exi Core.Logic.Modal.BSML.QVar.x Yan2023.freeTrip).nec

def Yan2023.asherConcl : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit AsherPred

The conclusion □∃xTx: Nicholas wants a trip.

Equations

• Yan2023.asherConcl = (Core.Logic.Modal.QBSML.QBSMLFormula.exi Core.Logic.Modal.BSML.QVar.x (Core.Logic.Modal.QBSML.QBSMLFormula.pred Yan2023.AsherPred.trip Core.Logic.Modal.BSML.QVar.x)).nec

theorem Yan2023.reinterpret_asherConcl : reinterpret subFree AsherPred.free asherConcl = (Core.Logic.Modal.QBSML.QBSMLFormula.exi Core.Logic.Modal.BSML.QVar.x (freeTrip.disj nonFreeTrip)).nec

Reinterpreting TRIP by FREE in the conclusion yields exactly the disjunctive want □∃x((F ∧ T)x ∨ (¬F ∧ T)x) — definitional.

theorem Yan2023.asher_monotone {W : Type u_1} {Domain : Type u_2} [DecidableEq W] [DecidableEq Domain] [Fintype Domain] (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Unit AsherPred) {s : Finset (Core.Logic.Modal.QBSML.Index W Core.Logic.Modal.BSML.QVar Domain)} (h : Core.Logic.Modal.QBSML.support M asherPremise s) : Core.Logic.Modal.QBSML.support M asherConcl s

Semantic validity of the monotonic step: □∃x(Fx ∧ Tx) ⊨ □∃xTx (conjunction elimination under ∃ under □), for any model.

theorem Yan2023.asher_fc {W : Type u_1} {Domain : Type u_2} [DecidableEq W] [DecidableEq Domain] [Fintype Domain] (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Unit AsherPred) {s : Finset (Core.Logic.Modal.QBSML.Index W Core.Logic.Modal.BSML.QVar Domain)} (h : Core.Logic.Modal.QBSML.support M (reinterpret subFree AsherPred.free asherConcl).enrich s) : Core.Logic.Modal.QBSML.support M (Core.Logic.Modal.QBSML.QBSMLFormula.exi Core.Logic.Modal.BSML.QVar.x freeTrip).poss s ∧ Core.Logic.Modal.QBSML.support M (Core.Logic.Modal.QBSML.QBSMLFormula.exi Core.Logic.Modal.BSML.QVar.x nonFreeTrip).poss s

The unwarranted inference ([Yan23] (27) and §4.4.3): the enriched reinterpreted conclusion [□∃x∥Tx∥_F]⁺ licenses, by quantified □-FC, both "ok with a free trip" and "ok with a non-free trip" — the latter being what makes the monotonic conclusion sound wrong.

def Yan2023.asherModel : Core.Logic.Modal.QBSML.QBSMLModel Bool Unit Unit AsherPred

Nicholas's bouletic state against a two-world background: in the desire-world true every trip is free; the non-desire world false has a non-free trip; only the desire-world is bouletically accessible.

Equations

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

def Yan2023.asherState : Finset (Core.Logic.Modal.QBSML.Index Bool Core.Logic.Modal.BSML.QVar Unit)

The Asher evaluation state: the desire-world with the empty assignment.

Equations

• Yan2023.asherState = {(true, fun (x : Core.Logic.Modal.BSML.QVar) => none)}

theorem Yan2023.asherModel_free_ssubset_trip : (∀ (w : Bool) (d : Unit), FirstOrder.Language.KripkeStructure.pInterp asherModel AsherPred.free w d → FirstOrder.Language.KripkeStructure.pInterp asherModel AsherPred.trip w d) ∧ ∃ (w : Bool) (d : Unit), FirstOrder.Language.KripkeStructure.pInterp asherModel AsherPred.trip w d ∧ ¬FirstOrder.Language.KripkeStructure.pInterp asherModel AsherPred.free w d

The paper's denotational side condition FREE ⊊ TRIP holds in the global model: FREE ⊆ TRIP at every world, strictly at the non-desire world. (In the desire-worlds themselves the inclusion is not strict — necessarily so, since blocking requires no accessible non-free trip; see reinterpret.)

theorem Yan2023.asher_premise : Core.Logic.Modal.QBSML.support asherModel asherPremise.enrich asherState

The premise is assertable: the desire state supports [□∃x(Fx ∧ Tx)]⁺.

theorem Yan2023.asher_blocked : ¬Core.Logic.Modal.QBSML.support asherModel (reinterpret subFree AsherPred.free asherConcl).enrich asherState

The block ([Yan23] Figure 4.3): the desire state does not support the enriched reinterpreted conclusion [□∃x∥Tx∥_F]⁺ — by asher_fc it would force an accessible non-free-trip witness, and all trips in Nicholas's desire-worlds are free. "Ok with a non-free trip" is licensed only by a premise the discourse never grants.

theorem Yan2023.asher_concl_enriched : Core.Logic.Modal.QBSML.support asherModel asherConcl.enrich asherState

Reinterpretation is pragmatically non-vacuous ([Yan23] §4.4.3: "it is possible to have a counterexample where [∃xQx]⁺ is supported but [∃x((Px ∨ ¬Px) ∧ Qx)]⁺ is not" — displayed there with the (Px ∨ ¬Px) ∧ Qx shape rather than Definition 32's). The unreinterpreted enriched conclusion [□∃xTx]⁺ IS supported at the very state where asher_blocked refutes the enriched reinterpreted form — the two classically equivalent formulas (eval_reinterpret_iff) come apart under [·]⁺, which is the paper's whole point.

Heim's example

"I want to teach on Tuesdays next semester. ⇒ I want to teach next semester." ([Hei92]; [Yan23] §4.3.3.) Same shape as Asher's puzzle: TEACH is reinterpreted by its salient sub-predicate TEACH-ON-TUESDAY, and quantified □-FC then licenses the unjustified "ok to teach on non-Tuesdays". The paper omits the rest of the derivation as parallel to Asher's (§4.4.3: "the details … are omitted"); so do we — the blocking countermodel is isomorphic to asher_blocked's. The paper also sketches an alternative ◊-FC route via the conditional-desire rephrasing of the example (its (17)–(18)); that variant is not formalized here.

inductive Yan2023.HeimPred : Type

Heim-example predicates: being on Tuesday and being a teaching (next semester).

• tuesday : HeimPred
• teach : HeimPred

@[implicit_reducible]

instance Yan2023.instDecidableEqHeimPred : DecidableEq HeimPred

Equations

• Yan2023.instDecidableEqHeimPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Yan2023.instReprHeimPred.repr : HeimPred → ℕ → Std.Format

Equations

• Yan2023.instReprHeimPred.repr Yan2023.HeimPred.tuesday prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yan2023.HeimPred.tuesday")).group prec✝
• Yan2023.instReprHeimPred.repr Yan2023.HeimPred.teach prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Yan2023.HeimPred.teach")).group prec✝

@[implicit_reducible]

instance Yan2023.instReprHeimPred : Repr HeimPred

Equations

• Yan2023.instReprHeimPred = { reprPrec := Yan2023.instReprHeimPred.repr }

def Yan2023.subTuesday : HeimPred → HeimPred → Prop

TUESDAY is the contextually salient sub-predicate of TEACH.

Equations

• Yan2023.subTuesday Yan2023.HeimPred.tuesday Yan2023.HeimPred.teach = True
• Yan2023.subTuesday x✝¹ x✝ = False

@[implicit_reducible]

instance Yan2023.instDecidableRelHeimPredSubTuesday : DecidableRel subTuesday

Equations

• Yan2023.instDecidableRelHeimPredSubTuesday Yan2023.HeimPred.tuesday Yan2023.HeimPred.teach = isTrue trivial
• Yan2023.instDecidableRelHeimPredSubTuesday Yan2023.HeimPred.tuesday Yan2023.HeimPred.tuesday = isFalse Yan2023.instDecidableRelHeimPredSubTuesday._proof_1
• Yan2023.instDecidableRelHeimPredSubTuesday Yan2023.HeimPred.teach Yan2023.HeimPred.tuesday = isFalse Yan2023.instDecidableRelHeimPredSubTuesday._proof_2
• Yan2023.instDecidableRelHeimPredSubTuesday Yan2023.HeimPred.teach Yan2023.HeimPred.teach = isFalse Yan2023.instDecidableRelHeimPredSubTuesday._proof_3

def Yan2023.tuesdayTeach : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit HeimPred

TUEx ∧ TEACHx: a Tuesday teaching.

Equations

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

def Yan2023.nonTuesdayTeach : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit HeimPred

¬TUEx ∧ TEACHx: a non-Tuesday teaching.

Equations

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

def Yan2023.heimConcl : Core.Logic.Modal.QBSML.QBSMLFormula Core.Logic.Modal.BSML.QVar Unit HeimPred

The conclusion □∃x TEACHx: I want to teach next semester.

Equations

• Yan2023.heimConcl = (Core.Logic.Modal.QBSML.QBSMLFormula.exi Core.Logic.Modal.BSML.QVar.x (Core.Logic.Modal.QBSML.QBSMLFormula.pred Yan2023.HeimPred.teach Core.Logic.Modal.BSML.QVar.x)).nec

theorem Yan2023.heim_fc {W : Type u_1} {Domain : Type u_2} [DecidableEq W] [DecidableEq Domain] [Fintype Domain] (M : Core.Logic.Modal.QBSML.QBSMLModel W Domain Unit HeimPred) {s : Finset (Core.Logic.Modal.QBSML.Index W Core.Logic.Modal.BSML.QVar Domain)} (h : Core.Logic.Modal.QBSML.support M (reinterpret subTuesday HeimPred.tuesday heimConcl).enrich s) : Core.Logic.Modal.QBSML.support M (Core.Logic.Modal.QBSML.QBSMLFormula.exi Core.Logic.Modal.BSML.QVar.x tuesdayTeach).poss s ∧ Core.Logic.Modal.QBSML.support M (Core.Logic.Modal.QBSML.QBSMLFormula.exi Core.Logic.Modal.BSML.QVar.x nonTuesdayTeach).poss s

The unwarranted inference ([Yan23] §4.4.3, "Reinterpretation of TEACH"): the enriched reinterpreted conclusion [□∃x∥TEACHx∥_TUE]⁺ licenses "ok to teach on a non-Tuesday" by quantified □-FC.