Cobreros, Egré, Ripley & van Rooij 2012: 4-Element Sorites Model

[CERvR12]

The paper's TCS apparatus together with its worked 4-element example (described in the body text on p. 354, immediately above footnote 4).

The model

Four individuals a, b, c, d arranged in a similarity chain a ~ b ~ c ~ d (with reflexivity and symmetry, no other pairs). The classical extension of tall is {a, b}. The paper uses this model to illustrate:

• The extension hierarchy: {a} ⊆ {a,b} ⊆ {a,b,c} (strict ⊆ classical ⊆ tolerant)

• Borderline cases: b and c are tolerantly tall AND tolerantly not-tall

• Two-step tolerance limit: d is NOT tolerantly tall (three steps from a exceeds Fact 3)

• Sorites resolution: each one-step inference Pa, aIb ⊨ˢᵗ Pb is valid; each two-step Pa, aIb, bIc ⊨ˢᵗ Pc is valid; but the three-step Pa, aIb, bIc, cId ⊨ˢᵗ Pd is invalid.

  Attribution: paper §3.4.1 (p. 372) demonstrates non-transitivity for ⊨ᶜᵗ (the chain Pa_1, a_1I_Pa_2, a_2I_Pa_3 ⊭ᶜᵗ Pa_3); the ⊨ˢᵗ version of the sorites is stated in §3.6 (Version 1, p. 376). The structural pattern — each step valid, chain fails — is §3.4.1's contribution; the st-instantiation here applies that pattern to the relation the paper ultimately advocates (paper p. 373).

Cross-framework note

tcs_supervaluation_disagree_concrete instantiates the existence theorem tcs_vs_supervaluation_borderline_contradiction at (soritesModel, .tall, .b). Comparator caveat: the paper's headline borderline-contradiction contrast (p. 356) is actually with Hyde 1997 subvaluationism, not with Fine 1975 supervaluation. Subvaluationism agrees with TCS that P ∧ ¬P holds at borderline cases — they disagree on framework foundations. The Lean theorem here formalises the formal-validity-side contrast (p. 359) where TCS at t mode says ✓ and supervaluation says ✗. Subvaluationism is not formalised in linglib; a proper "borderline-verdict comparator" theorem awaits its formalisation.

The asymmetric-engagement reciprocation: LassiterGoodman2017PMF.lean::lg_literal_borderline_bounded proves L&G's literal-meaning rule predicts ≤ 25% acceptance for borderline tall ∧ ¬ tall, well below the [AP11] empirical 44.7%. That paper's docstring cites TCS as the alternative that handles the data; this file's b_tolerant_contradiction shows the TCS prediction direction matches the data.

Architecture

This file is anchored on the Cobreros-Egré-Ripley-van Rooij 2012 paper itself and contains both the paper's TCS apparatus (the sections immediately below) and its worked example. General supervaluation substrate remains in Semantics/Supervaluation.lean.

The TCS apparatus

[CERvR12]

[CERvR12] "Tolerant, Classical, Strict", Journal of Philosophical Logic 41:347–385.

A similarity-based three-valued semantics for vague predicates that derives three notions of truth from a single model:

• Classical (c): standard satisfaction M ⊨ᶜ P(a) iff a ∈ I(P) (Def 9)
• Tolerant (t): M ⊨ᵗ P(a) iff ∃d ~_P a, d ∈ I(P) (Def 9)
• Strict (s): M ⊨ˢ P(a) iff ∀d ~_P a, d ∈ I(P) (Def 9)

The indifference relation ~_P is reflexive and symmetric — but, crucially, not necessarily transitive — capturing "looks the same for predicate P."

Paper-anchored mathematical foundation

