Coppock 2018: outlook-based semantics

[Cop18]

[Cop18]'s relativism for statements of opinion: outlooks — refinements of worlds that settle matters of opinion as well as fact — replace possible worlds as circumstances of evaluation, rather than supplementing them with a judge as in world-judge relativism ([Las05]). A proposition is a function from outlooks to three truth values (Prop3 Ω, with [Cop18]'s Weak Kleene connectives available as Trivalent.meetWeak/ Trivalent.joinWeak/Trivalent.neg); it is objective when its truth value never splits within a world's refinement class, discretionary when it does, and strongly discretionary when it splits within every world's class. Faultless disagreement ([Kol03]) then falls out: two agents can accept and reject the same strongly discretionary proposition at one outlook (genuine disagreement) while neither violates the norm of accuracy (no world makes such a proposition objectively false). The subjective attitude verb tycka 'think[opinion]' presupposes strong discretionariness of its complement relative to the common ground; the paper's ∂-operator rendering of that presupposition is played here by the project-canonical PartialProp.

The formal fragment's syntax (types, translations ⤳), the context-set parameter sequence, and the §4 pragmatics (assertion-as-proposal, seeking a common outlook) are not modelled. Studies/Kubota2026.lean borrows the outlook term for its two-layered outlook-marker denotation; the apparatus here is the paper's own, where outlook-relativity is a property of at-issue discretionary content. [KW16]'s counterstance contingency appears via the paper's translation: radically counterstance-contingent = strongly discretionary.

Main definitions

