Pragmatic usability of trivalent propositions

Križ evaluates a trivalent proposition W → SignType relative to an issue, a partition Setoid W of the worlds. A proposition is sufficientlyTrue at a world when the world's cell contains a world where it is true, addressesIssue when no cell contains both a true and a false world, and usable at a world when it is not false there, is sufficiently true there, and addresses the issue. Non-maximal readings are usability at gap-worlds (gap_enables_nonmax), gap removal blocks them (metaAssert_prevents_nonmax), and tolerated exceptions cannot be mentioned (exception_unaddressable). Strong relevance, after Križ and Spector, is the bivalent counterpart of addressing, holding when the issue decides the proposition (Setoid.Decides).

Main definitions

• sufficientlyTrue, addressesIssue, usable: Križ's weakened Quality.
• communicatedContent: worlds compatible with what is communicated.
• isStronglyRelevantProp: constancy on issue cells.
• bivalentPred: Bool-valued truth predicate of a bivalent proposition.

References

• [Kri16]
• [KS21b]

def Homogeneity.sufficientlyTrue {W : Type u_1} (q : Setoid W) (p : W → SignType) (w : W) : Prop

p is true enough at w relative to the issue q when some q-equivalent world makes p literally true. This weakens the maxim of Quality, so that a speaker need only assert something equivalent, for current purposes, to something true.

Equations

