Coppock's outlook-based semantics

Statements of opinion are evaluated at outlooks, refinements of possible worlds that settle matters of opinion as well as of fact, in place of worlds supplemented with a judge. A proposition is a function from outlooks to three truth values; it is objective when no world's refinements split it into true and false, discretionary when some world's do, and strongly discretionary when every world's do, each notion relative to an information state. Faultless disagreement follows: asserting a proposition puts one at fault only if it is objectively false at the world of the context, which no strongly discretionary proposition ever is, while two agents whose doxastic states over outlooks accept and reject it genuinely disagree. The Swedish subjective attitude verb tycka differs from think only in presupposing, through the ∂ operator of the paper's Weak Kleene logic, that its complement is strongly discretionary relative to the common ground, and the paper offers, as a parallel to Kennedy and Willer, that find and consider would demand strong and mere discretionariness. The paper's four-outlook model of accessibility and its Swedish and English judgments are the rows of Data/Examples/Coppock2018.json, against which the conditions on the three verbs are checked.

Implementation notes

• The refinement relation is a map ρ : Ω → W, whose fibres are the refinement classes; that every world has an inhabited class, implicit in the paper's set-based definition of strong discretionariness and in its footnote 8, is the hypothesis Function.Surjective ρ where it matters. The classification predicates take the information state as a parameter, the unrelativised notions being the case of the universal state.
• The objective propositions of §3.1 form a Boolean subalgebra of the powerset of the outlooks, the image of the powerset of the worlds under preimage, and are order-isomorphic to it when every world is refined, the paper's footnote 8.
• Acceptance is the Kripke box over the agent's accessibility relation on outlooks, from Logic/Modal/Defs.lean, and rejection the box of falsity, stronger than the paper's gloss "holds in none" on a trivalent proposition but the reading its analysis of (38) uses. Think and tycka are trivalent propositions built with the Weak Kleene conjunction and ∂ of Core/Data/Trivalent.lean, so that presupposition projection through negation is the logic's rather than a stipulation.
• The formal fragment's syntax and translations (§5.1, §5.3), the context-of-utterance parameter, and the §4 pragmatics of assertion as a proposal are not modelled.

TODO

• The felicity conditions on coordination and quantification under tycka ((20)–(27)) need the issues raised by the complement, which the paper leaves to a theory of manner; their rows carry no model classification.
• A world-judge relativist rendering of the same data (§2, §3.4, §3.5.2) would let the contrast on opinionatedness (38) be stated as a theorem rather than prose.
• The paper argues (33) over the outlooks where its presupposition holds; on an open information state its own definition fails at the other world, so the row's common ground entails the presupposition, and the general condition on states wants stating.
• The prose on Fig. 2 says that from o₁₀ and o₀₀ agent a reaches "the one in which both p and q hold" while also rejecting q; the figure has a reach o₁₀, which the model follows.
• The footnote 8 isomorphism holds only when every world is refined; the paper does not state the hypothesis.
• Footnote 15 reports the presupposition filtered in a conditional, which the Weak Kleene connectives cannot do; the Middle Kleene conjunction of the substrate could, and the contrast wants stating as a theorem.
• [kennedy-willer-2022]'s pragmatic reworking of counterstance contingency and [anand-korotkova-2022]'s de re readings of find are the data on which the strong against mere discretionariness split could be tested rather than coded.

References

• [E. Coppock, Outlook-based semantics (2018)][coppock-2018]
• [M. Kölbel, Truth Without Objectivity (2002)][kolbel-2002]
• [M. Kölbel, Faultless disagreement (2003)][kolbel-2003]
• [P. Lasersohn, Context dependence, disagreement, and predicates of personal taste (2005)][lasersohn-2005]
• [C. Kennedy, M. Willer, Subjective attitudes and counterstance contingency (2016)][kennedy-willer-2016]
• [D. Beaver, E. Krahmer, A Partial Account of Presupposition Projection (2001)][beaver-krahmer-2001]
• S. C. Kleene, Introduction to Metamathematics (1952)
• [K. J. Sæbø, Judgment Ascriptions (2009)][saebo-2009]
• [T. Stephenson, Judge Dependence, Epistemic Modals, and Predicates of Personal Taste (2007)][stephenson-2007]
• [C. Kennedy, M. Willer, Familiarity Inferences, Subjective Attitudes and Counterstance Contingency (2022)][kennedy-willer-2022]
• [P. Anand, N. Korotkova, How to Theorize about Subjective Language (2022)][anand-korotkova-2022]

