Yan (2023): Monotonicity in Intensional Contexts #
This file formalizes Chapter 4 of [Yan23], which defends an upward-monotonic semantics for
desire verbs against three puzzles: Asher's puzzle and the teach-on-Tuesdays example reported
in [Hei92], and Ross's paradox under want from [Crn11] after [Ros44]. Want
is the necessity modal over a bouletic accessibility relation and it is ok its dual, §4.4.1,
in the quantified bilateral state-based modal logic of [AvO23]. Each puzzle
reduces to a free-choice inference: the monotonic step is valid on the NE-free fragment
(nec_disj_intro, nec_exi_within_mono); the inference that the agent is ok with the
unwanted alternative follows by □-free choice, Fact 13, from the pragmatically enriched
disjunctive conclusion (ross_fc, fc_of_reinterpret); and at a desire state that supports
the enriched premise the enriched conclusion is unsupported (ross_blocked, asher_blocked,
heim_blocked), so the three puzzles are pragmatic failures, Table 4.3. Where no disjunction
is overt, the reinterpretation function of Definition 32 supplies one: a predicate with a
contextually salient sub-predicate is read as the disjunction of the predicate within the
sub-predicate and outside it (reinterpret), which stays NE-free and is bilaterally
equivalent to the original (reinterpret_neFree, eval_reinterpret_iff) yet parts from it
under enrichment (asher_concl_enriched, asher_blocked).
Implementation notes #
- The language of Definition 24 has primitive □, derived ◇ and no ∀. The substrate
Formulahas primitive ◇ and ∀ with □ derived, so the enrichment of□φis the negation-clause enrichment of¬◇¬φ, under which Fact 13 holds asboxFC;reinterpretextends Definition 32 to ∀ and, as a totality filler, to NE. - The side condition of Definition 32, that the denotation of the sub-predicate is a proper
subset of the predicate's, is checked against the global model (
IsSubPred): within the agent's desire worlds it must fail, since blocking requires every trip there to be free. The relationsubthat triggers reinterpretation is therefore a contextual parameter, andeval_reinterpret_iffholds for any choice of it. - The premise of Asher's puzzle is
□∃x(FREE x ∧ TRIP x), the paper's□∃x FREE xunabbreviated after its footnote reading the generalisation as conjunction elimination; the conclusion◇∃x ¬FREE xof (27d) is◇∃x(¬FREE x ∧ TRIP x). - Asher's and Heim's puzzles share one two-world model,
desireModel: every predicate holds at the desire world and only the wanted predicate at the other. The ◇-free-choice route through the conditional rephrasing (17)–(18) and the deontic applications of §4.5 are not formalized.
References #
The reinterpretation function, Definition 32 #
within P Q x, Q within P, is P x ∧ Q x, the paper's P_Q x.
Equations
- Yan2023.within P Q x = (QBSML.Formula.pred P x).conj (QBSML.Formula.pred Q x)
Instances For
without P Q x, Q outside P, is ¬P x ∧ Q x, the paper's ¬P_Q x.
Equations
- Yan2023.without P Q x = (QBSML.Formula.pred P x).neg.conj (QBSML.Formula.pred Q x)
Instances For
Reinterpretation by P replaces each atom whose predicate Q has P as a contextually
salient sub-predicate, sub P Q, by the disjunction of Q within P and Q outside P, and
commutes with every connective.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Reinterpretation stays in the NE-free fragment.
The reinterpreted want □∃x‖Qx‖_P is the disjunctive want.
Substitution salva veritate, §4.3.2 #
The classical equivalence of Q x and (P x ∧ Q x) ∨ (¬P x ∧ Q x) that licenses
reinterpretation holds bilaterally in team semantics for unenriched formulas.
Reinterpretation is bilaterally equivalent to the original. ‖φ‖_P and φ are
supported and anti-supported by the same states, for any sub, since the sub-predicate and
salience conditions govern felicity rather than truth.
Monotonicity, free choice and blocking, §4.4.3 #
The pattern of Figures 4.2 and 4.3 on an arbitrary model: the monotonic step is valid, the enriched conclusion yields the unwanted possibility by □-free choice, and a desire state whose accessible worlds contain no instance of the unwanted disjunct supports the enriched premise but not the enriched conclusion.
Disjunction introduction under want, the mode of Ross's paradox in Table 4.1, is valid for an NE-free added disjunct.
Conjunction elimination under want and ∃, the mode of Asher's and Heim's puzzles in Table 4.1, is valid.
By free choice from the enriched reinterpreted want, (14) and (27), the agent is ok with
Q within P and with Q outside P.
The enriched want of a constant atom is supported at a nonempty state each of whose indices sees some world, all of them verifying the atom.
The enriched disjunctive want [□(A c ∨ B c)]⁺ is unsupported at a nonempty state none
of whose accessible worlds verifies B c.
The enriched want [□∃x(P x ∧ Q x)]⁺ is supported at a nonempty state each of whose
indices sees some world, all of them holding an individual that is P and Q.
The enriched premise supports the enriched unreinterpreted conclusion, since the same
witnesses serve [□∃x Q x]⁺.
The enriched reinterpreted want [□∃x‖Q x‖_P]⁺ is unsupported at a nonempty state whose
accessible worlds have every Q within P: by free choice it would need an accessible Q
outside P.
Equations
- Yan2023.instDecidableEqVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Yan2023.instFintypeVar = { elems := { val := ↑Yan2023.Var.enumList, nodup := Yan2023.Var.enumList_nodup }, complete := Yan2023.instFintypeVar._proof_1 }
Ross's paradox under desire, (3), (26), Figure 4.2 #
The predicates of Ross's paradox are sending and burning the letter.
Instances For
Equations
- Yan2023.instDecidableEqRossPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
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✝
Instances For
Equations
- Yan2023.instReprRossPred = { reprPrec := Yan2023.instReprRossPred.repr }
John's desire model has one desire world, reflexively accessible, where the letter is sent and not burnt.
Equations
- Yan2023.rossModel = QBSML.Model.ofMonadic (fun (x : Unit) => {()}) (fun (x x_1 : Unit) => ()) fun (x : Unit) (P : Yan2023.RossPred) (x_1 : Unit) => P = Yan2023.RossPred.send
Instances For
John's desire state is the desire world with the empty assignment.
Equations
- Yan2023.rossState = {((), ⊥)}
Instances For
The monotonic step (26a) to (26b) is semantically valid.
From the enriched disjunctive want, it is ok to send, (26c), and ok to burn, (26d).
The enriched premise [□SEND a]⁺ is supported at John's desire state.
The enriched disjunctive want [□(SEND a ∨ BURN a)]⁺ is not supported there, since free
choice would require an accessible burn world.
A desire model for a salient sub-predicate #
Nicholas wants a free trip, (1); I want to teach on Tuesdays, (2). At the desire world every predicate holds of the one individual; at the other world only the wanted predicate, so the sub-predicate's denotation is a proper subset globally.
P is a sub-predicate of Q in M when its denotation is a proper subset of Q's.
Equations
- One or more equations did not get rendered due to their size.
Instances For
In the two-world desire model for the wanted predicate Q, only the desire world true is
accessible; every predicate holds there and only Q at false.
Equations
- Yan2023.desireModel Q = QBSML.Model.ofMonadic (fun (x : Bool) => {true}) (fun (x : Bool) (x_1 : Unit) => ()) fun (w : Bool) (P : Pred) (x : Unit) => P = Q ∨ w = true
Instances For
The desire state is the desire world with the empty assignment.
Equations
- Yan2023.desireState = {(true, ⊥)}
Instances For
Any other predicate is a sub-predicate of Q in desireModel Q.
The enriched premise [□∃x(P x ∧ Q x)]⁺ is supported at the desire state.
The enriched unreinterpreted conclusion [□∃x Q x]⁺ is supported at the desire state.
The enriched reinterpreted conclusion [□∃x‖Q x‖_P]⁺ is not supported at the desire
state: every Q in the desire world is P. The two classically equivalent conclusions part
under enrichment.
Asher's puzzle, (1), (27), Figure 4.3 #
The predicates of Asher's puzzle are being free and being a trip on the Concorde.
Instances For
Equations
- Yan2023.instDecidableEqAsherPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Yan2023.instReprAsherPred = { reprPrec := Yan2023.instReprAsherPred.repr }
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✝
Instances For
FREE is the contextually salient sub-predicate of TRIP.
Equations
- Yan2023.subFree P Q = (P = Yan2023.AsherPred.free ∧ Q = Yan2023.AsherPred.trip)
Instances For
Equations
- Yan2023.instDecidableRelAsherPredSubFree x✝¹ x✝ = { decide := decide (x✝¹ = Yan2023.AsherPred.free) && decide (x✝ = Yan2023.AsherPred.trip), reflects_decide := ⋯ }
The side condition of Definition 32 holds globally.
The monotonic step (27a) to (27b) is semantically valid on any model.
The enriched reinterpreted conclusion licenses being ok with a free trip, (27c), and with a non-free trip, (27d).
Nicholas's desire state supports the enriched premise but not the enriched reinterpreted conclusion: being ok with a non-free trip is licensed only by a premise never granted.
Heim's example, (2), (15)–(16) #
TEACH is reinterpreted by its salient sub-predicate teaching on Tuesday; the paper leaves the derivation as parallel to Asher's.
The predicates of Heim's example are being on Tuesday and being a teaching next semester.
Instances For
Equations
- Yan2023.instDecidableEqHeimPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Yan2023.instReprHeimPred = { reprPrec := Yan2023.instReprHeimPred.repr }
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✝
Instances For
TUESDAY is the contextually salient sub-predicate of TEACH.
Equations
- Yan2023.subTuesday P Q = (P = Yan2023.HeimPred.tuesday ∧ Q = Yan2023.HeimPred.teach)
Instances For
Equations
- Yan2023.instDecidableRelHeimPredSubTuesday x✝¹ x✝ = { decide := decide (x✝¹ = Yan2023.HeimPred.tuesday) && decide (x✝ = Yan2023.HeimPred.teach), reflects_decide := ⋯ }
The enriched reinterpreted conclusion licenses being ok with teaching on a non-Tuesday, (16c).
The desire state of a speaker who teaches only on Tuesdays supports the enriched premise (15a) but not the enriched reinterpreted conclusion.