Tolerant, Classical, Strict (TCS) #

@cite{cobreros-etal-2012}

@cite{cobreros-etal-2012} "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 @cite{pawlak-1982} (paper's reference [19]) for the equivalence-relation case; borderline cases are exactly the boundary upper \ lower.

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 Core/Logic/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 ≡ boxR (~_P) I(P) a (Definition 9)
tolerant P at a ≡ diamondR (~_P) I(P) a (Definition 9)

The s ⊆ c ⊆ t hierarchy is the T axiom instantiated at boxR (Core.Logic.Intensional.boxR_T); the t/s duality is the standard modal de Morgan boxR R ¬p ↔ ¬diamondR R p. T-models satisfy frameConditions Logic.KTB by construction (Definition 4 of @cite{cobreros-etal-2012}); see TModel.satisfies_KTB for the explicit witness. The Brouwersche axiom B / symmetric-frame correspondence is a standard Sahlqvist result; for systematic treatment see @cite{blackburn-derijke-venema-2001} §3.5–3.6 and the model-theoretic overview @cite{goranko-otto-2007}. 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 @cite{skowron-stepaniuk-1996}; 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 Phenomena/Gradability/Studies/CobrerosEtAl2012.lean. The asymmetric reciprocation point with LassiterGoodman2017PMF.lean::lg_literal_borderline_bounded is addressed in that Studies file's §8-§9.

Tolerant, Classical, Strict (TCS) #

Paper-anchored mathematical foundation #

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

Key Results (paper-section-tagged) #

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

Architecture #