Refinement and objective propositions (§3.1)

Outlooks refine worlds: each settles the facts of its world and the matters of opinion besides. The refinement structure is a map from outlooks to worlds, the refinement class of a world being its fibre, so classes are disjoint and in one-to-one correspondence with the refined worlds, the paper's ∝.

def Coppock2018.Objective {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (O : Set Ω) : Prop

A set of outlooks is an objective proposition when it corresponds to a set of worlds, a union of refinement classes: a preimage of a set of worlds. A discretionary proposition is one that is not.

Equations

• Coppock2018.Objective ρ O = ∃ (V : Set W), O = ρ ⁻¹' V

theorem Coppock2018.objective_iff_forall_mem_iff {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (O : Set Ω) : Objective ρ O ↔ ∀ (o o' : Ω), ρ o = ρ o' → (o ∈ O ↔ o' ∈ O)

Objectivity is invariance across each refinement class: membership depends only on the refined world.

theorem Coppock2018.objective_iff_preimage_image {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (O : Set Ω) : Objective ρ O ↔ ρ ⁻¹' ρ '' O = O

Objectivity is saturation under the refinement map: the proposition already contains every outlook sharing a world with one of its members.

def Coppock2018.objectiveSubalgebra {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) : BooleanSubalgebra (Set Ω)

The objective propositions form a Boolean subalgebra of the powerset of the outlooks: the image of the powerset of the worlds under preimage, so closure under ⊔, ⊓ and ᶜ is inherited wholesale.

Equations

• Coppock2018.objectiveSubalgebra ρ = BooleanSubalgebra.map (CompleteLatticeHom.setPreimage ρ).toBoundedLatticeHom ⊤

@[simp]

theorem Coppock2018.mem_objectiveSubalgebra {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) {O : Set Ω} : O ∈ objectiveSubalgebra ρ ↔ Objective ρ O

def Coppock2018.objectiveOrderIso {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (hρ : Function.Surjective ρ) : Set W ≃o ↥(objectiveSubalgebra ρ)

When every world is refined by some outlook, the objective subalgebra is order-isomorphic to the powerset of the worlds, the paper's footnote 8.

Equations

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

The three-valued classification relative to an information state (§3.5)

To carry presupposition, propositions are total functions from outlooks to true, false and undefined; an information state is a set of outlooks, and the classification quantifies over each refinement class restricted to the state. The unrelativised notions of the paper are the case of the universal state.

def Coppock2018.ObjectivelyFalseAt {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (w : W) : Prop

p is objectively false at w: false at every refinement of w.

Equations

• Coppock2018.ObjectivelyFalseAt ρ p w = ∀ (o : Ω), ρ o = w → p o = Trivalent.false

def Coppock2018.ObjectiveOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) : Prop

Objective relative to C: no refinement class restricted to C assigns p both true and false.

Equations

• Coppock2018.ObjectiveOn ρ p C = ∀ o ∈ C, ∀ o' ∈ C, ρ o = ρ o' → p o = Trivalent.true → p o' ≠ Trivalent.false

def Coppock2018.DiscretionaryOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) : Prop

Discretionary relative to C: some refinement class restricted to C assigns p both true and false.

Equations

• Coppock2018.DiscretionaryOn ρ p C = ∃ o ∈ C, ∃ o' ∈ C, ρ o = ρ o' ∧ p o = Trivalent.true ∧ p o' = Trivalent.false

def Coppock2018.StronglyDiscretionaryOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) : Prop

Strongly discretionary relative to C: every refinement class the state leaves nonempty assigns p both true and false, a cut within every world the state leaves open.

Equations

• Coppock2018.StronglyDiscretionaryOn ρ p C = ∀ (w : W), (∃ o ∈ C, ρ o = w) → ∃ o ∈ C, ∃ o' ∈ C, ρ o = w ∧ ρ o' = w ∧ p o = Trivalent.true ∧ p o' = Trivalent.false

theorem Coppock2018.discretionaryOn_iff_not_objectiveOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) : DiscretionaryOn ρ p C ↔ ¬ObjectiveOn ρ p C

Discretionary is exactly the failure of objective.

theorem Coppock2018.StronglyDiscretionaryOn.discretionaryOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) (h : StronglyDiscretionaryOn ρ p C) (hC : C.Nonempty) : DiscretionaryOn ρ p C

Strong discretionariness entails discretionariness on any nonempty state: the paper's rendering of Kennedy and Willer, on which find demands radical counterstance contingency and consider mere counterstance contingency, so whatever embeds under find embeds under consider.

theorem Coppock2018.stronglyDiscretionaryOn_univ_iff {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (hρ : Function.Surjective ρ) : StronglyDiscretionaryOn ρ p Set.univ ↔ ∀ (w : W), ∃ (o : Ω) (o' : Ω), ρ o = w ∧ ρ o' = w ∧ p o = Trivalent.true ∧ p o' = Trivalent.false

On the universal state, when every world is refined, strong discretionariness is the paper's unrelativised definition: every world's refinements split p.

theorem Coppock2018.objectiveOn_univ_iff_objective_posExt {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (h : p.isBivalent) : ObjectiveOn ρ p Set.univ ↔ Objective ρ p.posExt

For a bivalent proposition the revised classification agrees with the set-based one of §3.1 on its positive extension.

@[instance_reducible]

instance Coppock2018.instDecidableObjectivelyFalseAt {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) [Fintype Ω] [DecidableEq W] (w : W) : Decidable (ObjectivelyFalseAt ρ p w)

Equations

• Coppock2018.instDecidableObjectivelyFalseAt ρ p w = id inferInstance

@[instance_reducible]

instance Coppock2018.instDecidableObjectiveOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) [Fintype Ω] [DecidableEq W] [DecidablePred fun (x : Ω) => x ∈ C] : Decidable (ObjectiveOn ρ p C)

Equations

• Coppock2018.instDecidableObjectiveOn ρ p C = id inferInstance

@[instance_reducible]

instance Coppock2018.instDecidableDiscretionaryOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) [Fintype Ω] [DecidableEq W] [DecidablePred fun (x : Ω) => x ∈ C] : Decidable (DiscretionaryOn ρ p C)

Equations

• Coppock2018.instDecidableDiscretionaryOn ρ p C = id inferInstance

@[instance_reducible]

instance Coppock2018.instDecidableStronglyDiscretionaryOnOfFintype {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) [Fintype Ω] [DecidableEq W] [DecidablePred fun (x : Ω) => x ∈ C] [Fintype W] : Decidable (StronglyDiscretionaryOn ρ p C)

Equations

• Coppock2018.instDecidableStronglyDiscretionaryOnOfFintype ρ p C = id inferInstance

The norm of accuracy and faultlessness (§3.2)

Being at fault is relative to the world of the context of utterance, which determines a world and not an outlook: one is at fault for asserting a proposition iff it is objectively false there. A strongly discretionary proposition is true at some refinement of every world the state leaves open, so no one is ever at fault for asserting it, the faultlessness half of faultless disagreement; contradiction is supplied by the propositions being complements.

def Coppock2018.SplitsAt {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (w : W) : Prop

p splits w: some refinement makes it true and another false. A disagreement about p at such a world is faultless, the paper's footnote 12.

Equations

• Coppock2018.SplitsAt ρ p w = ((∃ (o : Ω), ρ o = w ∧ p o = Trivalent.true) ∧ ∃ (o : Ω), ρ o = w ∧ p o = Trivalent.false)

theorem Coppock2018.SplitsAt.not_objectivelyFalseAt {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) {w : W} (h : SplitsAt ρ p w) : ¬ObjectivelyFalseAt ρ p w

The norm of accuracy: at a world the proposition splits, no asserter of it is at fault.

theorem Coppock2018.splitsAt_of_stronglyDiscretionaryOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) (h : StronglyDiscretionaryOn ρ p C) {w : W} (hw : ∃ o ∈ C, ρ o = w) : SplitsAt ρ p w

A strongly discretionary proposition splits every world the state leaves open, so any disagreement about it there is faultless.

theorem Coppock2018.not_objectivelyFalseAt_of_stronglyDiscretionaryOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) (C : Set Ω) (h : StronglyDiscretionaryOn ρ p C) {w : W} (hw : ∃ o ∈ C, ρ o = w) : ¬ObjectivelyFalseAt ρ p w

A strongly discretionary proposition is never objectively false at a world the state leaves open: its asserter is never at fault.

Doxastic states, acceptance and disagreement (§3.3)

An agent's doxastic state at an outlook is the set of outlooks accessible from it, so states vary from outlook to outlook: whether an agent holds a belief is itself settled by outlooks. To accept a proposition is for it to hold throughout one's accessible outlooks, the Kripke box over outlooks with the proposition's truth as valuation.

def Coppock2018.Accepts {Ω : Type u_2} (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) : Ω → Prop

An agent with accessibility R accepts p at o: p is true at every accessible outlook.

Equations

• Coppock2018.Accepts R p = ModalLogic.box R fun (x : Ω) => p x = Trivalent.true

def Coppock2018.Rejects {Ω : Type u_2} (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) : Ω → Prop

An agent with accessibility R rejects p at o: p is false at every accessible outlook, which is stronger than not accepting it.

Equations

• Coppock2018.Rejects R p = ModalLogic.box R fun (x : Ω) => p x = Trivalent.false

def Coppock2018.DisagreeAt {Ω : Type u_2} (p : Trivalent.Prop3 Ω) (R₁ R₂ : Ω → Ω → Prop) (o : Ω) : Prop

Two agents disagree about p at o when one accepts it and the other rejects it.

Equations

• Coppock2018.DisagreeAt p R₁ R₂ o = (Coppock2018.Accepts R₁ p o ∧ Coppock2018.Rejects R₂ p o)

def Coppock2018.Opinionated {Ω : Type u_2} (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) (o : Ω) : Prop

An agent is opinionated about p at o when they accept or reject it; the paper's (38) denies opinionatedness without contradiction.

Equations

• Coppock2018.Opinionated R p o = (Coppock2018.Accepts R p o ∨ Coppock2018.Rejects R p o)

def Coppock2018.ObjectiveRel {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) : Prop

An accessibility relation is a matter of fact when it depends on an outlook only through the world it refines: the paper's assumption that whether an agent holds a belief is settled by worlds.

Equations

• Coppock2018.ObjectiveRel ρ R = ∀ (o o' o'' : Ω), ρ o = ρ o' → (R o o'' ↔ R o' o'')

theorem Coppock2018.accepts_iff_of_objectiveRel {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) (hR : ObjectiveRel ρ R) {o o' : Ω} (h : ρ o = ρ o') : Accepts R p o ↔ Accepts R p o'

Acceptance under a factual accessibility relation is constant across a refinement class, so disagreement at an outlook is disagreement at its world.

@[instance_reducible]

instance Coppock2018.instDecidableAccepts {Ω : Type u_2} (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) [Fintype Ω] [DecidableRel R] (o : Ω) : Decidable (Accepts R p o)

Equations

• Coppock2018.instDecidableAccepts R p o = id (id inferInstance)

@[instance_reducible]

instance Coppock2018.instDecidableRejects {Ω : Type u_2} (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) [Fintype Ω] [DecidableRel R] (o : Ω) : Decidable (Rejects R p o)

Equations

• Coppock2018.instDecidableRejects R p o = id (id inferInstance)

@[instance_reducible]

instance Coppock2018.instDecidableDisagreeAtOfDecidableRel {Ω : Type u_2} (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) [Fintype Ω] [DecidableRel R] (o : Ω) (R₂ : Ω → Ω → Prop) [DecidableRel R₂] : Decidable (DisagreeAt p R R₂ o)

Equations

• Coppock2018.instDecidableDisagreeAtOfDecidableRel R p o R₂ = id inferInstance

@[instance_reducible]

instance Coppock2018.instDecidableOpinionated {Ω : Type u_2} (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) [Fintype Ω] [DecidableRel R] (o : Ω) : Decidable (Opinionated R p o)

Equations

• Coppock2018.instDecidableOpinionated R p o = id inferInstance

@[instance_reducible]

instance Coppock2018.instDecidableObjectiveRelOfDecidableEq {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) [Fintype Ω] [DecidableRel R] [DecidableEq W] : Decidable (ObjectiveRel ρ R)

Equations

• Coppock2018.instDecidableObjectiveRelOfDecidableEq ρ R = id inferInstance

Subjective attitude verbs (§3.5, §5)

English think and Swedish tycka 'think[opinion]' both denote doxastic acceptance; tycka alone carries the presupposition that its complement is strongly discretionary relative to the information state, (32) ∂(discretionary(φ)) ∧ □φ in the paper's Weak Kleene logic, on which an undefined conjunct makes the conjunction undefined.

def Coppock2018.think {Ω : Type u_2} (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) [DecidablePred (Accepts R p)] : Trivalent.Prop3 Ω

think (31): bare doxastic acceptance.

Equations

• Coppock2018.think R p o = Trivalent.ofProp (Coppock2018.Accepts R p o)

def Coppock2018.tycka {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) (C : Set Ω) [DecidablePred (Accepts R p)] [Decidable (StronglyDiscretionaryOn ρ p C)] : Trivalent.Prop3 Ω

tycka (32): the presupposition that the complement is strongly discretionary relative to C, conjoined by Weak Kleene conjunction with acceptance.

Equations

• Coppock2018.tycka ρ R p C o = (Trivalent.ofProp (Coppock2018.StronglyDiscretionaryOn ρ p C)).presuppose.meetWeak (Trivalent.ofProp (Coppock2018.Accepts R p o))

theorem Coppock2018.tycka_eq_indet_iff {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) (C : Set Ω) [DecidablePred (Accepts R p)] [Decidable (StronglyDiscretionaryOn ρ p C)] (o : Ω) : tycka ρ R p C o = Trivalent.indet ↔ ¬StronglyDiscretionaryOn ρ p C

A tycka report is undefined exactly when its complement is not strongly discretionary relative to the state: the subjectivity requirement is a presupposition, (28)–(29).

theorem Coppock2018.tycka_eq_true_iff {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) (C : Set Ω) [DecidablePred (Accepts R p)] [Decidable (StronglyDiscretionaryOn ρ p C)] (o : Ω) : tycka ρ R p C o = Trivalent.true ↔ StronglyDiscretionaryOn ρ p C ∧ Accepts R p o

A tycka report is true iff its complement is strongly discretionary and the agent accepts it.

theorem Coppock2018.tycka_eq_think_of_ne_indet {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) (C : Set Ω) [DecidablePred (Accepts R p)] [Decidable (StronglyDiscretionaryOn ρ p C)] (o : Ω) (h : tycka ρ R p C o ≠ Trivalent.indet) : tycka ρ R p C o = think R p o

tycka and think agree wherever the former is defined: the verbs differ only in the presupposition.

theorem Coppock2018.neg_tycka_eq_indet_iff {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) (C : Set Ω) [DecidablePred (Accepts R p)] [Decidable (StronglyDiscretionaryOn ρ p C)] (o : Ω) : (tycka ρ R p C o).neg = Trivalent.indet ↔ ¬StronglyDiscretionaryOn ρ p C

The presupposition projects through negation: I don't think[opinion] it's Tuesday is undefined in the same states as the unnegated report, (28).

theorem Coppock2018.tycka_eq_indet_of_objectiveOn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (R : Ω → Ω → Prop) (p : Trivalent.Prop3 Ω) (C : Set Ω) [DecidablePred (Accepts R p)] [Decidable (StronglyDiscretionaryOn ρ p C)] (o : Ω) (hobj : ObjectiveOn ρ p C) (hC : C.Nonempty) : tycka ρ R p C o = Trivalent.indet

An objective complement is presupposition failure for tycka on any nonempty state: the #I think[opinion] it's Tuesday effect, (2b), (28).

The chili model (§3.3, Fig. 2)

Four outlooks o_pq settle whether the chili is tasty, p, and whether the speaker is an opera singer, q; worlds settle only q. Agent a reaches from every outlook the one tasty outlook of its world, and agent b reaches the non-tasty singer outlook from the singer world and both tasty outlooks from the other, so a accepts p everywhere while b accepts it in the non-singer world and rejects it in the singer world: the two disagree about p at o₁₁ and o₀₁ and agree about q there, and b is unopinionated about q elsewhere. Both relations are matters of fact, so acceptance is constant across each refinement class. The hybrid (10) and the presupposing complements (33) and (34), for which the paper gives no model, are read on the same two coordinates.

@[reducible, inline]

abbrev Coppock2018.Chili.Outlook : Type

An outlook (tasty?, singer?).

Equations

• Coppock2018.Chili.Outlook = (Bool × Bool)

def Coppock2018.Chili.world : Outlook → Bool

Worlds settle the objective coordinate.

Equations

• Coppock2018.Chili.world = Prod.snd

def Coppock2018.Chili.tasty : Trivalent.Prop3 Outlook

p, the chili is tasty.

Equations

• Coppock2018.Chili.tasty o = Trivalent.ofBool o.1

def Coppock2018.Chili.opera : Trivalent.Prop3 Outlook

q, I am an opera singer.

Equations

• Coppock2018.Chili.opera o = Trivalent.ofBool o.2

def Coppock2018.Chili.sexyLinguist : Trivalent.Prop3 Outlook

John is a sexy linguist (10), the objective coordinate read as linguisthood.

Equations

• Coppock2018.Chili.sexyLinguist o = Trivalent.ofBool (o.1 && o.2)

def Coppock2018.Chili.terribleDumped : Trivalent.Prop3 Outlook

It's terrible that he dumped her (33): defined only where he did, the objective coordinate, and then settled by the discretionary one.

Equations

• Coppock2018.Chili.terribleDumped o = if o.2 = true then Trivalent.ofBool o.1 else Trivalent.indet

def Coppock2018.Chili.caresNotIdiot : Trivalent.Prop3 Outlook

She doesn't care that he is an idiot (34): defined only where he is, the discretionary coordinate, and then settled by the objective one.

Equations

• Coppock2018.Chili.caresNotIdiot o = if o.1 = true then Trivalent.ofBool o.2 else Trivalent.indet

def Coppock2018.Chili.accessA : Outlook → Outlook → Prop

Agent a reaches the tasty outlook of the current world.

Equations

• Coppock2018.Chili.accessA o o' = (o' = (true, o.2))

@[instance_reducible]

instance Coppock2018.Chili.instDecidableRelOutlookAccessA : DecidableRel accessA

Equations

• Coppock2018.Chili.instDecidableRelOutlookAccessA x✝¹ x✝ = id inferInstance

def Coppock2018.Chili.accessB : Outlook → Outlook → Prop

Agent b reaches the non-tasty outlook from the singer world and both tasty outlooks from the other.

Equations

• Coppock2018.Chili.accessB o o' = ((o.2 = true → o' = (false, true)) ∧ (o.2 = false → o'.1 = true))

@[instance_reducible]

instance Coppock2018.Chili.instDecidableRelOutlookAccessB : DecidableRel accessB

Equations

• Coppock2018.Chili.instDecidableRelOutlookAccessB x✝¹ x✝ = id inferInstance

theorem Coppock2018.Chili.objectiveRel_accessA : ObjectiveRel world accessA

theorem Coppock2018.Chili.objectiveRel_accessB : ObjectiveRel world accessB

inductive Coppock2018.Chili.CommonGround : Type

The information states of the model: open, or with the objective coordinate given, or with the discretionary one given.

• open : CommonGround
• objectiveGiven : CommonGround
• discretionaryGiven : CommonGround

@[instance_reducible]

instance Coppock2018.Chili.instDecidableEqCommonGround : DecidableEq CommonGround

Equations

• Coppock2018.Chili.instDecidableEqCommonGround x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Coppock2018.Chili.instFintypeCommonGround : Fintype CommonGround

Equations

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

def Coppock2018.Chili.CommonGround.toSet : CommonGround → Set Outlook

The outlooks a common ground leaves open.

Equations

• Coppock2018.Chili.CommonGround.open.toSet = Set.univ
• Coppock2018.Chili.CommonGround.objectiveGiven.toSet = {o : Coppock2018.Chili.Outlook | o.2 = true}
• Coppock2018.Chili.CommonGround.discretionaryGiven.toSet = {o : Coppock2018.Chili.Outlook | o.1 = true}

@[instance_reducible]

instance Coppock2018.Chili.instDecidablePredOutlookMemSetToSet (cg : CommonGround) : DecidablePred fun (x : Outlook) => x ∈ cg.toSet

Equations

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

theorem Coppock2018.Chili.stronglyDiscretionaryOn_tasty : StronglyDiscretionaryOn world tasty Set.univ

Tasty is strongly discretionary.

theorem Coppock2018.Chili.objectiveOn_opera : ObjectiveOn world opera Set.univ

Opera singer is objective.

theorem Coppock2018.Chili.discretionaryOn_sexyLinguist : DiscretionaryOn world sexyLinguist Set.univ

The hybrid (10) is discretionary, cutting the linguist world's refinements.

theorem Coppock2018.Chili.not_stronglyDiscretionaryOn_sexyLinguist : ¬StronglyDiscretionaryOn world sexyLinguist Set.univ

The hybrid is not strongly discretionary: false at every refinement of the non-linguist world.

theorem Coppock2018.Chili.stronglyDiscretionaryOn_sexyLinguist_objectiveGiven : StronglyDiscretionaryOn world sexyLinguist CommonGround.objectiveGiven.toSet

The hybrid is strongly discretionary once the linguist world is given: Ebba tycker att Jonas är en sexig lingvist (15)–(17) is acceptable only in a context where Jonas is taken to be a linguist.

theorem Coppock2018.Chili.stronglyDiscretionaryOn_terribleDumped_objectiveGiven : StronglyDiscretionaryOn world terribleDumped CommonGround.objectiveGiven.toSet

Presupposition placement, (33): a discretionary assertion with an objective presupposition is strongly discretionary once the presupposition is given.

theorem Coppock2018.Chili.not_stronglyDiscretionaryOn_caresNotIdiot (cg : CommonGround) : ¬StronglyDiscretionaryOn world caresNotIdiot cg.toSet

Presupposition placement, (34): an objective assertion with a discretionary presupposition is strongly discretionary on no information state.

theorem Coppock2018.Chili.accepts_accessA_tasty (o : Outlook) : Accepts accessA tasty o

a accepts p everywhere.

theorem Coppock2018.Chili.accepts_accessB_tasty_iff (o : Outlook) : Accepts accessB tasty o ↔ o.2 = false

b accepts p exactly in the non-singer world and rejects it exactly in the singer world.

theorem Coppock2018.Chili.rejects_accessB_tasty_iff (o : Outlook) : Rejects accessB tasty o ↔ o.2 = true

theorem Coppock2018.Chili.disagreeAt_tasty_iff (o : Outlook) : DisagreeAt tasty accessA accessB o ↔ o.2 = true

The two disagree about p exactly in the singer world, o₁₁ and o₀₁.

theorem Coppock2018.Chili.accepts_accessA_opera_iff (o : Outlook) : Accepts accessA opera o ↔ o.2 = true

Both accept q in the singer world; in the other, a rejects it and b is unopinionated, so they never disagree about q.

theorem Coppock2018.Chili.accepts_accessB_opera_iff (o : Outlook) : Accepts accessB opera o ↔ o.2 = true

theorem Coppock2018.Chili.rejects_accessA_opera_iff (o : Outlook) : Rejects accessA opera o ↔ o.2 = false

theorem Coppock2018.Chili.not_opinionated_accessB_opera (o : Outlook) (h : o.2 = false) : ¬Opinionated accessB opera o

theorem Coppock2018.Chili.not_disagreeAt_opera (o : Outlook) : ¬DisagreeAt opera accessA accessB o ∧ ¬DisagreeAt opera accessB accessA o

theorem Coppock2018.Chili.not_objectivelyFalseAt_tasty (w : Bool) : ¬ObjectivelyFalseAt world tasty w

The chili dialogue (3) is faultless: no world makes tasty objectively false.

theorem Coppock2018.Chili.objectivelyFalseAt_opera : ObjectivelyFalseAt world opera false

The doctor dialogue (6) contrast: asserting I am an opera singer in the non-singer world violates the norm of accuracy.

theorem Coppock2018.Chili.objectivelyFalseAt_sexyLinguist : ObjectivelyFalseAt world sexyLinguist false

So does asserting the hybrid (10) where John is no linguist, (12).

theorem Coppock2018.Chili.tycka_tasty (o : Outlook) : tycka world accessA tasty Set.univ o = Trivalent.true

Tycka reports of tasty are defined everywhere and true for a.

theorem Coppock2018.Chili.tycka_opera (o : Outlook) : tycka world accessA opera Set.univ o = Trivalent.indet

Tycka reports of opera singer are undefined.

The paper's judgments

The rows of Data/Examples/Coppock2018.json with a complement feature denote a proposition of the chili model, their commonGround feature an information state, and their verb a subjective attitude verb: tycka under the paper's condition (19), find and consider under the parallel it offers to Kennedy and Willer. Which predicates are discretionary is the theory's lexical assumption, as the paper says of doctor and tasty, so the rows with a bare taste or factual complement check consistency only; the predictions are the model theorems above, the hybrid rescued by a common ground ((15)–(17)), presupposition placement ((33) against (34)) and the split of find from consider on the hybrid (37).

def Coppock2018.complements : List (String × Trivalent.Prop3 Chili.Outlook)

The model proposition a row's complement denotes.

Equations

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

def Coppock2018.commonGrounds : List (String × Chili.CommonGround)

The common ground a row names.

Equations

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

inductive Coppock2018.VerbCondition : Type

The condition a subjective attitude verb places on its complement: strong discretionariness, or mere discretionariness.

• strong : VerbCondition
• mere : VerbCondition

@[instance_reducible]

instance Coppock2018.instDecidableEqVerbCondition : DecidableEq VerbCondition

Equations

• Coppock2018.instDecidableEqVerbCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Coppock2018.VerbCondition.Holds : VerbCondition → Trivalent.Prop3 Chili.Outlook → Set Chili.Outlook → Prop

The condition as a predicate on a proposition of the chili model relative to a state.

Equations

• Coppock2018.VerbCondition.strong.Holds x✝¹ x✝ = Coppock2018.StronglyDiscretionaryOn Coppock2018.Chili.world x✝¹ x✝
• Coppock2018.VerbCondition.mere.Holds x✝¹ x✝ = Coppock2018.DiscretionaryOn Coppock2018.Chili.world x✝¹ x✝

@[instance_reducible]

instance Coppock2018.instDecidableHoldsToSet (vc : VerbCondition) (p : Trivalent.Prop3 Chili.Outlook) (cg : Chili.CommonGround) : Decidable (vc.Holds p cg.toSet)

Equations

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

def Coppock2018.verbConditions : List (String × VerbCondition)

tycka demands strong discretionariness (19); that find demands the same and consider mere discretionariness is the parallel to Kennedy and Willer the paper offers, leaving the difference between the verbs open.

Equations

• Coppock2018.verbConditions = [("tycka", Coppock2018.VerbCondition.strong), ("find", Coppock2018.VerbCondition.strong), ("consider", Coppock2018.VerbCondition.mere)]

theorem Coppock2018.verb_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → ∀ vc ∈ row.parse? "verb" verbConditions, ∀ c ∈ row.feature? "complement", ∃ p ∈ List.lookup c complements, ∃ cg ∈ List.lookup ((row.feature? "commonGround").getD "open") commonGrounds, row.judgment = Features.Judgment.acceptable ↔ vc.Holds p cg.toSet

Row consistency: a subjective attitude report is acceptable exactly when its complement meets the verb's condition relative to the common ground, open unless the row names one. A complement the model does not read fails the check outright.