Cobreros, Egré, Ripley & van Rooij 2012: 4-Element Sorites Model #
The paper's worked 4-element example (described in the body text on
p. 354, immediately above footnote 4), formalized against the substrate
types in Semantics/Supervaluation/TCS.lean.
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:
bandcare tolerantly tall AND tolerantly not-tallTwo-step tolerance limit:
dis NOT tolerantly tall (three steps fromaexceeds Fact 3)Sorites resolution: each one-step inference
Pa, aIb ⊨ˢᵗ Pbis valid; each two-stepPa, aIb, bIc ⊨ˢᵗ Pcis valid; but the three-stepPa, aIb, bIc, cId ⊨ˢᵗ Pdis invalid.Attribution: paper §3.4.1 (p. 372) demonstrates non-transitivity for
⊨ᶜᵗ(the chainPa_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; thest-instantiation here applies that pattern to the relation the paper ultimately advocates (paper p. 373).
Cross-framework note #
tcs_supervaluation_disagree_concrete instantiates the Theory-file
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. Per the "no bridge files" + "worked examples live in Studies, not
theory files" discipline, the worked example was extracted here from a
previous embedding inside Semantics/Supervaluation/TCS.lean.
Equations
- CobrerosEtAl2012.instReprElt = { reprPrec := CobrerosEtAl2012.instReprElt.repr }
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✝
Instances For
Equations
- CobrerosEtAl2012.instDecidableEqElt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- CobrerosEtAl2012.instReprVPred = { reprPrec := CobrerosEtAl2012.instReprVPred.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CobrerosEtAl2012.instDecidableEqVPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- CobrerosEtAl2012.instFintypeVPred = { elems := {CobrerosEtAl2012.VPred.tall}, complete := CobrerosEtAl2012.instFintypeVPred._proof_1 }
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
Instances For
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)
Instances For
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
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
TolerantAt is decidable on the sorites model: it's a finite
existential.
Equations
- CobrerosEtAl2012.soritesModel_tolerant_dec P x = Fintype.decidableExistsFintype
Strict extension of tall: {a} only. Other elements have
similar individuals that aren't classically tall.
Classical extension of tall: {a, b} directly from I(tall).
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).
b is borderline-tall: tolerantly tall (witness: a), but not
strictly tall (counter-witness: c, which is similar to b but
not classically tall).
c is borderline-tall: tolerantly tall (witness: b), but not
strictly tall (counter-witness: d).
a is NOT borderline: strictly tall, hence not in tolerant \ strict.
d is NOT borderline: not even tolerantly tall, hence not in tolerant \ strict.
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.
Same for c.
At the non-borderline individual a (strictly tall), the
contradiction tall ∧ ¬ tall is NOT tolerantly true.
Dually for d (not even tolerantly tall).
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 (=
Truth3.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.
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.
Two-step st-validity: tall(a), aIb, bIc ⊨ˢᵗ tall(c).
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).
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.
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.
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 borderlinea. This is a categorical framework prediction — independent of any parameter. - Product-rule half: any product
q · (1 - q)forq ∈ [0, 1]is bounded above by1/4(AM-GM). This is the framework-level ceiling on any literal-meaning rule that multiplies a probability by its complement. L&G'slg_literal_borderline_boundedis thePMF-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.
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/Gradability/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.
Single-premise sorites unsoundness (the previous formalization's
sorites_chain_invalid). Subsumed by st_three_step_invalid above
but kept under the historical name.