• Homogeneity.sufficientlyTrue q p w = ∃ (w' : W), q w w' ∧ p w' = 1

@[instance_reducible]

instance Homogeneity.sufficientlyTrue.instDecidable {W : Type u_1} [Fintype W] (q : Setoid W) [DecidableRel ⇑q] (p : W → SignType) (w : W) : Decidable (sufficientlyTrue q p w)

Equations

• Homogeneity.sufficientlyTrue.instDecidable q p w = { decide := decide (∃ a ∈ Finset.univ, (fun (w' : W) => q w w' ∧ p w' = 1) a), reflects_decide := ⋯ }

theorem Homogeneity.literal_imp_sufficient {W : Type u_1} (q : Setoid W) (p : W → SignType) (w : W) (h : p w = 1) : sufficientlyTrue q p w

Literal truth implies sufficient truth, for any issue.

def Homogeneity.addressesIssue {W : Type u_1} (q : Setoid W) (p : W → SignType) : Prop

p addresses issue q when no cell of q overlaps both the positive and the negative extension. Gap-worlds do not count, since only cells straddling the true/false boundary disqualify.

Equations

• Homogeneity.addressesIssue q p = ¬∃ (w₁ : W) (w₂ : W), q w₁ w₂ ∧ p w₁ = 1 ∧ p w₂ = -1

@[instance_reducible]

instance Homogeneity.addressesIssue.instDecidable {W : Type u_1} [Fintype W] (q : Setoid W) [DecidableRel ⇑q] (p : W → SignType) : Decidable (addressesIssue q p)

Equations

• Homogeneity.addressesIssue.instDecidable q p = { decide := !decide (∃ (w₁ : W) (w₂ : W), q w₁ w₂ ∧ p w₁ = 1 ∧ p w₂ = -1), reflects_decide := ⋯ }

def Homogeneity.usable {W : Type u_1} (q : Setoid W) (p : W → SignType) (w : W) : Prop

p may be used at w when it is not false at w, sufficiently true at w, and addresses the issue.

Equations

• Homogeneity.usable q p w = (p w ≠ -1 ∧ Homogeneity.sufficientlyTrue q p w ∧ Homogeneity.addressesIssue q p)

@[instance_reducible]

instance Homogeneity.usable.instDecidable {W : Type u_1} [Fintype W] (q : Setoid W) [DecidableRel ⇑q] (p : W → SignType) (w : W) : Decidable (usable q p w)

Equations

• Homogeneity.usable.instDecidable q p w = { decide := decide (p w ≠ -1) && decide (Homogeneity.sufficientlyTrue q p w ∧ Homogeneity.addressesIssue q p), reflects_decide := ⋯ }

theorem Homogeneity.usable_iff_of_isBivalent {W : Type u_1} {p : W → SignType} (hbiv : Trivalent.IsBivalent p) (q : Setoid W) (w : W) : usable q p w ↔ p w = 1 ∧ addressesIssue q p

For a bivalent proposition, usability is literal truth plus addressing, since sufficient truth adds nothing without gap-worlds.

Usability at gap-worlds

theorem Homogeneity.gap_enables_nonmax {W : Type u_1} (q : Setoid W) (p : W → SignType) (w w' : W) (hGap : p w = 0) (hEquiv : q w w') (hTrue : p w' = 1) (hAddr : addressesIssue q p) : usable q p w

The gap enables non-maximal use — a gapped world whose cell contains a true-world is usable, given addressing.

theorem Homogeneity.metaAssert_prevents_nonmax {W : Type u_1} (q : Setoid W) (p : W → SignType) (w : W) (h : usable q ((fun (v : SignType) => SignType.ofProp (v = 1)) ∘ p) w) : SignType.ofProp (p w = 1) = 1

Gap removal forces literal truth for usability, the general form of the result that homogeneity removers prevent non-maximal use.

theorem Homogeneity.exception_unaddressable {W : Type u_1} (q : Setoid W) (p e : W → SignType) (w : W) (hUse : usable q p w) (hEw : e w = 1) (hEfalse : ∀ (w' : W), p w' = 1 → e w' = -1) : ¬addressesIssue q e

Exceptions are unmentionable ([Kri16] §4.1). When p is used at w under the issue q, an exception-mentioning sentence e, true at w but false wherever p is literally true, cannot address the same issue, since w's cell contains a literally-true world and e straddles the true/false boundary between w and that world.

Communicated content

def Homogeneity.communicatedContent {W : Type u_1} (q : Setoid W) (p : W → SignType) : Set W

The worlds the hearer considers possible after hearing p under issue q are those indistinguishable, for current purposes, from a world where p is literally true.

Equations

• Homogeneity.communicatedContent q p = {w : W | Homogeneity.sufficientlyTrue q p w}

@[simp]

theorem Homogeneity.mem_communicatedContent {W : Type u_1} {q : Setoid W} {p : W → SignType} {w : W} : w ∈ communicatedContent q p ↔ sufficientlyTrue q p w

@[instance_reducible]

instance Homogeneity.communicatedContent.instDecidableMem {W : Type u_1} [Fintype W] (q : Setoid W) [DecidableRel ⇑q] (p : W → SignType) (w : W) : Decidable (w ∈ communicatedContent q p)

Equations

• Homogeneity.communicatedContent.instDecidableMem q p w = { decide := decide (∃ a ∈ Finset.univ, (fun (w' : W) => q w w' ∧ p w' = 1) a), reflects_decide := ⋯ }

theorem Homogeneity.posExt_subset_communicated {W : Type u_1} (q : Setoid W) (p : W → SignType) : Trivalent.posExt p ⊆ communicatedContent q p

Literal truth is always communicated.

theorem Homogeneity.communicatedContent_eq_posExt {W : Type u_1} {p : W → SignType} (hbiv : Trivalent.IsBivalent p) (q : Setoid W) (hAddr : addressesIssue q p) : communicatedContent q p = Trivalent.posExt p

For a bivalent proposition that addresses the issue, communicated content is exactly the positive extension, with no pragmatic weakening.

theorem Homogeneity.communicatedContent_antitone {W : Type u_1} {q q' : Setoid W} (p : W → SignType) (hRef : q' ≤ q) : communicatedContent q' p ⊆ communicatedContent q p

Coarser issues communicate more — if q' refines q, everything communicated under q' is communicated under q. This is [Kri16]'s key prediction that coarse issues enable non-maximal use.

Strong relevance

Bivalent counterpart of addressesIssue, from [KS21b]: a W → Prop is strongly relevant to an issue when it is constant on each cell, that is, when the issue decides it; Addressing has it as its special case on bivalent propositions (KrizSpector2021.addressesIssue_iff_stronglyRelevant).

@[reducible, inline]

abbrev Homogeneity.isStronglyRelevantProp {W : Type u_1} (q : Setoid W) (p : W → Prop) : Prop

A proposition is strongly relevant to an issue iff the issue decides it.

Equations

• Homogeneity.isStronglyRelevantProp q p = q.Decides {w : W | p w}

def Homogeneity.stronglyRelevantSet {W : Type u_1} (q : Setoid W) (candidates : Set (W → Prop)) : Set (W → Prop)

Filter a set of propositions to those strongly relevant to q.

Equations

• Homogeneity.stronglyRelevantSet q candidates = {p : W → Prop | p ∈ candidates ∧ Homogeneity.isStronglyRelevantProp q p}

theorem Homogeneity.trivial_relevant_iff_constant {W : Type u_1} (p : W → Prop) : isStronglyRelevantProp ⊤ p ↔ ∀ (w₁ w₂ : W), p w₁ ↔ p w₂

With the trivial issue, strong relevance is constancy on W.

theorem Homogeneity.exact_all_relevant {W : Type u_1} (p : W → Prop) : isStronglyRelevantProp ⊥ p

With the finest issue, every proposition is strongly relevant.

theorem Homogeneity.exact_stronglyRelevantSet_eq {W : Type u_1} (candidates : Set (W → Prop)) : stronglyRelevantSet ⊥ candidates = candidates

With the finest issue, the strongly-relevant filter is the identity.

def Homogeneity.bivalentPred {W : Type u_1} (p : W → SignType) : W → Bool

The Bool truth predicate of a proposition. Bridges the trivalent Addressing constraint to bivalent strong-relevance filtering ([KS21b]).

Equations

• Homogeneity.bivalentPred p w = (p w == 1)