Tolerant, Classical, Strict (TCS) #
@cite{cobreros-etal-2012}
@cite{cobreros-etal-2012} "Tolerant, Classical, Strict." Journal of Philosophical Logic 41:347–385.
Overview #
A similarity-based semantics for vague predicates that derives three notions of truth from a single model:
- Classical (c): standard satisfaction M ⊨c P(a) iff a ∈ I(P)
- Tolerant (t): M ⊨t P(a) iff ∃d ~_P a, d ∈ I(P)
- Strict (s): M ⊨s P(a) iff ∀d ~_P a, d ∈ I(P)
The tolerance relation ~_P is reflexive and symmetric (but not transitive) — an indifference relation for predicate P.
Key Results #
- Extension hierarchy: strict ⊆ classical ⊆ tolerant (Lemma 1)
- Tolerance is t-valid: ∀x∀y(P(x) ∧ x~_Py → P(y)) (Fact 2)
- Two-step tolerance: ∀x∀y∀z(P(x) ∧ x~_Py ∧ y~_Pz → P(z)) (Fact 3)
- Borderline contradictions: borderline cases tolerantly satisfy P ∧ ¬P
- LP/K3 correspondence: t-consequence = LP-consequence, s-consequence = K3-consequence (Theorem 3)
Connection to Supervaluation #
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 the existential dual (sub-truth). This makes TCS a
localized supervaluation — each individual gets its own specification
space determined by its similarity neighborhood.
Unlike standard supervaluationism, TCS allows borderline contradictions: P ∧ ¬P is tolerantly true for borderline cases. In supervaluationism, P ∧ ¬P is super-false even when P is borderline (penumbral connection). This difference traces to TCS negation: tolerant ¬φ = not strictly φ (weaker than not classically φ).
Architecture #
This file provides the core TCS framework. It connects to
Supervaluation/Basic.lean by showing that strict/tolerant truth
instantiate superTrue over tolerance neighborhoods.
A T-model: a classical model equipped with tolerance (indifference) relations per predicate. Each ~_P is reflexive and symmetric but possibly non-transitive — capturing "looks the same" for predicate P.
Definition 4 of @cite{cobreros-etal-2012}. 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.
- interp : Pred → D → Bool
Classical interpretation: I(P) ∈ {0,1}^D
- sim : Pred → D → D → Bool
Tolerance relation ~_P per predicate
Reflexivity: every individual is similar to itself
Symmetry: similarity is undirected
Instances For
Tolerant atomic satisfaction: M ⊨t P(a) iff some P-similar individual classically satisfies P. Definition 9, t-atomic.
Equations
Instances For
Strict atomic satisfaction: M ⊨s P(a) iff every P-similar individual classically satisfies P. Definition 9, s-atomic.
Equations
Instances For
Strict ⟹ classical: if P holds for all similar individuals, it holds for a itself (by reflexivity of ~_P).
Strict ⟹ tolerant (transitive from above).
Strict P at a, plus a ~_P b, gives classical P at b. The strict extension is closed under similarity.
One-step tolerance (Fact 2): if a is strictly P and a _P b,
then b is tolerantly P. This is the tolerance principle
∀x∀y(P(x) ∧ x_Py → P(y)) being t-valid: the premises hold
strictly, the conclusion holds tolerantly.
Proof: strict(a) + sim(a,b) → classical(b) → tolerant(b).
Two-step tolerance (Fact 3): tolerance propagates across
two similarity steps. If strictly P(a), a _P b, b _P c, then
tolerantly P(c). Two steps is the maximum: the third step can
fail because ~_P is non-transitive.
Proof: strict(a) + sim(a,b) → classical(b). Then b witnesses tolerant(c) via sim(c,b) (by symmetry).
An individual is borderline-P if it is in the tolerant extension but not the strict extension. Equivalently: tolerantly P AND tolerantly ¬P (since tolerant ¬P = not strictly P).
Equations
Instances For
Borderline ↔ witnesses exist on both sides: some P-similar individual is classically P, and some is classically not-P.
Borderline cases satisfy tolerant contradictions: tolerantly P AND not strictly P (= tolerantly ¬P). Unlike supervaluationism where P ∧ ¬P is super-false even for borderline cases, TCS allows borderline contradictions because tolerant negation only requires strict truth to fail.
The tolerance neighborhood of a under P: the set of individuals
P-similar to a. This is a SpecSpace because ~_P is reflexive
(a is always in its own neighborhood).
This makes TCS a localized supervaluation: each individual gets its own specification space.
Equations
Instances For
Strict truth = super-truth over the tolerance neighborhood.
An individual strictly satisfies P iff P is true at ALL
specification points (P-similar individuals) in its tolerance
space. This is the central architectural connection to
Supervaluation/Basic.lean.
¬Tolerant = super-false over the tolerance neighborhood. An individual is not tolerantly P iff P is false at ALL specification points in its tolerance space.
Borderline = indefinite under supervaluation. An individual is borderline-P in TCS iff P is indefinite (neither super-true nor super-false) over its tolerance space.
This connects TCS to @cite{fine-1975}'s supervaluationism: borderline cases are exactly the cases where the tolerance neighborhood disagrees — some similar individuals satisfy P, others don't.
Propositional TCS formulas with ground atomic predications. No quantifiers — the key results (hierarchy, tolerance, borderline contradictions) are visible at this level.
- atom {Pred : Type u_3} {D : Type u_4} : Pred → D → TCSFormula Pred D
- neg {Pred : Type u_3} {D : Type u_4} : TCSFormula Pred D → TCSFormula Pred D
- conj {Pred : Type u_3} {D : Type u_4} : TCSFormula Pred D → TCSFormula Pred D → TCSFormula Pred D
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dual mode: negation swaps t ↔ s and leaves c fixed. This encodes the mutual recursion of Definition 9: tolerant negation checks strict failure, strict negation checks tolerant failure.
Equations
Instances For
Three-valued satisfaction (Definition 9). The mutual recursion
between t and s through negation is encoded via SatMode.dual.
Equations
- Semantics.Supervaluation.TCS.sat M Semantics.Supervaluation.TCS.SatMode.classical (Semantics.Supervaluation.TCS.TCSFormula.atom P a) = M.interp P a
- Semantics.Supervaluation.TCS.sat M Semantics.Supervaluation.TCS.SatMode.tolerant (Semantics.Supervaluation.TCS.TCSFormula.atom P a) = Semantics.Supervaluation.TCS.tolerantAtom M P a
- Semantics.Supervaluation.TCS.sat M Semantics.Supervaluation.TCS.SatMode.strict (Semantics.Supervaluation.TCS.TCSFormula.atom P a) = Semantics.Supervaluation.TCS.strictAtom M 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✝ ψ)
Instances For
Lemma 1 (full formula level): for any formula φ, strict satisfaction implies classical, and classical implies tolerant. The negation case uses contrapositive of the other direction — this is why both directions must be proved together.
Remark 1: tolerant and strict are duals. M ⊨t φ iff M ⊭s ¬φ, and M ⊨s φ iff M ⊭t ¬φ. This falls out of the definition: sat .tolerant (neg φ) = !(sat .strict φ).
Dual direction: M ⊨s φ iff M ⊭t ¬φ.
The paper's running example (p. 354–355): four individuals
a, b, c, d in a chain of pairwise similarities.
I(P) = {a, b}: a and b are classically tall.
a _P b _P c ~_P d (chain), nothing else beyond reflexivity.
Predictions:
- Strict extension: {a} (only a has ALL neighbors classically P)
- Classical extension: {a, b}
- Tolerant extension: {a, b, c} (c has neighbor b who is P)
- Borderline: {b, c}
- b and c tolerantly satisfy P ∧ ¬P
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Semantics.Supervaluation.TCS.instBEqElt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@cite{cobreros-etal-2012} §3: from three notions of satisfaction {s, c, t} we obtain nine consequence relations ⊨ᵐⁿ by varying the standard for premises (m) and conclusions (n).
Lift Boolean satisfaction to Prop for use with MixedConsequence.
Equations
- Semantics.Supervaluation.TCS.satProp M mode φ = (Semantics.Supervaluation.TCS.sat M mode φ = true)
Instances For
The nine TCS consequence relations as instances of MixedConsequence.
Equations
Instances For
Strict satisfaction implies classical.
Classical satisfaction implies tolerant.
Strict satisfaction implies tolerant (transitive).
An identity T-model: similarity is the identity relation. In such models, tolerant = classical = strict for all formulas, since the only element similar to a is a itself.
This is the key construction in @cite{cobreros-etal-2012} Lemma 2: every C-model can be expanded to a T-model where all three notions of satisfaction coincide.
Equations
Instances For
In an identity model, tolerant satisfaction equals classical.
In an identity model, strict satisfaction equals classical.
All modes agree in an identity model (Lemma 2). For any formula, satisfaction under all three modes coincides.
Lemma 8: cc = sc = ct = st. All four relations coincide.
Proof strategy:
- cc ⊆ sc ⊆ st (by premise/conclusion monotonicity)
- cc ⊆ ct ⊆ st (by premise/conclusion monotonicity)
- st ⊆ cc (by identity model argument: every cc-counterexample gives an st-counterexample via the identity model)
Hence all four are equal. We prove st ⊆ cc; the rest follow from monotonicity.
cc ⊆ st (by monotonicity).
cc = st: the four mixed consequence relations coincide.
Satisfaction-level duality: M ⊨ᵐ ¬φ iff M ⊭^{d(m)} φ. Negation swaps the satisfaction mode via the dual operation.
Note: TCSFormula.neg is NOT an involution (¬¬φ ≠ φ syntactically),
so the abstract SatDuality structure from Consequence.lean
does not apply. Instead we prove the key property directly.
st is self-dual: d(t) = s and d(s) = t. Self-dual consequence relations satisfy the deduction theorem (Lemma 10 of @cite{cobreros-etal-2012}).
cc is self-dual: d(c) = c.
Construct a three-valued interpretation from a T-model. Each atom (P, a) gets:
Truth3.trueif strictly P(a) (all similar individuals satisfy P)Truth3.falseif not tolerantly P(a) (no similar individual satisfies P)Truth3.indetotherwise (borderline: some similar individuals do, others don't)
This is the construction in Lemma 4 of @cite{cobreros-etal-2012}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Three-valued evaluation of TCS formulas using Strong Kleene connectives, parameterized by a three-valued atom valuation.
Equations
- Semantics.Supervaluation.TCS.mvEvalTCS v (Semantics.Supervaluation.TCS.TCSFormula.atom P a) = v P a
- Semantics.Supervaluation.TCS.mvEvalTCS v φ.neg = (Semantics.Supervaluation.TCS.mvEvalTCS v φ).neg
- Semantics.Supervaluation.TCS.mvEvalTCS v (φ.conj ψ) = (Semantics.Supervaluation.TCS.mvEvalTCS v φ).meet (Semantics.Supervaluation.TCS.mvEvalTCS v ψ)
Instances For
The three-valued interpretation correctly classifies atoms:
toMV produces Truth3.true exactly when strict, Truth3.false
exactly when not tolerant, and Truth3.indet for borderline.
Correspondence at the formula level (Theorem 3).
For any T-model M and formula φ:
This establishes that t-satisfaction = LP-satisfaction and
s-satisfaction = K3-satisfaction via the toMV translation.
Theorem 3, t-direction: tolerant satisfaction = LP-satisfaction.
Theorem 3, s-direction: strict satisfaction = K3-satisfaction.
The sorites paradox is resolved by st-consequence:
**Version 1**: Pa₁, a₁Iₚa₂, a₂Iₚa₃, ..., aₙ₋₁Iₚaₙ ⊨ˢᵗ Paₙ
This is st-INVALID. The premises require strict truth (all
similar individuals satisfy P), but in the sorites model,
the first premise Pa₁ is strictly true while the similarity
premises create a chain. The conclusion Paₙ fails tolerantly.
Each individual step IS st-valid: Pa, aIₚb ⊨ˢᵗ Pb.
But st-consequence is non-transitive, so chaining fails.
We demonstrate this on the concrete 4-element model from § 11.
Tolerance steps in the sorites model: each adjacent pair has the tolerant-conclusion step valid (the similar individual is tolerantly P), but the strict-premise step only works for a.
a: strictly tall, b: tolerantly tall (but not strictly), c: tolerantly tall (but not classically), d: not tolerantly tall.
Non-transitivity of st-consequence. Even though each step
a→b and b→c holds individually in soritesModel, the chain
a→d fails: d is NOT tolerantly tall.
In the 4-element sorites model:
- a is strictly tall, b is tolerantly tall (step a→b valid)
- b is classically tall, c is tolerantly tall (step b→c valid)
- But d is NOT tolerantly tall (chain breaks)
This demonstrates that st-consequence is non-transitive (Footnote 14 of @cite{cobreros-etal-2012}).
The sorites argument a₁ → a₂ → a₃ → a₄ is st-invalid: we cannot derive tolerant Pa₄ from strict Pa₁ plus the full similarity chain, because the chain exceeds the two-step tolerance limit.
The nine consequence relations on the restricted vocabulary (propositional formulas — no identity or similarity predicates) collapse to six distinct relations, ordered by strength:
```
cc = sc = ct = st (classical)
/ \
ss tt
\ /
cs tc
\ /
ts (empty)
```
- **cc = st**: classical consequence (four collapse)
- **ss**: K3-consequence (strict-to-strict)
- **tt**: LP-consequence (tolerant-to-tolerant)
- **cs**: strictly weaker than ss
- **tc**: strictly weaker than tt
- **ts**: the empty relation (Lemma 9: nothing follows)
Key properties of st (the recommended relation):
- Validates tolerance (the principle ∀xy(Px ∧ xIᵨy → Py))
- Satisfies the deduction theorem
- Has modus ponens
- Is non-transitive (blocks sorites chaining)