• Objective, objective_iff_fiberInvariant, objective_iff_preimage_image — set-of-outlooks propositions (§3.1): objective = union of refinement classes = fiber-invariant = saturated under the refinement map. objectiveSubalgebra bundles the objective propositions as a BooleanSubalgebra of the powerset of Ω, and objectiveOrderIso realizes the paper's note that it is isomorphic to the powerset of the worlds. The classification predicates carry Decidable instances for finite models.
• Objective3, Discretionary3, StronglyDiscretionary3 — the revised three-valued classification, plus the information-state-relativized ObjectiveIn/DiscretionaryIn/ StronglyDiscretionaryIn.
• Accepts, Rejects, DisagreeAt, Opinionated — doxastic accessibility as a binary relation on outlooks (§5's R_a), acceptance as the Kripke box (Core.Logic.Modal.box).
• AtFault — the norm of accuracy: asserting what is objectively false at the context world.
• think, tycka — the attitude verbs as PartialProps: same assertion (doxastic acceptance), differing only in tycka's strong-discretionariness presupposition.

Main results

• stronglyDiscretionary3_never_atFault — a strongly discretionary proposition never puts its asserter at fault: the faultlessness half of faultless disagreement.
• chili_disagreement, tasty_never_atFault — the chili dialogue in a four-outlook model: genuine disagreement about tasty with neither party at fault; contrast opera_atFault (objective propositions do incur fault) and the sexy linguist hybrid (discretionary but not strongly so, hence world-level falsity).
• think_tycka_same_assertion, tycka_presup_survives_neg — tycka differs from think only in its presupposition, and that presupposition projects through negation.
• tycka_undefined_of_objectiveIn — an objective complement yields presupposition failure (the "#I think[opinion] it's Tuesday" effect).
• stronglyDiscretionaryIn_discretionaryIn — strong discretionariness entails discretionariness on nonempty restricted classes: [Cop18]'s translation of [KW16]'s find (radical) vs consider (mere counterstance contingency).

References

[Cop18] [Kol03] [Las05] [KW16] [Kle52] [BK01]

Refinement and objectivity (§3.1)

Outlooks refine worlds: each outlook settles all the facts its world settles, plus matters of opinion. The refinement structure is a map ρ : Ω → W; the refinement class of w is the fiber ρ ⁻¹' {w}, so classes are automatically mutually non-overlapping and in one-to-one correspondence with (inhabited fibers of) worlds — [Cop18]'s ∝.

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

A set-of-outlooks proposition is objective when it corresponds to a set of possible worlds: a union of refinement classes, i.e. a preimage of a set of worlds.

Equations

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

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

A discretionary proposition doesn't "color within the lines": it is not objective.

Equations

• Coppock2018.Discretionary ρ O = ¬Coppock2018.Objective ρ O

theorem Coppock2018.objective_iff_fiberInvariant {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: an outlook proposition is objective iff 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: O already contains every outlook that shares a world with one of its members.

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

Only the kernel of the refinement map matters: objectivity is constancy on the classes of Setoid.ker ρ. (The worlds beyond the fibers are inert — W could be replaced by Quotient (Setoid.ker ρ) without loss.)

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 image of the powerset of W under Set.preimage ρ bundled as a bounded-lattice homomorphism, so closure under ⊔/⊓/ᶜ is inherited wholesale rather than proved operation-by-operation.

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 — [Cop18]'s ∝ pairs each world with an inhabited refinement class — the objective subalgebra is order-isomorphic to the powerset of the worlds (and an order iso between Boolean algebras preserves the whole Boolean structure).

Equations

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

The revised three-valued classification (§3.5)

To carry presupposition, propositions become total functions from outlooks to {T, F, #} — Prop3 Ω. The classification now quantifies over truth-value splits within refinement classes.

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

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

Equations

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

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.Objective3 {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) : Prop

Objective (revised): no world has refinements assigning p both T and F.

Equations

• Coppock2018.Objective3 ρ p = ∀ (o o' : Ω), ρ o = ρ o' → p o = Trivalent.true → p o' ≠ Trivalent.false

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

Discretionary (revised): some world has refinements assigning p both T and F.

Equations

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

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

Strongly discretionary (revised): every world's refinements split p into T and F — the proposition makes a cut across all the worlds.

Equations

• Coppock2018.StronglyDiscretionary3 ρ p = ∀ (w : W), ∃ (o : Ω) (o' : Ω), ρ o = w ∧ ρ o' = w ∧ p o = Trivalent.true ∧ p o' = Trivalent.false

theorem Coppock2018.discretionary3_iff_not_objective3 {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (p : Trivalent.Prop3 Ω) : Discretionary3 ρ p ↔ ¬Objective3 ρ p

Discretionary is exactly the failure of objective.

The classification predicates are finitely checkable, so they carry Decidable instances (delegating to the definitional quantifier forms) — model verifications below are bare decides.

@[implicit_reducible]

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

Equations

• Coppock2018.instDecidableObjectivelyTrueAt ρ p w = Coppock2018.instDecidableObjectivelyTrueAt._aux_1 ρ p w

@[implicit_reducible]

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

Equations

• Coppock2018.instDecidableObjectivelyFalseAt ρ p w = Coppock2018.instDecidableObjectivelyFalseAt._aux_1 ρ p w

@[implicit_reducible]

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

Equations

• Coppock2018.instDecidableObjective3 ρ p = Coppock2018.instDecidableObjective3._aux_1 ρ p

@[implicit_reducible]

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

Equations

• Coppock2018.instDecidableDiscretionary3 ρ p = Coppock2018.instDecidableDiscretionary3._aux_1 ρ p

@[implicit_reducible]

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

Equations

• Coppock2018.instDecidableStronglyDiscretionary3OfFintype ρ p = Coppock2018.instDecidableStronglyDiscretionary3OfFintype._aux_1 ρ p

theorem Coppock2018.StronglyDiscretionary3.discretionary3 {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) {p : Trivalent.Prop3 Ω} [Nonempty W] (h : StronglyDiscretionary3 ρ p) : Discretionary3 ρ p

Strong discretionariness entails discretionariness whenever some world exists.

Relativization to an information state (§3.5)

Discretionariness for tycka is evaluated against the common ground: an information state is a set of outlooks C, and the classification quantifies over the C-restricted refinement classes ρ ⁻¹' {w} ∩ C.

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

Objective relative to C: no C-restricted refinement class splits p.

Equations

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

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

Discretionary relative to C: some C-restricted refinement class splits p.

Equations

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

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

Strongly discretionary relative to C: every nonempty C-restricted refinement class splits p — the proposition makes a cut within every world the state leaves open.

Equations

• Coppock2018.StronglyDiscretionaryIn ρ C p = ∀ (w : W), (ρ ⁻¹' {w} ∩ C).Nonempty → ∃ o ∈ C, ∃ o' ∈ C, ρ o = w ∧ ρ o' = w ∧ p o = Trivalent.true ∧ p o' = Trivalent.false

theorem Coppock2018.stronglyDiscretionaryIn_discretionaryIn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (C : Set Ω) {p : Trivalent.Prop3 Ω} (h : StronglyDiscretionaryIn ρ C p) {w : W} (hw : (ρ ⁻¹' {w} ∩ C).Nonempty) : DiscretionaryIn ρ C p

Strong discretionariness entails discretionariness on any state leaving a world open — [Cop18]'s rendering of [KW16]: find demands radical counterstance contingency (strong discretionariness), consider mere counterstance contingency (discretionariness), so whatever embeds under find embeds under consider.

The norm of accuracy and faultlessness (§3.2)

Being at fault is relative to a world (the world of the context of utterance — contexts determine worlds, not outlooks): one is at fault for expressing φ iff φ is objectively false at that world. A strongly discretionary proposition is never objectively false at any world, so no speaker of one is ever at fault — the faultlessness half of faultless disagreement; genuine contradiction is supplied by the propositions being complements.

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

The norm of accuracy: an asserter of p is at fault at w iff p is objectively false at w.

Equations

• Coppock2018.AtFault ρ p w = Coppock2018.ObjectivelyFalseAt ρ p w

@[implicit_reducible]

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

Equations

• Coppock2018.instDecidableAtFaultOfFintypeOfDecidableEq ρ p w = Coppock2018.instDecidableAtFaultOfFintypeOfDecidableEq._aux_1 ρ p w

theorem Coppock2018.stronglyDiscretionary3_never_atFault {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) {p : Trivalent.Prop3 Ω} (h : StronglyDiscretionary3 ρ p) (w : W) : ¬AtFault ρ p w

A strongly discretionary proposition never puts its asserter at fault: every world has a refinement where it is true.

Doxastic states, acceptance, and disagreement (§3.3)

An agent's accessibility is a binary relation on outlooks ([Cop18] §5's R_a); the doxastic state at o is the set of outlooks it reaches (states vary from outlook to outlook, since 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 (Core.Logic.Modal.box) over outlooks with the proposition's truth as valuation.

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

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

Equations

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

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

An agent with accessibility R rejects p at o: p fails at every accessible outlook. Rejection is stronger than non-acceptance.

Equations

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

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

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

Equations

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

def Coppock2018.Opinionated {Ω : Type u_2} (R : Core.Logic.Modal.AccessRel Ω) (p : Trivalent.Prop3 Ω) (o : Ω) : Prop

An agent is opinionated about p at o when they accept or reject it; lack of opinionatedness — both live possibilities — is the state tycka-reports deny without contradiction ([Cop18] (38)).

Equations

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

@[implicit_reducible]

instance Coppock2018.instDecidableAccepts {Ω : Type u_2} [Fintype Ω] (R : Core.Logic.Modal.AccessRel Ω) [DecidableRel R] (p : Trivalent.Prop3 Ω) (o : Ω) : Decidable (Accepts R p o)

Equations

• Coppock2018.instDecidableAccepts R p o = Coppock2018.instDecidableAccepts._aux_1 R p o

@[implicit_reducible]

instance Coppock2018.instDecidableRejects {Ω : Type u_2} [Fintype Ω] (R : Core.Logic.Modal.AccessRel Ω) [DecidableRel R] (p : Trivalent.Prop3 Ω) (o : Ω) : Decidable (Rejects R p o)

Equations

• Coppock2018.instDecidableRejects R p o = Coppock2018.instDecidableRejects._aux_1 R p o

@[implicit_reducible]

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

Equations

• Coppock2018.instDecidableDisagreeAtOfDecidableRel R p o R₂ = Coppock2018.instDecidableDisagreeAtOfDecidableRel._aux_1 R p o R₂

@[implicit_reducible]

instance Coppock2018.instDecidableOpinionated {Ω : Type u_2} [Fintype Ω] (R : Core.Logic.Modal.AccessRel Ω) [DecidableRel R] (p : Trivalent.Prop3 Ω) (o : Ω) : Decidable (Opinionated R p o)

Equations

• Coppock2018.instDecidableOpinionated R p o = Coppock2018.instDecidableOpinionated._aux_1 R p o

The chili dialogue: faultless disagreement in a four-outlook model

Four outlooks (tasty?, opera?) : Bool × Bool refine two worlds according to the objective coordinate (whether the speaker is an opera singer); tastiness cuts across both refinement classes. John accepts the chili is tasty, Mary rejects it: genuine disagreement, and by stronglyDiscretionary3_never_atFault neither is at fault. The objective proposition I am an opera singer contrasts on both counts, and the sexy linguist hybrid ([Cop18] (10)) is discretionary without being strongly so — false at every refinement of a world where John is not a linguist, so assertable at fault.

@[reducible, inline]

abbrev Coppock2018.ChiliOutlook : Type

Chili-model outlooks: (chili is tasty?, speaker is an opera singer?).

Equations

• Coppock2018.ChiliOutlook = (Bool × Bool)

def Coppock2018.chiliWorld : ChiliOutlook → Bool

The refinement map: outlooks refine worlds that settle only the objective coordinate.

Equations

• Coppock2018.chiliWorld = Prod.snd

def Coppock2018.tasty : Trivalent.Prop3 ChiliOutlook

The chili is tasty — settled by the discretionary coordinate.

Equations

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

def Coppock2018.opera : Trivalent.Prop3 ChiliOutlook

I am an opera singer — settled by the objective coordinate.

Equations

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

def Coppock2018.sexyLinguist : Trivalent.Prop3 ChiliOutlook

John is a sexy linguist with world = linguisthood: true only where both coordinates hold, reading the objective coordinate as John is a linguist ([Cop18] (10)).

Equations

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

@[reducible, inline]

abbrev Coppock2018.johnR : Core.Logic.Modal.AccessRel ChiliOutlook

John's doxastic state: only tasty-outlooks accessible.

Equations

• Coppock2018.johnR x✝ o' = (o'.1 = true)

@[reducible, inline]

abbrev Coppock2018.maryR : Core.Logic.Modal.AccessRel ChiliOutlook

Mary's doxastic state: only non-tasty-outlooks accessible.

Equations

• Coppock2018.maryR x✝ o' = (o'.1 = false)

@[reducible, inline]

abbrev Coppock2018.openR : Core.Logic.Modal.AccessRel ChiliOutlook

An unopinionated agent: every outlook accessible (Core.Logic.Modal.universalR, inlined for decidability).

Equations

• Coppock2018.openR x✝¹ x✝ = True

theorem Coppock2018.chili_disagreement (o : ChiliOutlook) : DisagreeAt johnR maryR tasty o

The chili dialogue is a genuine disagreement: at every outlook, John accepts tasty and Mary rejects it.

theorem Coppock2018.tasty_never_atFault (w : Bool) : ¬AtFault chiliWorld tasty w

… and it is faultless: no world makes tasty objectively false, so neither party violates the norm of accuracy.

theorem Coppock2018.open_agent_unopinionated (o : ChiliOutlook) : ¬Opinionated openR tasty o

Lack of opinionatedness is representable: the open-minded agent neither accepts nor rejects tasty — the consistency of [Cop18] (38), which totally-opinionated-judge frameworks wrongly rule out.

Subjective attitude verbs (§3.5, §5)

English think and Swedish tycka 'think[opinion]' are both doxastic-acceptance operators; the only difference is that tycka carries a presupposition that its complement is strongly discretionary relative to the common ground — ∂(discretionary(φ)) ∧ □φ. The ∂-operator's role is played by PartialProp's presupposition field (the project-canonical rendering of partiality); the presupposition is outlook-independent because discretionariness is a global property of p against C.

def Coppock2018.think {Ω : Type u_2} (R : Core.Logic.Modal.AccessRel Ω) (p : Trivalent.Prop3 Ω) : Semantics.Presupposition.PartialProp Ω

think: bare doxastic acceptance, no presupposition.

Equations

• Coppock2018.think R p = { presup := fun (x : Ω) => True, assertion := Coppock2018.Accepts R p }

def Coppock2018.tycka {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (C : Set Ω) (R : Core.Logic.Modal.AccessRel Ω) (p : Trivalent.Prop3 Ω) : Semantics.Presupposition.PartialProp Ω

tycka 'think[opinion]': doxastic acceptance, presupposing that the complement is strongly discretionary relative to the information state C.

Equations

• Coppock2018.tycka ρ C R p = { presup := fun (x : Ω) => Coppock2018.StronglyDiscretionaryIn ρ C p, assertion := Coppock2018.Accepts R p }

theorem Coppock2018.think_tycka_same_assertion {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (C : Set Ω) (R : Core.Logic.Modal.AccessRel Ω) (p : Trivalent.Prop3 Ω) : (think R p).assertion = (tycka ρ C R p).assertion

think and tycka assert the same thing — the verbs differ only in tycka's discretionariness presupposition.

theorem Coppock2018.tycka_presup_survives_neg {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (C : Set Ω) (R : Core.Logic.Modal.AccessRel Ω) (p : Trivalent.Prop3 Ω) : (tycka ρ C R p).neg.presup = (tycka ρ C R p).presup

tycka's subjectivity requirement projects through negation (via PartialProp.neg): "#I don't think[opinion] it's Tuesday" is as bad as the unnegated version.

theorem Coppock2018.tycka_undefined_of_objectiveIn {W : Type u_1} {Ω : Type u_2} (ρ : Ω → W) (C : Set Ω) {p : Trivalent.Prop3 Ω} (hobj : ObjectiveIn ρ C p) {w : W} (hw : (ρ ⁻¹' {w} ∩ C).Nonempty) (R : Core.Logic.Modal.AccessRel Ω) (o : Ω) : ¬(tycka ρ C R p).presup o

An objective complement is presupposition failure for tycka, given that the state leaves some world's refinements open in a way p actually cuts — the "#I think[opinion] it's Tuesday / that she's a doctor" effect.