The paper formulates TCS in terms of indifference relations derived from semi-orders (paper p. 350 fn 1, citing Luce 1956). The same atom-level operators are equivalently described as the lower / upper approximation operators of a tolerance approximation space in the rough-set tradition. The paper flags this analogy in footnote 5 (p. 355), citing [Paw82] (paper's reference [19]) for the equivalence-relation case; borderline cases are exactly the boundary upper \ lower.

Re-reading TCS through a modal-logic lens (formaliser's framing)

The paper itself does NOT use modal-logic vocabulary. The framing in this section is the formaliser's lens, used to integrate with the existing Semantics/Intensional/RestrictedModality.lean substrate; it is not paper-anchored.

Structurally, TCS is a propositional modal logic in which each predicate P carries its own reflexive-symmetric (KTB) Kripke accessibility relation ~_P. The strict and tolerant satisfaction operators are exactly the modal □ and ◇ over ~_P, applied to the classical extension of P:

• strict P at a ≡ box (~_P) I(P) a (Definition 9)
• tolerant P at a ≡ diamond (~_P) I(P) a (Definition 9)

The s ⊆ c ⊆ t hierarchy is the T axiom instantiated at box (ModalLogic.box_T); the t/s duality is the standard modal de Morgan box R ¬p ↔ ¬diamond R p. T-models are KTB frames by construction (Definition 4 of [CERvR12]): each ~_P carries an IsKTBFrame instance. The Brouwersche axiom B / symmetric-frame correspondence is a standard Sahlqvist result; for systematic treatment see [BdRV01] §3.5–3.6 and the model-theoretic overview [GO07]. The non-equivalence-relation generalisation of Pawlak's rough sets to tolerance approximation spaces (which the paper implicitly uses in footnote 5) is due to [SS96]; this attribution is supplied by the formaliser, not the paper.

Key Results (paper-section-tagged)

• Definition 9 (p. 353): t/s atomic clauses + their compositional lift
• Lemma 1 (p. 357): extension hierarchy s ⊆ c ⊆ t
• Facts 2-3 (p. 354): one-step + two-step tolerance principle
• Definition 10 (p. 355): borderline = upper \ lower
• Lemma 2 (p. 357): identity-model collapse of all three modes
• Definition 17 (p. 366): nine mixed consequence relations ⊨ᵐⁿ
• Lemma 7 (p. 368): strength ordering ⊨ᵗᵐ ⊆ ⊨ᶜᵐ ⊆ ⊨ˢᵐ
• Lemma 8 (p. 369): collapse cc = sc = ct = st on restricted vocabulary
• Remark 1 (p. 353), Lemma 10 (p. 371): t/s duality + self-duality of st and cc → deduction theorem
• Lemma 4 (p. 361) + Theorem 3 (p. 362): formula-level then consequence-level correspondence with LP and K3. Note: paper Lemma 4 is stated only for the restricted vocabulary (no I_P); the formalisation in §15 extends it to handle similarity atoms by treating them as classical Bool-valued (always in {0, 1} ⊂ {0, 1/2, 1}), which is a faithful extension of the paper's construction.

Cross-framework comparators (paper p. 356, p. 359)

The paper draws TWO distinct contrasts on the borderline-contradictions question, with two different opponents:

• Borderline-verdict contrast (p. 356) — TCS vs subvaluationism (Hyde 1997). Both make P ∧ ¬P true at borderline cases; the contrast is over the underlying framework foundations (TCS via similarity-based modal semantics; subvaluationism via dual super-truth). Subvaluationism is not formalised in linglib; this is the closer comparator on the verdict but cannot be checked at the Lean level here.
• Formal-validity contrast (p. 359) — TCS vs supervaluationism (Fine 1975). Supervaluationism makes P ∧ ¬P super-FALSE even at borderline cases (penumbral connection); this is the comparator formalised here, and it is realised as the §17 cross-framework theorem tcs_vs_supervaluation_borderline_contradiction. The Lean theorem combines the TCS half (IsBorderline definition unfolding through SatMode.dual) with the supervaluation half (nonContradiction_superFalse from Supervaluation/Basic.lean).

Strict truth for an atomic predicate at individual a IS supervaluation over the tolerance neighborhood of a: superTrue I(P) {d | d ~_P a}. Tolerant truth is its existential dual. This makes TCS a localized supervaluation — each individual gets its own specification space determined by its similarity neighborhood.

Architecture

This file provides the propositional restricted-vocabulary fragment of TCS — atoms cover both predicate atoms P(a) and similarity atoms a I_P b (paper Definition 8), but no quantifiers. All §2 (restricted vocabulary) results apply; phenomena requiring first-order quantifiers (paper §2.3) are out of scope.

The 4-element worked example from p. 354 of the paper (in the body text immediately above footnote 4) lives in the study sections below. The asymmetric reciprocation point with LassiterGoodman2017PMF.lean::lg_literal_borderline_bounded is addressed in §8–§9 below.

structure Semantics.Supervaluation.TCS.TModel (D : Type u_1) (Pred : Type u_2) : Type (max u_1 u_2)

A T-model: a classical model equipped with per-predicate tolerance relations. Each ~_P is reflexive and symmetric — but possibly non-transitive — capturing "looks the same for predicate P."

Definition 4 of [CERvR12]. The non-transitivity of ~_P is what makes vagueness possible: a can look like b and b can look like c, but a need not look like c.

Following the modal-logic tradition, the similarity relation is Prop-valued so that it integrates directly with box/diamond. Decidability is added per-model where computation is needed.

• interp : Pred → D → Prop

  Classical interpretation I : Pred → D → Prop.

• decInterp (P : Pred) (d : D) : Decidable (self.interp P d)

  Decidability of the interpretation (per predicate, per individual). Bundled so each TModel instance carries its own decision procedure.

• sim : Pred → D → D → Prop

  Tolerance (indifference) relation ~_P per predicate.

• sim_ktb (P : Pred) : ModalLogic.IsKTBFrame (self.sim P)

  Each ~_P is reflexive + symmetric (KTB frame).

@[instance_reducible]

instance Semantics.Supervaluation.TCS.TModel.instDecidablePredInterp {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) : DecidablePred (M.interp P)

Per-TModel decidability instance for the classical interpretation, extracted from the bundled decInterp field.

Equations

• M.instDecidablePredInterp P = M.decInterp P

@[reducible]

def Semantics.Supervaluation.TCS.TModel.simAccess {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) : D → D → Prop

The similarity relation as a Kripke accessibility relation — the frame associated with each predicate. By construction this frame is reflexive + symmetric, i.e., a KTB frame (ModalLogic.IsKTBFrame).

Equations

• M.simAccess P = M.sim P

instance Semantics.Supervaluation.TCS.TModel.instIsKTBFrameSim {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) : ModalLogic.IsKTBFrame (M.sim P)

Per-(M, P) KTB-frame instance: lets typeclass search reach Std.Refl and Std.Symm on M.sim P from any call site.

inductive Semantics.Supervaluation.TCS.TCSAtom (Pred : Type u_1) (D : Type u_2) : Type (max u_1 u_2)

Atoms of the propositional restricted vocabulary of TCS. Two constructors per Definitions 8-9 of [CERvR12]:

• pred P a ≡ P(a) — predicate application; t/c/s satisfaction clauses depend on the mode (Definition 9).
• sim P a b ≡ a I_P b — similarity predicate; classically interpreted in all modes (Definition 8, p. 353 + Remark 2, p. 354 reiterating the assumption for s/t modes).

• pred {Pred : Type u_1} {D : Type u_2} : Pred → D → TCSAtom Pred D
• sim {Pred : Type u_1} {D : Type u_2} : Pred → D → D → TCSAtom Pred D

@[reducible, inline]

abbrev Semantics.Supervaluation.TCS.TCSFormula (Pred : Type u_1) (D : Type u_2) : Type (max u_2 u_1)

TCS formulas: propositional combinations (¬, ∧) of TCS atoms. Reuses the canonical Trivalent.Formula rather than introducing a duplicate inductive — Trivalent.Formula.eval and the Trivalent.Formula.Realize lemmas apply directly.

Equations

• Semantics.Supervaluation.TCS.TCSFormula Pred D = Trivalent.Formula (Semantics.Supervaluation.TCS.TCSAtom Pred D)

def Semantics.Supervaluation.TCS.StrictAt {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : Prop

Strict atomic satisfaction: P holds at every ~_P-neighbour of a. Definition 9, atomic clause for ⊨ˢ. Modal-logic-wise, this is box (M.simAccess P) over the classical extension.

Equations

• Semantics.Supervaluation.TCS.StrictAt M P a = ∀ (d : D), M.sim P a d → M.interp P d

def Semantics.Supervaluation.TCS.TolerantAt {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : Prop

Tolerant atomic satisfaction: P holds at some ~_P-neighbour of a. Definition 9, atomic clause for ⊨ᵗ. Modal-logic-wise, this is diamond (M.simAccess P) over the classical extension.

Equations

• Semantics.Supervaluation.TCS.TolerantAt M P a = ∃ (d : D), M.sim P a d ∧ M.interp P d

theorem Semantics.Supervaluation.TCS.strictAt_eq_box {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : StrictAt M P a = ModalLogic.box (M.simAccess P) (fun (d : D) => M.interp P d) a

Strict atom = box over the similarity frame. This is definitionally true; the lemma exists to expose the modal-logic framing and to let downstream proofs invoke box_T/box_B directly.

theorem Semantics.Supervaluation.TCS.tolerantAt_eq_diamond {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : TolerantAt M P a = ModalLogic.diamond (M.simAccess P) (fun (d : D) => M.interp P d) a

Tolerant atom = diamond over the similarity frame. Definitional.

theorem Semantics.Supervaluation.TCS.StrictAt.imp_classical {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) (hs : StrictAt M P a) : M.interp P a

Strict ⟹ classical at the atomic level: if P holds for every ~_P-neighbour of a, it holds for a itself by reflexivity of ~_P. This is the T axiom instantiated.

theorem Semantics.Supervaluation.TCS.TolerantAt.of_classical {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) (hc : M.interp P a) : TolerantAt M P a

Classical ⟹ tolerant at the atomic level: a itself witnesses the existential by reflexivity of ~_P.

theorem Semantics.Supervaluation.TCS.StrictAt.imp_tolerant {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) (hs : StrictAt M P a) : TolerantAt M P a

Strict ⟹ tolerant (transitive from above).

theorem Semantics.Supervaluation.TCS.tolerance_one_step {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a b : D) (hs : StrictAt M P a) (hsim : M.sim P a b) : TolerantAt M P b

One-step tolerance (Fact 2 of [CERvR12], p. 354): if a is strictly P and a ~_P b, then b is tolerantly P. The tolerance principle ∀x∀y(P(x) ∧ x~_Py → P(y)) is t-valid.

Proof structure: strict-at-a + sim(a,b) gives classical-at-b (via the strict clause); classical implies tolerant.

theorem Semantics.Supervaluation.TCS.tolerance_two_step {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a b c : D) (hs : StrictAt M P a) (hab : M.sim P a b) (hbc : M.sim P b c) : TolerantAt M P c

Two-step tolerance (Fact 3 of [CERvR12], p. 354): tolerance propagates across two similarity steps. The third step can fail because ~_P is non-transitive — paper footnote 4 illustrates this on the 4-element model with Pa, a~b, b~c, c~d where Pd is NOT tolerantly true.

Proof: strict(a) + sim(a,b) gives classical(b); then b witnesses tolerant(c) via sim(c,b) (by symmetry).

def Semantics.Supervaluation.TCS.IsBorderline {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : Prop

Borderline: in the tolerant extension but not the strict.

Definition 10 (p. 355): b(P)^M := ⟦P⟧ᵗ \ ⟦P⟧ˢ. We adopt this set-difference form as canonical; the equivalent paraconsistent characterisation tolerant P ∧ tolerant ¬P follows from Definition 9's negation clause (tolerant ¬P ↔ ¬strict P) and is recorded as IsBorderline.iff_tolerant_pair below.

Equations

• Semantics.Supervaluation.TCS.IsBorderline M P a = (Semantics.Supervaluation.TCS.TolerantAt M P a ∧ ¬Semantics.Supervaluation.TCS.StrictAt M P a)

theorem Semantics.Supervaluation.TCS.IsBorderline.iff_both_witnesses {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : IsBorderline M P a ↔ (∃ (d : D), M.sim P a d ∧ M.interp P d) ∧ ∃ (d : D), M.sim P a d ∧ ¬M.interp P d

Borderline iff witnesses on both sides of the classical extension in the similarity neighbourhood. This is the structural reading underlying paper p. 355's discussion of borderline-as-disagreement.

def Semantics.Supervaluation.TCS.toleranceSpace {D : Type u_1} {Pred : Type u_2} [Fintype D] (M : TModel D Pred) (P : Pred) (a : D) [DecidablePred (M.sim P a)] : SpecSpace D

The tolerance neighborhood of a under P as a SpecSpace. Reflexivity of ~_P ensures a is in its own neighbourhood, so the admissible Finset is non-empty.

This makes TCS a localized supervaluation: each individual gets its own specification space (the rough-set / tolerance-approximation "granule" around it).

Equations

• Semantics.Supervaluation.TCS.toleranceSpace M P a = { admissible := Finset.filter (M.sim P a) Finset.univ, nonempty := ⋯ }

theorem Semantics.Supervaluation.TCS.StrictAt.iff_superTrue {D : Type u_1} {Pred : Type u_2} [Fintype D] (M : TModel D Pred) (P : Pred) (a : D) [DecidablePred (M.sim P a)] : StrictAt M P a ↔ superTrue (M.interp P) (toleranceSpace M P a) = Trivalent.true

Strict truth = super-truth over the tolerance neighborhood. P is strict at a iff P is super-true (true at every spec point) over a's tolerance space. The central architectural connection to Supervaluation/Basic.lean.

theorem Semantics.Supervaluation.TCS.TolerantAt.not_iff_superFalse {D : Type u_1} {Pred : Type u_2} [Fintype D] (M : TModel D Pred) (P : Pred) (a : D) [DecidablePred (M.sim P a)] : ¬TolerantAt M P a ↔ superTrue (M.interp P) (toleranceSpace M P a) = Trivalent.false

¬Tolerant = super-false over the tolerance neighborhood.

theorem Semantics.Supervaluation.TCS.IsBorderline.iff_superTrue_indet {D : Type u_1} {Pred : Type u_2} [Fintype D] (M : TModel D Pred) (P : Pred) (a : D) [DecidablePred (M.sim P a)] : IsBorderline M P a ↔ superTrue (M.interp P) (toleranceSpace M P a) = Trivalent.indet

Borderline = supervaluationally indeterminate over the tolerance neighborhood. Connects TCS to [Fin75]: borderline cases are exactly where the tolerance neighborhood disagrees on P.

inductive Semantics.Supervaluation.TCS.SatMode : Type

The three satisfaction modes of [CERvR12].

• tolerant : SatMode
• classical : SatMode
• strict : SatMode

@[instance_reducible]

instance Semantics.Supervaluation.TCS.instDecidableEqSatMode : DecidableEq SatMode

Equations

• Semantics.Supervaluation.TCS.instDecidableEqSatMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Supervaluation.TCS.instReprSatMode.repr : SatMode → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Supervaluation.TCS.instReprSatMode : Repr SatMode

Equations

• Semantics.Supervaluation.TCS.instReprSatMode = { reprPrec := Semantics.Supervaluation.TCS.instReprSatMode.repr }

@[instance_reducible]

instance Semantics.Supervaluation.TCS.instInhabitedSatMode : Inhabited SatMode

Equations

• Semantics.Supervaluation.TCS.instInhabitedSatMode = { default := Semantics.Supervaluation.TCS.instInhabitedSatMode.default }

def Semantics.Supervaluation.TCS.SatMode.dual : SatMode → SatMode

The dual operation on modes: tolerant ↔ strict, classical fixed. Encodes the mutual recursion of Definition 9: M ⊨ᵗ ¬φ iff M ⊭ˢ φ.

Equations

• Semantics.Supervaluation.TCS.SatMode.tolerant.dual = Semantics.Supervaluation.TCS.SatMode.strict
• Semantics.Supervaluation.TCS.SatMode.strict.dual = Semantics.Supervaluation.TCS.SatMode.tolerant
• Semantics.Supervaluation.TCS.SatMode.classical.dual = Semantics.Supervaluation.TCS.SatMode.classical

theorem Semantics.Supervaluation.TCS.SatMode.dual_involutive : Function.Involutive dual

dual is an involution. Packaged as Function.Involutive so downstream consumers can use mathlib's involution machinery.

@[simp]

theorem Semantics.Supervaluation.TCS.SatMode.dual_dual (m : SatMode) : m.dual.dual = m

def Semantics.Supervaluation.TCS.Sat {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) : SatMode → TCSFormula Pred D → Prop

Three-valued satisfaction (Definition 9 full). The propositional fragment of Definition 9, dispatching on mode at atoms and threading SatMode.dual through negation. Similarity atoms a I_P b are classically interpreted regardless of mode (Definition 8 + standing assumption above Definition 9).

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Supervaluation.TCS.Sat M x✝ (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.sim P a b)) = M.sim P a b
• Semantics.Supervaluation.TCS.Sat M Semantics.Supervaluation.TCS.SatMode.classical (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred P a)) = M.interp P a
• Semantics.Supervaluation.TCS.Sat M x✝ φ.neg = ¬Semantics.Supervaluation.TCS.Sat M x✝.dual φ
• Semantics.Supervaluation.TCS.Sat M x✝ (φ.conj ψ) = (Semantics.Supervaluation.TCS.Sat M x✝ φ ∧ Semantics.Supervaluation.TCS.Sat M x✝ ψ)

@[simp]

theorem Semantics.Supervaluation.TCS.Sat.atom_classical_pred {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : Sat M SatMode.classical (Trivalent.Formula.atom (TCSAtom.pred P a)) = M.interp P a

@[simp]

theorem Semantics.Supervaluation.TCS.Sat.atom_tolerant_pred {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : Sat M SatMode.tolerant (Trivalent.Formula.atom (TCSAtom.pred P a)) = TolerantAt M P a

@[simp]

theorem Semantics.Supervaluation.TCS.Sat.atom_strict_pred {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : Sat M SatMode.strict (Trivalent.Formula.atom (TCSAtom.pred P a)) = StrictAt M P a

@[simp]

theorem Semantics.Supervaluation.TCS.Sat.atom_sim {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (m : SatMode) (P : Pred) (a b : D) : Sat M m (Trivalent.Formula.atom (TCSAtom.sim P a b)) = M.sim P a b

@[simp]

theorem Semantics.Supervaluation.TCS.Sat.neg_eq {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (m : SatMode) (φ : TCSFormula Pred D) : Sat M m (Trivalent.Formula.neg φ) = ¬Sat M m.dual φ

@[simp]

theorem Semantics.Supervaluation.TCS.Sat.conj_eq {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (m : SatMode) (φ ψ : TCSFormula Pred D) : Sat M m (Trivalent.Formula.conj φ ψ) = (Sat M m φ ∧ Sat M m ψ)

theorem Semantics.Supervaluation.TCS.Sat.hierarchy {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (φ : TCSFormula Pred D) : (Sat M SatMode.strict φ → Sat M SatMode.classical φ) ∧ (Sat M SatMode.classical φ → Sat M SatMode.tolerant φ)

Lemma 1 (paper p. 357, formula level): for any TCS formula φ, strict satisfaction implies classical, and classical implies tolerant. Both directions must be proved together because the negation case for one direction needs the contrapositive of the other.

For predicate atoms this is the atomic Lemma 1 (StrictAt.imp_classical, TolerantAt.of_classical). For similarity atoms all three modes agree (similarity predicates are uniformly classical). The negation case turns into a dual-swap; conjunction is pointwise.

theorem Semantics.Supervaluation.TCS.Sat.strict_imp_classical {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (φ : TCSFormula Pred D) : Sat M SatMode.strict φ → Sat M SatMode.classical φ

theorem Semantics.Supervaluation.TCS.Sat.classical_imp_tolerant {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (φ : TCSFormula Pred D) : Sat M SatMode.classical φ → Sat M SatMode.tolerant φ

theorem Semantics.Supervaluation.TCS.Sat.strict_imp_tolerant {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (φ : TCSFormula Pred D) : Sat M SatMode.strict φ → Sat M SatMode.tolerant φ

def Semantics.Supervaluation.TCS.identityModel {D : Type u_1} {Pred : Type u_2} (interp : Pred → D → Prop) [(P : Pred) → (d : D) → Decidable (interp P d)] : TModel D Pred

An identity T-model: similarity is propositional equality. Paper Lemma 2 (p. 357): every C-model can be expanded to a T-model where t/c/s satisfaction coincide.

The construction is parameterised by an interp and produces the T-model whose similarity relation is (· = ·).

Equations

• Semantics.Supervaluation.TCS.identityModel interp = { interp := interp, decInterp := inferInstance, sim := fun (x : Pred) (d₁ d₂ : D) => d₁ = d₂, sim_ktb := ⋯ }

theorem Semantics.Supervaluation.TCS.identityModel.tolerantAt_iff {D : Type u_1} {Pred : Type u_2} (interp : Pred → D → Prop) [(P : Pred) → (d : D) → Decidable (interp P d)] (P : Pred) (a : D) : TolerantAt (identityModel interp) P a ↔ interp P a

In an identity model, tolerant atomic = classical.

theorem Semantics.Supervaluation.TCS.identityModel.strictAt_iff {D : Type u_1} {Pred : Type u_2} (interp : Pred → D → Prop) [(P : Pred) → (d : D) → Decidable (interp P d)] (P : Pred) (a : D) : StrictAt (identityModel interp) P a ↔ interp P a

In an identity model, strict atomic = classical.

theorem Semantics.Supervaluation.TCS.identityModel.modes_agree {D : Type u_1} {Pred : Type u_2} (interp : Pred → D → Prop) [(P : Pred) → (d : D) → Decidable (interp P d)] (mode : SatMode) (φ : TCSFormula Pred D) : Sat (identityModel interp) mode φ ↔ Sat (identityModel interp) SatMode.classical φ

Lemma 2 (formula level): all three modes agree in an identity model, for every formula.

@[reducible, inline]

abbrev Semantics.Supervaluation.TCS.tcsConsequence {D : Type u_1} {Pred : Type u_2} (m n : SatMode) (Γ : List (TCSFormula Pred D)) (φ : TCSFormula Pred D) : Prop

Mixed TCS-consequence (Definition 17 of [CERvR12]): Γ ⊨ᵐⁿ φ iff every T-model that m-satisfies all premises also n-satisfies the conclusion. The nine combinations (m, n ∈ {t, c, s}) yield the nine consequence relations.

Specialisation of Consequence.MixedConsequence. As an abbrev so the substrate API surface (mixed_monotone, etc.) is reachable without unfold.

Equations

• Semantics.Supervaluation.TCS.tcsConsequence m n Γ φ = Consequence.MixedConsequence Semantics.Supervaluation.TCS.Sat m n Γ φ

theorem Semantics.Supervaluation.TCS.satImplies_strict_classical {D : Type u_1} {Pred : Type u_2} : Consequence.SatImplies Sat SatMode.strict SatMode.classical

The atomic-level SatImplies witnesses for the three pairwise implications among satisfaction modes. These lift the formula-level Lemma 1 (Sat.strict_imp_classical etc.) into the abstract SatImplies shape that MixedConsequence's monotonicity API consumes.

theorem Semantics.Supervaluation.TCS.satImplies_classical_tolerant {D : Type u_1} {Pred : Type u_2} : Consequence.SatImplies Sat SatMode.classical SatMode.tolerant

theorem Semantics.Supervaluation.TCS.satImplies_strict_tolerant {D : Type u_1} {Pred : Type u_2} : Consequence.SatImplies Sat SatMode.strict SatMode.tolerant

theorem Semantics.Supervaluation.TCS.tcsConsequence.from_tolerant_premise {D : Type u_1} {Pred : Type u_2} {m : SatMode} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (h : tcsConsequence SatMode.tolerant m Γ φ) : tcsConsequence SatMode.classical m Γ φ

Lemma 7, premise-mode clause (p. 368): premise-mode strengthening coarsens consequence: ⊨ᵗᵐ ⊆ ⊨ᶜᵐ ⊆ ⊨ˢᵐ for any conclusion mode m. The "first/second part" decomposition is the formaliser's exposition; the paper states both clauses as a single result.

theorem Semantics.Supervaluation.TCS.tcsConsequence.from_classical_premise {D : Type u_1} {Pred : Type u_2} {m : SatMode} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (h : tcsConsequence SatMode.classical m Γ φ) : tcsConsequence SatMode.strict m Γ φ

theorem Semantics.Supervaluation.TCS.tcsConsequence.to_classical_conclusion {D : Type u_1} {Pred : Type u_2} {m : SatMode} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (h : tcsConsequence m SatMode.strict Γ φ) : tcsConsequence m SatMode.classical Γ φ

Lemma 7, conclusion-mode clause (p. 368): conclusion-mode weakening coarsens consequence: ⊨ᵐˢ ⊆ ⊨ᵐᶜ ⊆ ⊨ᵐᵗ for any premise mode m.

theorem Semantics.Supervaluation.TCS.tcsConsequence.to_tolerant_conclusion {D : Type u_1} {Pred : Type u_2} {m : SatMode} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (h : tcsConsequence m SatMode.classical Γ φ) : tcsConsequence m SatMode.tolerant Γ φ

def Semantics.Supervaluation.TCS.IsRestricted {D : Type u_1} {Pred : Type u_2} : TCSFormula Pred D → Prop

A TCS formula is restricted if it uses only predicate atoms. Paper §2 (p. 356) defines the restricted vocabulary as formulas free of BOTH I_P (similarity) atoms AND = (identity) atoms; this Lean substrate has no = constructor on TCSAtom, so this predicate captures only the no-I_P half of the paper's restriction. For the propositional fragment under consideration here, the two coincide.

On this fragment the Lemma 8 collapse holds (paper §3.3.1, p. 369, states ⊨ˢᵗ ⇒ ⊨ᶜᶜ, and combined with Lemma 7 monotonicity gives cc = sc = ct = st). With similarity (or identity) atoms in the language, ALL NINE consequence relations of Definition 17 become genuinely distinct (paper §3.4 full-vocabulary diagram, p. 371); the four strongest (cc, sc, ct, st) are demonstrated distinct in paper §3.4 via the one-step tolerance inference {Pa, aI_Pb} ⊨ Pb.

Equations

• Semantics.Supervaluation.TCS.IsRestricted (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred a a_1)) = True
• Semantics.Supervaluation.TCS.IsRestricted (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.sim a a_1 a_2)) = False
• Semantics.Supervaluation.TCS.IsRestricted φ.neg = Semantics.Supervaluation.TCS.IsRestricted φ
• Semantics.Supervaluation.TCS.IsRestricted (φ.conj ψ) = (Semantics.Supervaluation.TCS.IsRestricted φ ∧ Semantics.Supervaluation.TCS.IsRestricted ψ)

theorem Semantics.Supervaluation.TCS.tcsConsequence.st_imp_cc_restricted {D : Type u_1} {Pred : Type u_2} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (hΓ : ∀ ψ ∈ Γ, IsRestricted ψ) (hφ : IsRestricted φ) (hst : tcsConsequence SatMode.strict SatMode.tolerant Γ φ) : tcsConsequence SatMode.classical SatMode.classical Γ φ

Lemma 8, st ⟹ cc on restricted formulas (paper p. 369): the heart of the collapse. An st-counterexample to a cc-claim survives in the identity model where all modes agree.

The restriction to IsRestricted formulas is essential — paper §3.4 (p. 371) shows all nine consequence relations are distinct in the full vocabulary.

theorem Semantics.Supervaluation.TCS.tcsConsequence.cc_imp_st {D : Type u_1} {Pred : Type u_2} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (hcc : tcsConsequence SatMode.classical SatMode.classical Γ φ) : tcsConsequence SatMode.strict SatMode.tolerant Γ φ

cc ⟹ st by monotonicity (Lemma 7, twice). Holds unrestricted.

theorem Semantics.Supervaluation.TCS.tcsConsequence.cc_iff_st_restricted {D : Type u_1} {Pred : Type u_2} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (hΓ : ∀ ψ ∈ Γ, IsRestricted ψ) (hφ : IsRestricted φ) : tcsConsequence SatMode.classical SatMode.classical Γ φ ↔ tcsConsequence SatMode.strict SatMode.tolerant Γ φ

Lemma 8 cc ↔ st on restricted formulas: classical consequence collapses with strict-to-tolerant.

theorem Semantics.Supervaluation.TCS.tcsConsequence.cc_iff_sc_restricted {D : Type u_1} {Pred : Type u_2} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (hΓ : ∀ ψ ∈ Γ, IsRestricted ψ) (hφ : IsRestricted φ) : tcsConsequence SatMode.classical SatMode.classical Γ φ ↔ tcsConsequence SatMode.strict SatMode.classical Γ φ

Lemma 8 cc ↔ sc on restricted formulas: sandwiching via Lemma 7.

theorem Semantics.Supervaluation.TCS.tcsConsequence.cc_iff_ct_restricted {D : Type u_1} {Pred : Type u_2} {Γ : List (TCSFormula Pred D)} {φ : TCSFormula Pred D} (hΓ : ∀ ψ ∈ Γ, IsRestricted ψ) (hφ : IsRestricted φ) : tcsConsequence SatMode.classical SatMode.classical Γ φ ↔ tcsConsequence SatMode.classical SatMode.tolerant Γ φ

Lemma 8 cc ↔ ct on restricted formulas: the dual sandwich.

theorem Semantics.Supervaluation.TCS.Sat.neg_swap {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (m : SatMode) (φ : TCSFormula Pred D) : Sat M m (Trivalent.Formula.neg φ) ↔ ¬Sat M m.dual φ

Remark 1 (p. 353): satisfaction-level duality. Negation swaps the satisfaction mode via dual: M ⊨ᵐ ¬φ ↔ ¬ M ⊨^{dual m} φ. Definitionally true from Sat.neg_eq.

Note: the abstract Bilateral.SatDuality structure requires neg to be a syntactic involution (¬¬φ = φ). TCSFormula negation is NOT syntactically involutive (we have .neg (.neg φ), not φ), so the abstract structure does not literally apply. The semantic-level swap is what's needed downstream and is proved here directly.

theorem Semantics.Supervaluation.TCS.st_self_dual : Consequence.IsSelfDual SatMode.dual SatMode.strict SatMode.tolerant

Lemma 10 self-dual witnesses: the consequence relations satisfying m = dual n (equivalently n = dual m) are exactly the self-dual ones, and these are exactly the ones for which the deduction theorem holds. For TCS this gives st, ts, and cc.

theorem Semantics.Supervaluation.TCS.ts_self_dual : Consequence.IsSelfDual SatMode.dual SatMode.tolerant SatMode.strict

theorem Semantics.Supervaluation.TCS.cc_self_dual : Consequence.IsSelfDual SatMode.dual SatMode.classical SatMode.classical

noncomputable def Semantics.Supervaluation.TCS.toMV {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) : Trivalent.Model (TCSAtom Pred D)

The MV-model construction of Lemma 4 (p. 361). Each TCS atom is classified into Strong Kleene's {true, false, indet}:

• pred P a → .true if StrictAt M P a, .false if ¬TolerantAt M P a, .indet otherwise (borderline).
• sim P a b → classical: .true if similar, .false otherwise.

Definition is noncomputable because strictness/tolerance are not decidable in general (only when D is finite and sim is decidable). The local Classical.propDecidable instance makes the if-then-else well-typed; every theorem about toMV remains constructive.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Supervaluation.TCS.toMV M (Semantics.Supervaluation.TCS.TCSAtom.sim P a b) = if M.sim P a b then Trivalent.true else Trivalent.false

theorem Semantics.Supervaluation.TCS.toMV_pred_true_iff {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : toMV M (TCSAtom.pred P a) = Trivalent.true ↔ StrictAt M P a

theorem Semantics.Supervaluation.TCS.toMV_pred_false_iff {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) : toMV M (TCSAtom.pred P a) = Trivalent.false ↔ ¬TolerantAt M P a

theorem Semantics.Supervaluation.TCS.toMV_sim_true_iff {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a b : D) : toMV M (TCSAtom.sim P a b) = Trivalent.true ↔ M.sim P a b

theorem Semantics.Supervaluation.TCS.toMV_sim_false_iff {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a b : D) : toMV M (TCSAtom.sim P a b) = Trivalent.false ↔ ¬M.sim P a b

theorem Semantics.Supervaluation.TCS.tcs_lp_k3_correspondence {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (φ : TCSFormula Pred D) : (Sat M SatMode.tolerant φ ↔ Trivalent.Formula.Realize (toMV M) Trivalent.Designation.lp φ) ∧ (Sat M SatMode.strict φ ↔ Trivalent.Formula.Realize (toMV M) Trivalent.Designation.k3 φ)

Lemma 4 (p. 361, formula-level): for every T-model M and TCS formula φ,

• M ⊨ᵗ φ ↔ Trivalent.Formula.eval (toMV M) φ is LP-designated (non-false)
• M ⊨ˢ φ ↔ Trivalent.Formula.eval (toMV M) φ is K3-designated (= true)

The two halves are proved by mutual induction. The negation case uses lpSat_neg_iff/k3Sat_neg_iff from the substrate; the conjunction case uses lpSat_conj/k3Sat_conj.

theorem Semantics.Supervaluation.TCS.tolerant_iff_lp {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (φ : TCSFormula Pred D) : Sat M SatMode.tolerant φ ↔ Trivalent.Formula.Realize (toMV M) Trivalent.Designation.lp φ

Lemma 4, t-direction: tolerant satisfaction = LP-satisfaction via toMV.

theorem Semantics.Supervaluation.TCS.strict_iff_k3 {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (φ : TCSFormula Pred D) : Sat M SatMode.strict φ ↔ Trivalent.Formula.Realize (toMV M) Trivalent.Designation.k3 φ

Lemma 4, s-direction: strict satisfaction = K3-satisfaction via toMV.

theorem Semantics.Supervaluation.TCS.tcs_lp_consequence_correspondence {D : Type u_1} {Pred : Type u_2} (Γ : List (TCSFormula Pred D)) (φ : TCSFormula Pred D) : tcsConsequence SatMode.tolerant SatMode.tolerant Γ φ ↔ ∀ (M : TModel D Pred), (∀ γ ∈ Γ, Trivalent.Formula.Realize (toMV M) Trivalent.Designation.lp γ) → Trivalent.Formula.Realize (toMV M) Trivalent.Designation.lp φ

Theorem 3 (paper p. 362, consequence-level): on the restricted propositional vocabulary, t-consequence equals LP-consequence and s-consequence equals K3-consequence (modulo the toMV translation on premise/conclusion). The forward direction lifts Lemma 4 pointwise; the reverse direction uses the same toMV.

theorem Semantics.Supervaluation.TCS.tcs_k3_consequence_correspondence {D : Type u_1} {Pred : Type u_2} (Γ : List (TCSFormula Pred D)) (φ : TCSFormula Pred D) : tcsConsequence SatMode.strict SatMode.strict Γ φ ↔ ∀ (M : TModel D Pred), (∀ γ ∈ Γ, Trivalent.Formula.Realize (toMV M) Trivalent.Designation.k3 γ) → Trivalent.Formula.Realize (toMV M) Trivalent.Designation.k3 φ

Schema theorems for the non-transitivity demonstration. With similarity atoms in the formula language, we can now state and prove the structural pattern of paper §3.4.1: each one-step / two-step sorites inference is individually valid in mixed consequence, but chaining past Fact 3's two-step limit fails.

Attribution caveat: the paper's §3.4.1 demonstration of
non-transitivity is for `⊨ᶜᵗ` (the corresponding chain `Pa, aI_Pb,
bI_Pc ⊭ᶜᵗ Pc`). The `⊨ˢᵗ` version of the sorites is stated separately
in paper §3.6 (Version 1 of the sorites, p. 376). The structural
pattern — each step valid in isolation, chain fails — is what §3.4.1
contributes; the `st`-instantiation here applies the same pattern to
the relation the paper ultimately advocates (paper p. 373: "st" is
the best-motivated choice).

Each one-step inference `[Pa, a I_P b] ⊨ˢᵗ Pb` is st-valid (Fact 2 of
the paper, p. 354). Two such inferences chain to give
`[Pa, a I_P b, b I_P c] ⊨ˢᵗ Pc` via Fact 3 (two-step tolerance,
p. 354). But three steps cannot be chained: on a model where `~_P`
exhausts at two steps, `[Pa, a I_P b, b I_P c, c I_P d] ⊭ˢᵗ Pd`. The
Studies file instantiates this on the 4-element model from p. 354. 

theorem Semantics.Supervaluation.TCS.st_one_step_valid {D : Type u_1} {Pred : Type u_2} (P : Pred) (a b : D) : tcsConsequence SatMode.strict SatMode.tolerant [Trivalent.Formula.atom (TCSAtom.pred P a), Trivalent.Formula.atom (TCSAtom.sim P a b)] (Trivalent.Formula.atom (TCSAtom.pred P b))

Convenience: Pa, a I_P b ⊨ˢᵗ Pb is st-valid for every T-model (one-step tolerance, schema form). Consumes paper Fact 2.

theorem Semantics.Supervaluation.TCS.st_two_step_valid {D : Type u_1} {Pred : Type u_2} (P : Pred) (a b c : D) : tcsConsequence SatMode.strict SatMode.tolerant [Trivalent.Formula.atom (TCSAtom.pred P a), Trivalent.Formula.atom (TCSAtom.sim P a b), Trivalent.Formula.atom (TCSAtom.sim P b c)] (Trivalent.Formula.atom (TCSAtom.pred P c))

Two-step tolerance is st-valid in schema form. Consumes paper Fact 3.

Cross-framework divergence between TCS and Fine 1975 supervaluationism on borderline contradictions: TCS makes P ∧ ¬P tolerantly true while supervaluation makes it super-FALSE on the same neighbourhood. Both ingredients exist in the substrate (TolerantAt, nonContradiction_superFalse); this section combines them into a Lean-checkable existential divergence claim.

Comparator caveat: the paper's headline borderline-contradiction
contrast (p. 356) is actually with **Hyde 1997 subvaluationism**, NOT
with Fine 1975 supervaluationism. Subvaluation and TCS *agree* that
`P ∧ ¬P` holds at borderline cases; they disagree on the underlying
framework. The contrast formalised here — TCS vs supervaluation —
is the *formal-validity-side* contrast (paper p. 359, where TCS's
*t*/*s*-validity diverge from supervaluationist validity in the
quantifier-pattern sense). Subvaluationism is not formalised in
linglib; if it were, a NEW divergence theorem on the
framework-foundations axis would be the right comparator on the
*verdict* question.

A concrete instantiation on the paper's 4-element model is provided
in `Studies/CobrerosEtAl2012.lean`. 

theorem Semantics.Supervaluation.TCS.tcs_vs_supervaluation_borderline_contradiction {D : Type u_1} {Pred : Type u_2} [Fintype D] [DecidableEq D] (M : TModel D Pred) (P : Pred) (a : D) [DecidablePred (M.sim P a)] (hb : IsBorderline M P a) : Sat M SatMode.tolerant ((Trivalent.Formula.atom (TCSAtom.pred P a)).conj (Trivalent.Formula.atom (TCSAtom.pred P a)).neg) ∧ superTrue (fun (d : D) => M.interp P d ∧ ¬M.interp P d) (toleranceSpace M P a) = Trivalent.false

TCS-vs-Supervaluation borderline-contradiction divergence (schema form): for any T-model M, predicate P, and individual a that is borderline-P, the conjunction P(a) ∧ ¬P(a) is tolerantly true at a in TCS while the supervaluation of the same conjunction over the tolerance neighborhood is super-FALSE.

The two frameworks DISAGREE on the formal-validity-side verdict of borderline contradictions: TCS at t mode says ✓, supervaluation says ✗ everywhere. (Note: on the verdict question, the paper's headline contrast is with subvaluationism; see the section docstring.)

theorem Semantics.Supervaluation.TCS.tcs_borderline_excluded_middle_strict_fails {D : Type u_1} {Pred : Type u_2} (M : TModel D Pred) (P : Pred) (a : D) (hb : IsBorderline M P a) : ¬Sat M SatMode.strict ((Trivalent.Formula.atom (TCSAtom.pred P a)).conj (Trivalent.Formula.atom (TCSAtom.pred P a)).neg).neg

Paracomplete dual (schema form): on the same borderline cases, ¬(P ∧ ¬P) (i.e., excluded middle in dual form) fails strictly.

Note that strict satisfaction is the paracomplete dual of tolerant: in TCS, borderline cases satisfy P ∧ ¬P tolerantly AND fail to satisfy classical principles strictly.

inductive CobrerosEtAl2012.Elt : Type

Four individuals — the elements of the paper's chain.

• a : Elt
• b : Elt
• c : Elt
• d : Elt

@[instance_reducible]

instance CobrerosEtAl2012.instReprElt : Repr Elt

Equations

• CobrerosEtAl2012.instReprElt = { reprPrec := CobrerosEtAl2012.instReprElt.repr }

def CobrerosEtAl2012.instReprElt.repr : Elt → ℕ → Std.Format

Equations

• CobrerosEtAl2012.instReprElt.repr CobrerosEtAl2012.Elt.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CobrerosEtAl2012.Elt.a")).group prec✝
• CobrerosEtAl2012.instReprElt.repr CobrerosEtAl2012.Elt.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CobrerosEtAl2012.Elt.b")).group prec✝
• CobrerosEtAl2012.instReprElt.repr CobrerosEtAl2012.Elt.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CobrerosEtAl2012.Elt.c")).group prec✝
• CobrerosEtAl2012.instReprElt.repr CobrerosEtAl2012.Elt.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CobrerosEtAl2012.Elt.d")).group prec✝

@[instance_reducible]

instance CobrerosEtAl2012.instDecidableEqElt : DecidableEq Elt

Equations

• CobrerosEtAl2012.instDecidableEqElt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CobrerosEtAl2012.instFintypeElt : Fintype Elt

Equations

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

inductive CobrerosEtAl2012.VPred : Type

One vague predicate — "tall".

• tall : VPred

@[instance_reducible]

instance CobrerosEtAl2012.instReprVPred : Repr VPred

Equations

• CobrerosEtAl2012.instReprVPred = { reprPrec := CobrerosEtAl2012.instReprVPred.repr }

def CobrerosEtAl2012.instReprVPred.repr : VPred → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CobrerosEtAl2012.instDecidableEqVPred : DecidableEq VPred

Equations

• CobrerosEtAl2012.instDecidableEqVPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CobrerosEtAl2012.instFintypeVPred : Fintype VPred

Equations

• CobrerosEtAl2012.instFintypeVPred = { elems := {CobrerosEtAl2012.VPred.tall}, complete := CobrerosEtAl2012.instFintypeVPred._proof_1 }

def CobrerosEtAl2012.soritesSimBool : Elt → Elt → Bool

The similarity chain a ~ b ~ c ~ d with reflexivity + symmetry, nothing else. Implemented via a Bool-valued helper so the Decidable instance reduces through Bool equality, keeping the model fully computable for decide-based extension proofs.

Equations

• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.a CobrerosEtAl2012.Elt.a = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.a CobrerosEtAl2012.Elt.b = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.b CobrerosEtAl2012.Elt.a = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.b CobrerosEtAl2012.Elt.b = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.b CobrerosEtAl2012.Elt.c = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.c CobrerosEtAl2012.Elt.b = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.c CobrerosEtAl2012.Elt.c = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.c CobrerosEtAl2012.Elt.d = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.d CobrerosEtAl2012.Elt.c = true
• CobrerosEtAl2012.soritesSimBool CobrerosEtAl2012.Elt.d CobrerosEtAl2012.Elt.d = true
• CobrerosEtAl2012.soritesSimBool x✝¹ x✝ = false

def CobrerosEtAl2012.soritesSim (x y : Elt) : Prop

The similarity relation as a Prop, for direct integration with the modal-logic substrate's box/diamond.

Equations

• CobrerosEtAl2012.soritesSim x y = (CobrerosEtAl2012.soritesSimBool x y = true)

@[instance_reducible]

instance CobrerosEtAl2012.instDecidableRelEltSoritesSim : DecidableRel soritesSim

Equations

• CobrerosEtAl2012.instDecidableRelEltSoritesSim x y = CobrerosEtAl2012.instDecidableRelEltSoritesSim._aux_1 x y

def CobrerosEtAl2012.soritesModel : Semantics.Supervaluation.TCS.TModel Elt VPred

The paper's running 4-element model: I(tall) = {a, b}, similarity chain a ~ b ~ c ~ d.

Equations

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

@[instance_reducible]

instance CobrerosEtAl2012.soritesModel_sim_dec (P : VPred) (x y : Elt) : Decidable (soritesModel.sim P x y)

Per-pair decidability of the model's sim relation. Needed for decide-style proofs of the extension theorems below. Since soritesModel.sim P ignores P (definitionally soritesSim), the instance reduces to soritesSim's DecidableRel. The DecidablePred (soritesModel.sim P x) shape needed by toleranceSpace is auto-derived from this per-pair instance.

Equations

• CobrerosEtAl2012.soritesModel_sim_dec P x y = CobrerosEtAl2012.soritesModel_sim_dec._aux_1 P x y

@[instance_reducible]

instance CobrerosEtAl2012.soritesModel_strict_dec (P : VPred) (x : Elt) : Decidable (Semantics.Supervaluation.TCS.StrictAt soritesModel P x)

StrictAt is decidable on the sorites model: it's a finite universal over the 4 elements.

Equations

• CobrerosEtAl2012.soritesModel_strict_dec P x = Fintype.decidableForallFintype

@[instance_reducible]

instance CobrerosEtAl2012.soritesModel_tolerant_dec (P : VPred) (x : Elt) : Decidable (Semantics.Supervaluation.TCS.TolerantAt soritesModel P x)

TolerantAt is decidable on the sorites model: it's a finite existential.

Equations

• CobrerosEtAl2012.soritesModel_tolerant_dec P x = Fintype.decidableExistsFintype

@[instance_reducible]

instance CobrerosEtAl2012.soritesModel_borderline_dec (P : VPred) (x : Elt) : Decidable (Semantics.Supervaluation.TCS.IsBorderline soritesModel P x)

Equations

• CobrerosEtAl2012.soritesModel_borderline_dec P x = CobrerosEtAl2012.soritesModel_borderline_dec._aux_1 P x

theorem CobrerosEtAl2012.strict_extension : Semantics.Supervaluation.TCS.StrictAt soritesModel VPred.tall Elt.a ∧ ¬Semantics.Supervaluation.TCS.StrictAt soritesModel VPred.tall Elt.b ∧ ¬Semantics.Supervaluation.TCS.StrictAt soritesModel VPred.tall Elt.c ∧ ¬Semantics.Supervaluation.TCS.StrictAt soritesModel VPred.tall Elt.d

Strict extension of tall: {a} only. Other elements have similar individuals that aren't classically tall.

theorem CobrerosEtAl2012.classical_extension : soritesModel.interp VPred.tall Elt.a ∧ soritesModel.interp VPred.tall Elt.b ∧ ¬soritesModel.interp VPred.tall Elt.c ∧ ¬soritesModel.interp VPred.tall Elt.d

Classical extension of tall: {a, b} directly from I(tall).

theorem CobrerosEtAl2012.tolerant_extension : Semantics.Supervaluation.TCS.TolerantAt soritesModel VPred.tall Elt.a ∧ Semantics.Supervaluation.TCS.TolerantAt soritesModel VPred.tall Elt.b ∧ Semantics.Supervaluation.TCS.TolerantAt soritesModel VPred.tall Elt.c ∧ ¬Semantics.Supervaluation.TCS.TolerantAt soritesModel VPred.tall Elt.d

Tolerant extension of tall: {a, b, c}. d is too far from the classical extension to count as tolerantly tall (three steps from a, exceeding Fact 3's two-step limit).

theorem CobrerosEtAl2012.b_is_borderline : Semantics.Supervaluation.TCS.IsBorderline soritesModel VPred.tall Elt.b

b is borderline-tall: tolerantly tall (witness: a), but not strictly tall (counter-witness: c, which is similar to b but not classically tall).

theorem CobrerosEtAl2012.c_is_borderline : Semantics.Supervaluation.TCS.IsBorderline soritesModel VPred.tall Elt.c

c is borderline-tall: tolerantly tall (witness: b), but not strictly tall (counter-witness: d).

theorem CobrerosEtAl2012.a_not_borderline : ¬Semantics.Supervaluation.TCS.IsBorderline soritesModel VPred.tall Elt.a

a is NOT borderline: strictly tall, hence not in tolerant \ strict.

theorem CobrerosEtAl2012.d_not_borderline : ¬Semantics.Supervaluation.TCS.IsBorderline soritesModel VPred.tall Elt.d

d is NOT borderline: not even tolerantly tall, hence not in tolerant \ strict.

theorem CobrerosEtAl2012.b_tolerant_contradiction : Semantics.Supervaluation.TCS.Sat soritesModel Semantics.Supervaluation.TCS.SatMode.tolerant ((Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.b)).conj (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.b)).neg)

At the borderline individual b, tall ∧ ¬ tall is tolerantly true in TCS — the paraconsistent feature. Compare with the same conjunction being super-FALSE in supervaluation: see §8 below.

theorem CobrerosEtAl2012.c_tolerant_contradiction : Semantics.Supervaluation.TCS.Sat soritesModel Semantics.Supervaluation.TCS.SatMode.tolerant ((Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.c)).conj (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.c)).neg)

Same for c.

theorem CobrerosEtAl2012.a_no_tolerant_contradiction : ¬Semantics.Supervaluation.TCS.Sat soritesModel Semantics.Supervaluation.TCS.SatMode.tolerant ((Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.a)).conj (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.a)).neg)

At the non-borderline individual a (strictly tall), the contradiction tall ∧ ¬ tall is NOT tolerantly true.

theorem CobrerosEtAl2012.d_no_tolerant_contradiction : ¬Semantics.Supervaluation.TCS.Sat soritesModel Semantics.Supervaluation.TCS.SatMode.tolerant ((Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.d)).conj (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.d)).neg)

Dually for d (not even tolerantly tall).

theorem CobrerosEtAl2012.tcs_supervaluation_disagree_concrete : Semantics.Supervaluation.TCS.Sat soritesModel Semantics.Supervaluation.TCS.SatMode.tolerant ((Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.b)).conj (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.b)).neg) ∧ Semantics.Supervaluation.superTrue (fun (e : Elt) => (decide (soritesModel.interp VPred.tall e) && !decide (soritesModel.interp VPred.tall e)) = true) (Semantics.Supervaluation.TCS.toleranceSpace soritesModel VPred.tall Elt.b) = Trivalent.false

Cross-framework divergence theorem, instantiated at (soritesModel, .tall, .b).

On the same tolerance neighborhood {d | b ~ d}:

• TCS says tall(b) ∧ ¬ tall(b) is tolerantly true
• Fine 1975 supervaluation says it is super-FALSE (= Trivalent.false)

The frameworks disagree on the formal-validity-side verdict. Caveat (per the file docstring): the paper's headline contrast on borderline contradictions (p. 356) is with Hyde 1997 subvaluationism, which agrees with TCS on the verdict. Fine 1975 supervaluation is the comparator we can formalise here because it's the only one of the two with a substrate in linglib.

Non-transitivity in the full vocabulary with similarity predicates Iₚ. Each one-step Pa, aIb ⊨ˢᵗ Pb is valid (Fact 2, p. 354); each two-step Pa, aIb, bIc ⊨ˢᵗ Pc is valid (Fact 3, p. 354); but three-step Pa, aIb, bIc, cId ⊨ˢᵗ Pd is invalid because d requires three similarity steps from the classical extension {a, b}, exceeding Fact 3's two-step limit.

Attribution: paper §3.4.1 (p. 372) demonstrates non-transitivity for
`⊨ᶜᵗ` (the chain `Pa_1, a_1I_Pa_2, a_2I_Pa_3 ⊭ᶜᵗ Pa_3`), and
footnote 14 formalises the simple-transitivity statement. The `⊨ˢᵗ`
sorites version is in §3.6 (Version 1, p. 376). The structural
pattern (each step valid, chain fails) is §3.4.1's contribution; the
`st`-instantiation here transfers it to the relation the paper
advocates. 

theorem CobrerosEtAl2012.st_one_step_a_to_b : Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [CobrerosEtAl2012.fmlPa✝, CobrerosEtAl2012.fmlIab✝] CobrerosEtAl2012.fmlPb✝

One-step st-validity, instantiated to the model: tall(a), aIb ⊨ˢᵗ tall(b). The schema theorem Semantics.Supervaluation.TCS.st_one_step_valid instantiates here.

theorem CobrerosEtAl2012.st_two_step_a_to_c : Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [CobrerosEtAl2012.fmlPa✝, CobrerosEtAl2012.fmlIab✝, CobrerosEtAl2012.fmlIbc✝] CobrerosEtAl2012.fmlPc✝

Two-step st-validity: tall(a), aIb, bIc ⊨ˢᵗ tall(c).

theorem CobrerosEtAl2012.st_three_step_invalid : ¬Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [CobrerosEtAl2012.fmlPa✝, CobrerosEtAl2012.fmlIab✝, CobrerosEtAl2012.fmlIbc✝, CobrerosEtAl2012.fmlIcd✝] CobrerosEtAl2012.fmlPd✝

Three-step st-INVALIDITY: tall(a), aIb, bIc, cId ⊭ˢᵗ tall(d).

Each step is individually st-valid (above), but the chain of three exhausts the two-step tolerance limit (Fact 3, p. 354), so the conclusion fails to hold even tolerantly at d. Structural pattern of paper §3.4.1; paper itself states the ⊨ᶜᵗ version there and the ⊨ˢᵗ sorites Version 1 in §3.6 (p. 376).

theorem CobrerosEtAl2012.st_chain_breaks_at_step_three : Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [CobrerosEtAl2012.fmlPa✝, CobrerosEtAl2012.fmlIab✝] CobrerosEtAl2012.fmlPb✝ ∧ Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [CobrerosEtAl2012.fmlPa✝, CobrerosEtAl2012.fmlIab✝, CobrerosEtAl2012.fmlIbc✝] CobrerosEtAl2012.fmlPc✝ ∧ ¬Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [CobrerosEtAl2012.fmlPa✝, CobrerosEtAl2012.fmlIab✝, CobrerosEtAl2012.fmlIbc✝, CobrerosEtAl2012.fmlIcd✝] CobrerosEtAl2012.fmlPd✝

Convenience packaging: the chain of one-step + two-step st-valid inferences cannot be extended to three steps, even though each constituent step is valid.

Two Lean-checkable cross-framework theorems that close gaps flagged by the cross-framework reconciler:

1. **TCS-vs-product-rule expressivity gap**: TCS predicts borderline
   contradictions *categorically* (the conjunction is true, not
   fractional); any framework that predicts them as a product of
   complementary probabilities is *fractionally bounded* by 1/4
   (AM-GM). The architectural divergence between TCS and L&G's
   literal rule is structural, not parametric.
2. **Klein-delineation tension**: in `soritesModel`, two adjacent
   individuals are tolerantly similar AND both borderline, yet
   classically separated — exactly the configuration where any
   sound Klein delineation would over-impose a scalar relation. 

theorem CobrerosEtAl2012.tcs_borderline_contradiction_categorical {D' : Type u_1} {Pred' : Type u_2} (M : Semantics.Supervaluation.TCS.TModel D' Pred') (P : Pred') (a : D') (hb : Semantics.Supervaluation.TCS.IsBorderline M P a) : Semantics.Supervaluation.TCS.Sat M Semantics.Supervaluation.TCS.SatMode.tolerant ((Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred P a)).conj (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred P a)).neg)

TCS predicts borderline contradictions categorically. Helper: for any T-model M, predicate P, and individual a that is borderline-P, the conjunction P(a) ∧ ¬P(a) is tolerantly true. Extracted from the TCS half of tcs_vs_supervaluation_borderline_contradiction.

theorem CobrerosEtAl2012.tcs_categorical_vs_product_bounded {D' : Type u_1} {Pred' : Type u_2} (M : Semantics.Supervaluation.TCS.TModel D' Pred') (P : Pred') (a : D') (hb : Semantics.Supervaluation.TCS.IsBorderline M P a) (q : ℝ) : Semantics.Supervaluation.TCS.Sat M Semantics.Supervaluation.TCS.SatMode.tolerant ((Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred P a)).conj (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred P a)).neg) ∧ q * (1 - q) ≤ 1 / 4

TCS-vs-product-rule framework expressivity gap. A framework-level contrast theorem with two simultaneous halves, witnessing that TCS and any "literal rule = product of complementary probabilities" framework (paradigmatically L&G: Studies/LassiterGoodman2017PMF.lean::lg_literal_borderline_bounded) diverge structurally on borderline contradictions:

• TCS half: the conjunction P(a) ∧ ¬P(a) is tolerantly TRUE (not fractional) at every borderline a. This is a categorical framework prediction — independent of any parameter.
• Product-rule half: any product q · (1 - q) for q ∈ [0, 1] is bounded above by 1/4 (AM-GM). This is the framework-level ceiling on any literal-meaning rule that multiplies a probability by its complement. L&G's lg_literal_borderline_bounded is the PMF-typed instance of this generic bound.

The empirical Alxatib-Pelletier 2011 acceptance rate (44.7% — see the [AP11] contrast section of Studies/LassiterGoodman2017PMF.lean) exceeds the product-rule's 25% ceiling, refuting the literal-rule framework empirically. TCS's categorical prediction is consistent with the empirical direction without committing to any specific fractional value. The structural divergence is what's interesting: L&G's framework architecture cannot represent the empirical direction (any literal-rule PMF is bounded ≤ 25%); TCS's framework architecture predicts it categorically.

theorem CobrerosEtAl2012.klein_delineation_tension_concrete : Semantics.Supervaluation.TCS.IsBorderline soritesModel VPred.tall Elt.b ∧ Semantics.Supervaluation.TCS.IsBorderline soritesModel VPred.tall Elt.c ∧ soritesModel.sim VPred.tall Elt.b Elt.c ∧ soritesModel.interp VPred.tall Elt.b ∧ ¬soritesModel.interp VPred.tall Elt.c

Klein-delineation tension witness: in soritesModel, the individuals b and c are both borderline-tall AND tolerantly similar (b ~_tall c), yet classically separated (b is classically tall, c is classically not-tall). Any Klein-style sound delineation derived from M.interp .tall would impose a scalar relation R b c on this pair (per Semantics/Degree/Delineation.lean::IsSoundDelineation), over-generating where TCS says b and c are both equally borderline and the scalar relation should be unwarranted.

This is the Lean-checkable witness for the prose tension flagged at Comparison/Delineation.lean lines 566-571.

theorem CobrerosEtAl2012.sorites_chain_invalid : ¬Semantics.Supervaluation.TCS.tcsConsequence Semantics.Supervaluation.TCS.SatMode.strict Semantics.Supervaluation.TCS.SatMode.tolerant [Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.a)] (Trivalent.Formula.atom (Semantics.Supervaluation.TCS.TCSAtom.pred VPred.tall Elt.d))

Single-premise sorites unsoundness (the previous formalization's sorites_chain_invalid). Subsumed by st_three_step_invalid above but kept under the historical name.