[RK24]: Metalinguistic Gradability

Semantic expressivism for metalinguistic comparatives ("Ann is more a linguist than a philosopher"), equatives, degree modifiers, and conditionals [RK24], with the revised semantics and degree-theoretic formulation of its supplement [Koc24]. Speakers express interpretive as well as factual commitments: truth is evaluated at ⟨≤, i, w⟩ where ≤ is a total preorder over interpretations, and A ≻ B holds iff some (A∧¬B)-interpretation ranked ≤ i dominates every (B∧¬A)-interpretation.

The formalization is model-theoretic throughout: an interpretation — the paper's "function from expressions to intensions" — is a world-indexed family of first-order structures, and the language with its basic semantics IS the substrate's comparative-possibility logic (Core/Logic/FirstOrder/Comparative): L.CompFormula E evaluated by CompFormula.Realize, with ≻ the strict l-lifting. This file adds only what is RK-specific: acceptance and the common ground, degree modifiers and the conditional, the revised semantics, the delineation bridge, and the degree theory.

Main definitions

• SemanticOrdering, Eval, EvalRevised — the substrate's CompFormula language with the paper's basic (§4.2) and revised (supplement §B) semantics.
• AssertoricContent, MetalinguisticCG — acceptance and the common ground: the substrate's ContextSet at the ordering-world index, with assertion as ContextSet.update and the Stalnaker laws inherited.
• DistanceFunction, EvalVery, EvalSorta, EvalMostly, EvalMCond — degree modifiers (§6.1) and metalinguistic conditionals (§6.3).
• degreeEquiv, strictlyBetter, MetaDegree — the supplement's §C degree theory: metalinguistic degrees as a Quotient carrying LinearOrder and BoundedOrder instances.

Main results

• evalMuchMore_iff_strict_dominationLift, evalMostly_iff_strict_dominationLift — ≫ and mostly are strict l-liftings ([HI13]), extending the substrate's grounding of ≻; the distance-function axioms are exactly totality of "not far below".
• evalMCond_iff_entails — for an MC-free consequent the conditional is Stalnakerian ContextSet.entails of the consequent by the antecedent-cone.
• eval_mc_iff_delineation_of_noReversal — under No Reversal (§7) the MC is [Kle80]'s Delineation.comparativeSem.
• mc_iff_degree_gt, me_iff_same_degree — Facts 9–10: ≻ and ≈ are degree order and degree equality.
• mc_iff_comparativeSem — the paper's degree-theoretic claim, in substrate vocabulary: the revised MC is Degree.comparativeSem over the metalinguistic measure formulaDeg.
• Four finite models witness the §4.4 entailment patterns, nonclassical acceptance-preservation ([Yal07]), and the supplement's ME-transitivity counterexample and its revised-semantics repair.

Interpretations and semantic orderings

@[reducible, inline]

abbrev RudolphKocurek2024.SemanticOrdering (I : Type u_1) : Type u_1

The paper's ranking of interpretations by strength of interpretive commitment (§4.2).

Equations

• RudolphKocurek2024.SemanticOrdering I = Core.Order.TotalPreorder I

Semantics (§4.2 of the paper)

@[reducible, inline]

abbrev RudolphKocurek2024.Eval {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ : L.CompFormula E) (ord : SemanticOrdering I) (i : I) (w : W) : Prop

Truth at an index ⟨≤, i, w⟩: CompFormula.Realize at the ordering's le.

Equations

• RudolphKocurek2024.Eval interp φ ord i w = FirstOrder.Language.CompFormula.Realize interp φ ord.le i w

Assertoric Content

def RudolphKocurek2024.AssertoricContent {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) [Fintype I] (φ : L.CompFormula E) (ord : SemanticOrdering I) (w : W) : Prop

Assertoric content (§3.3): truth at all ≤-maximal interpretations — TotalPreorder.AcceptedAt. Acceptance-preservation is nonclassical (mc_disj_not_accepted).

Equations

• RudolphKocurek2024.AssertoricContent interp φ ord w = Core.Order.TotalPreorder.AcceptedAt ord fun (i : I) => RudolphKocurek2024.Eval interp φ ord i w

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableAssertoricContentOfFintypeOfDecidableEqOfDecidableAtomsOfDecidableRelLe {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) [Fintype I] [Fintype E] [DecidableEq E] [FirstOrder.Language.DecidableAtoms interp] (φ : L.CompFormula E) (ord : SemanticOrdering I) [DecidableRel ord.le] (w : W) : Decidable (AssertoricContent interp φ ord w)

Equations

• RudolphKocurek2024.instDecidableAssertoricContentOfFintypeOfDecidableEqOfDecidableAtomsOfDecidableRelLe interp φ ord w = id inferInstance

Distance Functions and Degree Modifiers (§6.1)

structure RudolphKocurek2024.DistanceFunction (I : Type u_4) (ord : SemanticOrdering I) : Type u_4

A distance function (§6.1): which interpretations count as reasonably close to each — the parameter behind very, sorta, mostly.

• close : I → I → Prop

  close i i' means i' is reasonably close to i.

• centered (i : I) : self.close i i

  Centered: i ∈ d(i)

• topBounded (i i' : I) : self.close i i' → ord.le i' i

  Top-bounded: if i' ∈ d(i), then i' ≤ i

• convex (i i' i'' : I) : self.close i i' → ord.le i' i'' → ord.le i'' i → self.close i i''

  Convex: if i' ∈ d(i) and i' ≤ i'' ≤ i, then i'' ∈ d(i)

• noncontractive (i i' j : I) : self.close i i' → ord.le i' j → ord.le j i → self.close j i'

  Noncontractive: if i' ∈ d(i) and i' ≤ j ≤ i, then i' ∈ d(j)

def RudolphKocurek2024.FarBelow {I : Type u_4} (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i j : I) : Prop

i ≪ j: i is below j and not even reasonably close to it.

Equations

• RudolphKocurek2024.FarBelow ord d i j = (ord.le i j ∧ ¬d.close j i)

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableRelFarBelowOfLeOfClose {I : Type u_4} (ord : SemanticOrdering I) (d : DistanceFunction I ord) [DecidableRel ord.le] [DecidableRel d.close] : DecidableRel (FarBelow ord d)

Equations

• RudolphKocurek2024.instDecidableRelFarBelowOfLeOfClose ord d x✝¹ x✝ = RudolphKocurek2024.instDecidableRelFarBelowOfLeOfClose._aux_1 ord d x✝¹ x✝

theorem RudolphKocurek2024.FarBelow.asymm {I : Type u_4} {ord : SemanticOrdering I} (d : DistanceFunction I ord) {a b : I} (h : FarBelow ord d a b) : ¬FarBelow ord d b a

≪ is asymmetric: centeredness plus noncontractivity force mutually-≤ points to be close.

theorem RudolphKocurek2024.not_farBelow_total {I : Type u_4} {ord : SemanticOrdering I} (d : DistanceFunction I ord) (a b : I) : ¬FarBelow ord d a b ∨ ¬FarBelow ord d b a

"Not far below" is total — what lets the strict l-lifting characterize ≫.

@[reducible, inline]

abbrev RudolphKocurek2024.EvalCompWith {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ ψ : L.CompFormula E) (ord : SemanticOrdering I) (below : I → I → Prop) (i : I) (w : W) : Prop

The paper's comparative template — the substrate's coneStrictLift at the formulas' truth sets: ≻'s clause with an arbitrary dominance relation in place of < (eval_comp_iff_compWith); ≫ is the instance at ≪.

Equations

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

theorem RudolphKocurek2024.eval_comp_iff_compWith {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ ψ : L.CompFormula E) (ord : SemanticOrdering I) (i : I) (w : W) : Eval interp (φ.comp ψ) ord i w ↔ EvalCompWith interp φ ψ ord (Core.Order.TotalPreorder.lt ord) i w

≻ is the template at <.

@[reducible, inline]

abbrev RudolphKocurek2024.EvalMuchMore {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ ψ : L.CompFormula E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Prop

Much more (A ≫ B): the template at ≪.

Equations

• RudolphKocurek2024.EvalMuchMore interp φ ψ ord d i w = RudolphKocurek2024.EvalCompWith interp φ ψ ord (RudolphKocurek2024.FarBelow ord d) i w

@[reducible, inline]

abbrev RudolphKocurek2024.EvalVery {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ : L.CompFormula E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Prop

very A := A ≫ ¬A — every reasonably close interpretation makes A true.

Equations

• RudolphKocurek2024.EvalVery interp φ ord d i w = RudolphKocurek2024.EvalMuchMore interp φ φ.not ord d i w

@[reducible, inline]

abbrev RudolphKocurek2024.EvalSorta {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ : L.CompFormula E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Prop

sorta A := ¬ very ¬A — some reasonably close interpretation makes A true.

Equations

• RudolphKocurek2024.EvalSorta interp φ ord d i w = ¬RudolphKocurek2024.EvalVery interp φ.not ord d i w

def RudolphKocurek2024.EvalMostly {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ : L.CompFormula E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Prop

mostly A (eq. 97 of [RK24]): some reasonably high level strictly below the top makes A uniformly true, and every A-false level below the current interpretation sits below it. Compatible with A and with ¬A (unlike very); entails sorta A; mostly A ∧ mostly ¬A is contradictory.

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEvalMostlyOfFintypeOfDecidableEqOfDecidableAtomsOfLeOfDecidableRelClose {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) [Fintype I] (φ : L.CompFormula E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) [Fintype E] [DecidableEq E] [FirstOrder.Language.DecidableAtoms interp] [DecidableRel ord.le] [DecidableRel d.close] : Decidable (EvalMostly interp φ ord d i w)

Equations

• RudolphKocurek2024.instDecidableEvalMostlyOfFintypeOfDecidableEqOfDecidableAtomsOfLeOfDecidableRelClose interp φ ord d i w = id inferInstance

theorem RudolphKocurek2024.evalMuchMore_iff_strict_dominationLift {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ ψ : L.CompFormula E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : EvalMuchMore interp φ ψ ord d i w ↔ ComparativeProbability.Strict (ComparativeProbability.dominationLift fun (a b : I) => ¬FarBelow ord d a b) {x : I | ord.le x i ∧ Eval interp φ ord x w ∧ ¬Eval interp ψ ord x w} {x : I | ord.le x i ∧ Eval interp ψ ord x w ∧ ¬Eval interp φ ord x w}

Grounding: ≫ is the strict l-lifting under the coarser total preorder "not far below" — the distance-function axioms are exactly what make that relation total, so [HI13]'s lift machinery applies with ≪ in the role of <.

theorem RudolphKocurek2024.evalMostly_iff_strict_dominationLift {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ : L.CompFormula E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : EvalMostly interp φ ord d i w ↔ ComparativeProbability.Strict (ComparativeProbability.dominationLift fun (a b : I) => ord.le b a) {x : I | Core.Order.TotalPreorder.lt ord x i ∧ d.close i x ∧ ∀ (j : I), Core.Order.TotalPreorder.equiv ord j x → Eval interp φ ord j w} {x : I | Core.Order.TotalPreorder.lt ord x i ∧ ∀ (j : I), Core.Order.TotalPreorder.equiv ord j x → ¬Eval interp φ ord j w}

Grounding: mostly is the strict l-lifting comparing φ-uniform levels (ord.equiv-classes, mathlib's AntisymmRel.setoid): some reasonably-high all-φ level strictly below the index dominates every all-¬φ level below it.

No Reversal and the delineation bridge ([Kle80], §7)

def RudolphKocurek2024.NoReversal {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (R : L.Relations 1) (w : W) (a b : E) : Prop

No Reversal (van Benthem 1990; §7 of [RK24]): below any interpretation separating a from b, every extension admitting b admits a — the order-restricted analogue of Klein's monotone delineation.

Equations

• RudolphKocurek2024.NoReversal interp ord R w a b = ∀ (i i' : I), ord.le i' i → a ∈ (interp i w).ext₁ R → b ∉ (interp i w).ext₁ R → b ∈ (interp i' w).ext₁ R → a ∈ (interp i' w).ext₁ R

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableNoReversalOfFintypeOfDecidableAtomsOfDecidableRelLe {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) [Fintype I] [FirstOrder.Language.DecidableAtoms interp] (ord : SemanticOrdering I) [DecidableRel ord.le] (R : L.Relations 1) (w : W) (a b : E) : Decidable (NoReversal interp ord R w a b)

Equations

• RudolphKocurek2024.instDecidableNoReversalOfFintypeOfDecidableAtomsOfDecidableRelLe interp ord R w a b = id (⋯.mpr inferInstance)

def RudolphKocurek2024.interpretationDelineation {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (R : L.Relations 1) (w : W) (i : I) : Semantics.Gradability.Delineation.ComparisonClass E → E → Prop

The delineation induced by a ranked interpretation family: admissible comparison classes are the extensions of R in the ≤-cone; x is R-in-C iff x ∈ C. Instantiates [Kle80]'s comparison-class parameter.

Equations

• RudolphKocurek2024.interpretationDelineation interp ord R w i C x = ((∃ (i' : I), ord.le i' i ∧ C = (interp i' w).ext₁ R) ∧ x ∈ C)

theorem RudolphKocurek2024.delineation_comparativeSem_iff {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (R : L.Relations 1) (w : W) (i : I) (a b : E) : Semantics.Gradability.Delineation.comparativeSem (interpretationDelineation interp ord R w i) a b ↔ ∃ (i' : I), ord.le i' i ∧ a ∈ (interp i' w).ext₁ R ∧ b ∉ (interp i' w).ext₁ R

The delineation comparative over the induced delineation is the ∃-witness clause of the MC: some cone extension separates a from b.

theorem RudolphKocurek2024.eval_mc_iff_delineation_of_noReversal {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (R : L.Relations 1) (w : W) (i : I) (a b : E) (hnr : NoReversal interp ord R w b a) : Eval interp ((FirstOrder.Language.CompFormula.matom R a).comp (FirstOrder.Language.CompFormula.matom R b)) ord i w ↔ Semantics.Gradability.Delineation.comparativeSem (interpretationDelineation interp ord R w i) a b

The §7 bridge, in the substrate's vocabulary: under No Reversal, the metalinguistic comparative for a gradable predicate IS [Kle80]'s delineation comparative (Delineation.comparativeSem) over the interpretation-induced delineation — the paper's eq. (128): NR makes the domination clause of the MC semantics redundant.

Revised Semantics ([Koc24] §B)

def RudolphKocurek2024.EvalRevised {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ : L.CompFormula E) (ord : SemanticOrdering I) (i : I) (w : W) : Prop

Truth under the revised MC semantics ([Koc24] §B). The basic semantics fails ME transitivity; the revision strengthens the MC: the (A∧¬B)-witness must dominate either all B-interpretations or all ¬A-interpretations, blocking vacuous comparatives.

Properties ([Koc24] §B): all basic entailment patterns (Fact 3 a–n) are preserved (Fact 5); ME transitivity is validated (Fact 6); interdefinable with the basic semantics (Fact 7).

Equations

• One or more equations did not get rendered due to their size.
• RudolphKocurek2024.EvalRevised interp (FirstOrder.Language.CompFormula.ofFormula ψ) ord i w = ψ.Realize id
• RudolphKocurek2024.EvalRevised interp A.not ord i w = ¬RudolphKocurek2024.EvalRevised interp A ord i w
• RudolphKocurek2024.EvalRevised interp (A.inf B) ord i w = (RudolphKocurek2024.EvalRevised interp A ord i w ∧ RudolphKocurek2024.EvalRevised interp B ord i w)
• RudolphKocurek2024.EvalRevised interp (A.sup B) ord i w = (RudolphKocurek2024.EvalRevised interp A ord i w ∨ RudolphKocurek2024.EvalRevised interp B ord i w)

@[implicit_reducible]

instance RudolphKocurek2024.EvalRevised.instDec {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) [Fintype I] [Fintype E] [DecidableEq E] [hA : FirstOrder.Language.DecidableAtoms interp] (φ : L.CompFormula E) (ord : SemanticOrdering I) [DecidableRel ord.le] (i : I) (w : W) : Decidable (EvalRevised interp φ ord i w)

Equations

• One or more equations did not get rendered due to their size.
• RudolphKocurek2024.EvalRevised.instDec interp (FirstOrder.Language.CompFormula.ofFormula ψ) ord i w = ψ.decRealize id
• RudolphKocurek2024.EvalRevised.instDec interp A.not ord i w = RudolphKocurek2024.EvalRevised.instDec._aux_1 interp ord i w A (RudolphKocurek2024.EvalRevised.instDec interp A ord i w)

theorem RudolphKocurek2024.evalRevised_mc_iff {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A B : L.CompFormula E) (ord : SemanticOrdering I) (i : I) (w : W) : EvalRevised interp (A.comp B) ord i w ↔ ∃ (i' : I), ord.le i' i ∧ EvalRevised interp A ord i' w ∧ ¬EvalRevised interp B ord i' w ∧ ((∀ (i'' : I), ord.le i'' i → EvalRevised interp B ord i'' w → Core.Order.TotalPreorder.lt ord i'' i') ∨ ∀ (i'' : I), ord.le i'' i → ¬EvalRevised interp A ord i'' w → Core.Order.TotalPreorder.lt ord i'' i')

Characterization of the revised MC case — definitional.

Metalinguistic Conditional (§6.3)

def RudolphKocurek2024.restrictLE {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A : L.CompFormula E) (le : I → I → Prop) (w : W) : I → I → Prop

Restrict an ordering relation to A-interpretations (§6.3): drops non-A interpretations, so the result satisfies reflexivity (at A-interpretations) and transitivity but not totality — hence the consequent of a conditional is evaluated via EvalGen rather than Eval.

Equations

• RudolphKocurek2024.restrictLE interp A le w i j = (le i j ∧ FirstOrder.Language.CompFormula.Realize interp A le i w ∧ FirstOrder.Language.CompFormula.Realize interp A le j w)

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableRelRestrictLEOfFintypeOfDecidableEqOfDecidableAtoms {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) [Fintype I] (A : L.CompFormula E) [Fintype E] [DecidableEq E] [FirstOrder.Language.DecidableAtoms interp] (le : I → I → Prop) [DecidableRel le] (w : W) : DecidableRel (restrictLE interp A le w)

Equations

• RudolphKocurek2024.instDecidableRelRestrictLEOfFintypeOfDecidableEqOfDecidableAtoms interp A le w x✝¹ x✝ = id inferInstance

def RudolphKocurek2024.EvalMCond {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A B : L.CompFormula E) (ord : SemanticOrdering I) (i : I) (w : W) : Prop

Metalinguistic conditional (eq. 120 of [RK24]): the antecedent is evaluated with the full ordering, the consequent with the A-restricted ordering ≤_A. For non-metagradable A and B this reduces to interpretation-strict implication.

Key properties: C1 (conditionals entail weak comparatives), M1 (⊨ A → (A ≻ ¬A), see mcond_m1), failure of modus tollens for acceptance.

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEvalMCondOfFintypeOfDecidableEqOfDecidableAtomsOfDecidableRelLe {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) [Fintype I] (A B : L.CompFormula E) (ord : SemanticOrdering I) (i : I) (w : W) [Fintype E] [DecidableEq E] [FirstOrder.Language.DecidableAtoms interp] [DecidableRel ord.le] : Decidable (EvalMCond interp A B ord i w)

Equations

• RudolphKocurek2024.instDecidableEvalMCondOfFintypeOfDecidableEqOfDecidableAtomsOfDecidableRelLe interp A B ord i w = id inferInstance

theorem RudolphKocurek2024.evalMCond_iff_entails {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A B : L.CompFormula E) (ord : SemanticOrdering I) (i : I) (w : W) (hB : B.CompFree) : EvalMCond interp A B ord i w ↔ CommonGround.ContextSet.entails {x : I | ord.le x i ∧ FirstOrder.Language.CompFormula.Realize interp A ord.le x w} {x : I | FirstOrder.Language.CompFormula.Realize interp B ord.le x w}

Grounding in the common-ground substrate: for an MC-free consequent — strictly weaker than the paper's reduction, which also assumes the antecedent MC-free — the metalinguistic conditional is Stalnakerian entailment (ContextSet.entails) of the consequent by the ranked antecedent-cone. The antecedent may contain ≻ freely: it is always evaluated at the full ordering, and an MC-free consequent never consults the restricted one.

Connection to Common Ground

structure RudolphKocurek2024.OrderingWorldPair (I : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

An ordering-world pair: the enriched index for the metalinguistic common ground — a Stalnakerian world that fixes interpretive as well as factual commitments.

• ord : SemanticOrdering I
• world : W

@[reducible, inline]

abbrev RudolphKocurek2024.MetalinguisticCG (I : Type u_1) (W : Type u_2) : Type (max u_2 u_1)

The metalinguistic common ground IS the substrate's ContextSet, taken at the enriched index type: the Stalnaker generalization is "same object, richer worlds", so ContextSet.update and its laws apply unchanged.

Equations

• RudolphKocurek2024.MetalinguisticCG I W = CommonGround.ContextSet (RudolphKocurek2024.OrderingWorldPair I W)

def RudolphKocurek2024.MetalinguisticCG.toContextSet {I : Type u_1} {W : Type u_2} (cg : MetalinguisticCG I W) : CommonGround.ContextSet W

Project to a classical context set: forget the ordering coordinate (Set.image of the world projection). A world survives iff some ordering paired with it does.

Equations

• cg.toContextSet = RudolphKocurek2024.OrderingWorldPair.world '' cg

def RudolphKocurek2024.MetalinguisticCG.assertoricProp {I : Type u_1} {W : Type u_2} {L : FirstOrder.Language} {E : Type u_3} [Fintype I] (interp : I → W → L.Structure E) (φ : L.CompFormula E) : Set (OrderingWorldPair I W)

The proposition a formula expresses over the enriched index: the ordering-world pairs at which its assertoric content holds.

Equations

• RudolphKocurek2024.MetalinguisticCG.assertoricProp interp φ = {pair : RudolphKocurek2024.OrderingWorldPair I W | RudolphKocurek2024.AssertoricContent interp φ pair.ord pair.world}

def RudolphKocurek2024.MetalinguisticCG.updateAssertoric {I : Type u_1} {W : Type u_2} {L : FirstOrder.Language} {E : Type u_3} [Fintype I] (interp : I → W → L.Structure E) (cg : MetalinguisticCG I W) (φ : L.CompFormula E) : MetalinguisticCG I W

Assertion is the substrate's ContextSet.update with the assertoric proposition — not a new operation.

Equations

• RudolphKocurek2024.MetalinguisticCG.updateAssertoric interp cg φ = CommonGround.ContextSet.update cg (RudolphKocurek2024.MetalinguisticCG.assertoricProp interp φ)

theorem RudolphKocurek2024.MetalinguisticCG.updateAssertoric_restricts {I : Type u_1} {W : Type u_2} {L : FirstOrder.Language} {E : Type u_3} [Fintype I] (interp : I → W → L.Structure E) (cg : MetalinguisticCG I W) (φ : L.CompFormula E) : updateAssertoric interp cg φ ⊆ cg

Stalnaker's law at the enriched type: assertion restricts the common ground (inherited from ContextSet.update_restricts).

theorem RudolphKocurek2024.MetalinguisticCG.updateAssertoric_comm {I : Type u_1} {W : Type u_2} {L : FirstOrder.Language} {E : Type u_3} [Fintype I] (interp : I → W → L.Structure E) (cg : MetalinguisticCG I W) (φ ψ : L.CompFormula E) : updateAssertoric interp (updateAssertoric interp cg φ) ψ = updateAssertoric interp (updateAssertoric interp cg ψ) φ

Assertion order is irrelevant (inherited from ContextSet.update_comm).

theorem RudolphKocurek2024.MetalinguisticCG.updateAssertoric_idem {I : Type u_1} {W : Type u_2} {L : FirstOrder.Language} {E : Type u_3} [Fintype I] (interp : I → W → L.Structure E) (cg : MetalinguisticCG I W) (φ : L.CompFormula E) : updateAssertoric interp (updateAssertoric interp cg φ) φ = updateAssertoric interp cg φ

Reassertion is idempotent (inherited from ContextSet.update_idem).

theorem RudolphKocurek2024.MetalinguisticCG.toContextSet_updateAssertoric_subset {I : Type u_1} {W : Type u_2} {L : FirstOrder.Language} {E : Type u_3} [Fintype I] (interp : I → W → L.Structure E) (cg : MetalinguisticCG I W) (φ : L.CompFormula E) : (updateAssertoric interp cg φ).toContextSet ⊆ cg.toContextSet

The projection is monotone, so assertion restricts the projected classical context set too: the enriched update is Stalnaker-conservative. (That the update does NOT factor through the projection — interpretive commitments do real work — is the paper's expressivist thesis.)

@[implicit_reducible]

instance RudolphKocurek2024.instHasContextSetMetalinguisticCG {I : Type u_1} {W : Type u_2} : CommonGround.HasContextSet (MetalinguisticCG I W) W

MetalinguisticCG projects to a ContextSet via HasContextSet.

Equations

• RudolphKocurek2024.instHasContextSetMetalinguisticCG = { toContextSet := RudolphKocurek2024.MetalinguisticCG.toContextSet }

Field and Denotation Sets

noncomputable def RudolphKocurek2024.field {I : Type u_1} [Fintype I] (ord : SemanticOrdering I) (i : I) : Finset I

The field I_i: the set of interpretations ranked at or below i. Classical: the degree theory proves structure, it never computes.

Equations

• RudolphKocurek2024.field ord i = {j : I | ord.le j i}

noncomputable def RudolphKocurek2024.denotation {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} [Fintype I] (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (i : I) (φ : L.CompFormula E) (w : W) : Finset I

The denotation of a formula: the set of interpretations in I_i where the formula is true (under the revised semantics).

Equations

• RudolphKocurek2024.denotation interp ord i φ w = {j ∈ RudolphKocurek2024.field ord i | RudolphKocurek2024.EvalRevised interp φ ord j w}

theorem RudolphKocurek2024.denotation_subset_field {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} [Fintype I] (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (i : I) (φ : L.CompFormula E) (w : W) : denotation interp ord i φ w ⊆ field ord i

The ∼ Equivalence Relation ([Koc24] §C, p. 9)

def RudolphKocurek2024.equivCond1 {I : Type u_1} [DecidableEq I] (ord : SemanticOrdering I) (X Y : Finset I) : Prop

∼ condition (i): each element of X \ Y is matched by one of Y \ X at least as high, and vice versa.

Equations

• RudolphKocurek2024.equivCond1 ord X Y = ((∀ i' ∈ X \ Y, ∃ i'' ∈ Y \ X, ord.le i' i'') ∧ ∀ i' ∈ Y \ X, ∃ i'' ∈ X \ Y, ord.le i' i'')

def RudolphKocurek2024.equivCond2 {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y : Finset I) : Prop

∼ condition (ii): each element of the symmetric difference is dominated both by an element of X ∩ Y and by one of the field outside X ∪ Y.

Equations

• RudolphKocurek2024.equivCond2 ord i X Y = ∀ i' ∈ (X ∪ Y) \ (X ∩ Y), (∃ i'' ∈ X ∩ Y, ord.le i' i'') ∧ ∃ i'' ∈ RudolphKocurek2024.field ord i \ (X ∪ Y), ord.le i' i''

def RudolphKocurek2024.degreeEquiv {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y : Finset I) : Prop

Metalinguistic degree equivalence X ∼_i Y: the revised ME truth conditions applied to interpretation sets.

Equations

• RudolphKocurek2024.degreeEquiv ord i X Y = (RudolphKocurek2024.equivCond1 ord X Y ∨ RudolphKocurek2024.equivCond2 ord i X Y)

Fact 8: ∼ is an Equivalence Relation

theorem RudolphKocurek2024.degreeEquiv_refl {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) : degreeEquiv ord i X X

Fact 8a: ∼ is reflexive.

theorem RudolphKocurek2024.degreeEquiv_symm {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y : Finset I) : degreeEquiv ord i X Y → degreeEquiv ord i Y X

Fact 8b: ∼ is symmetric.

The ⊐ Ordering on Sets ([Koc24] §C, p. 10)

def RudolphKocurek2024.strictlyBetter {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y : Finset I) : Prop

X ⊐ Y: some witness in X \ Y inside the field dominates all of Y \ X and, moreover, all of X ∩ Y or all of the field outside X ∪ Y — the revised MC truth conditions applied to interpretation sets.

Equations

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

Facts 11–12: ⊐ on Degrees

theorem RudolphKocurek2024.strictlyBetter_irrefl {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) : ¬strictlyBetter ord i X X

Fact 12a: ⊐ is irreflexive.

theorem RudolphKocurek2024.degreeEquiv_not_strictlyBetter {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y : Finset I) : degreeEquiv ord i X Y → ¬strictlyBetter ord i X Y

∼ refutes ⊐: equivalent sets are incomparable.

theorem RudolphKocurek2024.strictlyBetter_respects_right {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y Z : Finset I) (_hXf : X ⊆ field ord i) (hYf : Y ⊆ field ord i) (hZf : Z ⊆ field ord i) : strictlyBetter ord i X Y → degreeEquiv ord i Y Z → strictlyBetter ord i X Z

Fact 11: ⊐ respects ∼ on the right — X ⊐ Y and Y ∼ Z give X ⊐ Z.

theorem RudolphKocurek2024.strictlyBetter_respects_left {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y Z : Finset I) (hXf : X ⊆ field ord i) (_hYf : Y ⊆ field ord i) (hZf : Z ⊆ field ord i) : strictlyBetter ord i X Y → degreeEquiv ord i X Z → strictlyBetter ord i Z Y

Fact 11: ⊐ respects ∼ on the left — X ⊐ Y and X ∼ Z give Z ⊐ Y.

theorem RudolphKocurek2024.strictlyBetter_trans {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y Z : Finset I) : strictlyBetter ord i X Y → strictlyBetter ord i Y Z → strictlyBetter ord i X Z

Fact 12b: ⊐ is transitive.

theorem RudolphKocurek2024.strictlyBetter_total {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y : Finset I) (hX : X ⊆ field ord i) (hY : Y ⊆ field ord i) : degreeEquiv ord i X Y ∨ strictlyBetter ord i X Y ∨ strictlyBetter ord i Y X

Fact 12c: trichotomy — X ∼ Y, X ⊐ Y, or Y ⊐ X.

Fact 8c: ∼ Transitivity (via Totality + Respects)

theorem RudolphKocurek2024.degreeEquiv_trans {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y Z : Finset I) (hXf : X ⊆ field ord i) (hYf : Y ⊆ field ord i) (hZf : Z ⊆ field ord i) : degreeEquiv ord i X Y → degreeEquiv ord i Y Z → degreeEquiv ord i X Z

Fact 8c: ∼ is transitive on field-subsets, via trichotomy and Fact 11.

The degree normal form

An element is redundant when it has an X-mate weakly above it and a field-outsider weakly above it — equivCond2 made unary: dropping it leaves the degree unchanged. Iterated dropping yields a normal form; the degree of a set is the level multiset of its normal form (spike-verified: ⊐ is the descending lexicographic order on those multisets).

def RudolphKocurek2024.Redundant {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) (x : I) : Prop

x is redundant in X: an X-mate and a field-outsider both sit weakly above it.

Equations

• RudolphKocurek2024.Redundant ord i X x = ((∃ x' ∈ X.erase x, ord.le x x') ∧ ∃ z ∈ RudolphKocurek2024.field ord i \ X, ord.le x z)

theorem RudolphKocurek2024.degreeEquiv_erase_of_redundant {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) {X : Finset I} {x : I} (hx : x ∈ X) (h : Redundant ord i X x) : degreeEquiv ord i X (X.erase x)

Dropping a redundant element preserves the degree — equivCond2 with the redundancy witnesses.

@[irreducible]

def RudolphKocurek2024.normalize {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) : Finset I

The degree normal form: drop redundant elements until none remain.

Equations

• RudolphKocurek2024.normalize ord i X = if h : ∃ x ∈ X, RudolphKocurek2024.Redundant ord i X x then RudolphKocurek2024.normalize ord i (X.erase h.choose) else X

theorem RudolphKocurek2024.normalize_subset {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) : normalize ord i X ⊆ X

theorem RudolphKocurek2024.degreeEquiv_normalize {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) (hX : X ⊆ field ord i) : degreeEquiv ord i X (normalize ord i X)

Normalization preserves the degree.

theorem RudolphKocurek2024.not_redundant_normalize {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) (x : I) : x ∈ normalize ord i X → ¬Redundant ord i (normalize ord i X) x

Normal forms have no redundant elements.

noncomputable def RudolphKocurek2024.rank {I : Type u_1} [Fintype I] (ord : SemanticOrdering I) (x : I) : ℕ

The rank of an interpretation: how many interpretations sit strictly below it. Order-reflecting into ℕ (lt_iff_rank_lt, equiv_iff_rank_eq), so degree invariants can live in List ℕ under mathlib's lex order.

Equations

• RudolphKocurek2024.rank ord x = {x_1 : I | Core.Order.TotalPreorder.lt ord x_1 x}.card

theorem RudolphKocurek2024.lt_iff_rank_lt {I : Type u_1} [Fintype I] (ord : SemanticOrdering I) {x y : I} : Core.Order.TotalPreorder.lt ord x y ↔ rank ord x < rank ord y

theorem RudolphKocurek2024.equiv_iff_rank_eq {I : Type u_1} [Fintype I] (ord : SemanticOrdering I) {x y : I} : Core.Order.TotalPreorder.equiv ord x y ↔ rank ord x = rank ord y

noncomputable def RudolphKocurek2024.degList {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) : List ℕ

The degree list: ranks of the normal form, in descending order. ⊐ is the lexicographic order on degree lists (strictlyBetter_iff_degList_lex).

Equations

• RudolphKocurek2024.degList ord i X = (Multiset.map (RudolphKocurek2024.rank ord) (RudolphKocurek2024.normalize ord i X).val).sort fun (x1 x2 : ℕ) => x1 ≥ x2

theorem RudolphKocurek2024.normalize_idem {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) : normalize ord i (normalize ord i X) = normalize ord i X

Normalization is idempotent: normal forms are fixed points.

theorem RudolphKocurek2024.degList_normalize {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) : degList ord i (normalize ord i X) = degList ord i X

The degree list is invariant under normalization.

Normal-form structure

Rank multisets: invariance under ∼

noncomputable def RudolphKocurek2024.rankMS {I : Type u_1} [Fintype I] (ord : SemanticOrdering I) (X : Finset I) : Multiset ℕ

The rank multiset of a finset — its elements' ranks bagged. degList is this multiset sorted descending.

Equations

• RudolphKocurek2024.rankMS ord X = Multiset.map (RudolphKocurek2024.rank ord) X.val

Degree lists: ⊐ as descending lexicographic order

theorem RudolphKocurek2024.strictlyBetter_iff_degList_lex {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y : Finset I) (hX : X ⊆ field ord i) (hY : Y ⊆ field ord i) : strictlyBetter ord i X Y ↔ List.Lex (fun (x1 x2 : ℕ) => x1 < x2) (degList ord i Y) (degList ord i X)

Degree characterization (spike-verified oracle: scratch/colex_spike2.lean): ⊐ is the descending lexicographic order on degree lists.

Proof structure: forward direction reduces to normal forms and locates the top-rank divergence via the ⊐ witness; backward direction uses ⊐-trichotomy (strictlyBetter_total), asymmetry of List.Lex, and degList_eq_of_degreeEquiv to eliminate the other two cases.

theorem RudolphKocurek2024.degreeEquiv_iff_degList_eq {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X Y : Finset I) (hX : X ⊆ field ord i) (hY : Y ⊆ field ord i) : degreeEquiv ord i X Y ↔ degList ord i X = degList ord i Y

Degree equivalence is equality of degree lists. Follows from strictlyBetter_iff_degList_lex and List.Lex trichotomy on List ℕ (via ⊐-trichotomy: if X ⊐ Y or Y ⊐ X, lex holds, contradicting list equality).

def RudolphKocurek2024.metalinguisticSetoid {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) : Setoid { X : Finset I // X ⊆ field ord i }

∼ as a Setoid on field-subsets (transitivity needs the field bound).

Equations

• RudolphKocurek2024.metalinguisticSetoid ord i = { r := fun (X Y : { X : Finset I // X ⊆ RudolphKocurek2024.field ord i }) => RudolphKocurek2024.degreeEquiv ord i ↑X ↑Y, iseqv := ⋯ }

Metalinguistic Degree Type

def RudolphKocurek2024.MetaDegree (I : Type u_1) [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) : Type u_1

Metalinguistic degrees: ∼-classes of interpretation sets. The degree of a sentence is deg of its denotation (formulaDeg).

Equations

• RudolphKocurek2024.MetaDegree I ord i = Quotient (RudolphKocurek2024.metalinguisticSetoid ord i)

def RudolphKocurek2024.deg {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) (hX : X ⊆ field ord i) : MetaDegree I ord i

The metalinguistic degree of an interpretation set.

Equations

• RudolphKocurek2024.deg ord i X hX = ⟦⟨X, hX⟩⟧

Facts 9–10: Correspondence with Revised Semantics

noncomputable def RudolphKocurek2024.formulaDeg {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} [Fintype I] [DecidableEq I] (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (i : I) (φ : L.CompFormula E) (w : W) : MetaDegree I ord i

The metalinguistic degree of a formula's denotation.

Equations

• RudolphKocurek2024.formulaDeg interp ord i φ w = RudolphKocurek2024.deg ord i (RudolphKocurek2024.denotation interp ord i φ w) ⋯

theorem RudolphKocurek2024.mc_iff_degree_gt {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} [Fintype I] [DecidableEq I] (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (i : I) (A B : L.CompFormula E) (w : W) : EvalRevised interp (A.comp B) ord i w ↔ strictlyBetter ord i (denotation interp ord i A w) (denotation interp ord i B w)

Fact 10: revised MC holds iff denotation of A ⊐ denotation of B.

theorem RudolphKocurek2024.me_iff_same_degree {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} [Fintype I] [DecidableEq I] (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (i : I) (A B : L.CompFormula E) (w : W) : EvalRevised interp (A.equi B) ord i w ↔ degreeEquiv ord i (denotation interp ord i A w) (denotation interp ord i B w)

Fact 9: ME holds iff denotations have the same degree — the Boolean-free bridge from EvalRevised to the algebraic degree structure. Forward direction uses strictlyBetter_total.

The metalinguistic degree scale

Facts 11–13 make MetaDegree a bounded linear order — i.e., a scale in the degree substrate's sense. The instances below package that, and mc_iff_comparativeSem cashes it out: the revised MC is the degree substrate's binary comparative over the measure function formulaDeg.

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEquivCond1OfDecidableRelLe {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) [DecidableRel ord.le] (X Y : Finset I) : Decidable (equivCond1 ord X Y)

Equations

• RudolphKocurek2024.instDecidableEquivCond1OfDecidableRelLe ord X Y = id inferInstance

@[implicit_reducible]

noncomputable instance RudolphKocurek2024.instDecidableEquivCond2OfDecidableRelLe {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) [DecidableRel ord.le] (X Y : Finset I) : Decidable (equivCond2 ord i X Y)

Equations

• RudolphKocurek2024.instDecidableEquivCond2OfDecidableRelLe ord i X Y = id inferInstance

@[implicit_reducible]

noncomputable instance RudolphKocurek2024.instDecidableDegreeEquivOfDecidableRelLe {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) [DecidableRel ord.le] (X Y : Finset I) : Decidable (degreeEquiv ord i X Y)

Equations

• RudolphKocurek2024.instDecidableDegreeEquivOfDecidableRelLe ord i X Y = id inferInstance

@[implicit_reducible]

noncomputable instance RudolphKocurek2024.instDecidableStrictlyBetterOfDecidableRelLe {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) [DecidableRel ord.le] (X Y : Finset I) : Decidable (strictlyBetter ord i X Y)

Equations

• RudolphKocurek2024.instDecidableStrictlyBetterOfDecidableRelLe ord i X Y = id inferInstance

theorem RudolphKocurek2024.not_strictlyBetter_field {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) (hX : X ⊆ field ord i) : ¬strictlyBetter ord i X (field ord i)

Fact 13a: nothing is strictly better than the full field I_i (packaged as OrderTop below).

theorem RudolphKocurek2024.not_strictlyBetter_empty {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (X : Finset I) : ¬strictlyBetter ord i ∅ X

Fact 13b: the empty set is strictly better than nothing (packaged as OrderBot below).

theorem RudolphKocurek2024.strictlyBetter_congr {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) {X X' Y Y' : Finset I} (hXf : X ⊆ field ord i) (hX'f : X' ⊆ field ord i) (hYf : Y ⊆ field ord i) (hY'f : Y' ⊆ field ord i) (hX : degreeEquiv ord i X X') (hY : degreeEquiv ord i Y Y') : strictlyBetter ord i X Y ↔ strictlyBetter ord i X' Y'

Fact 11 packaged as a congruence: ⊐ is invariant under ∼ on both sides.

@[implicit_reducible]

noncomputable instance RudolphKocurek2024.instDecidableEqMetaDegreeOfDecidableRelLe {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) [DecidableRel ord.le] : DecidableEq (MetaDegree I ord i)

Equations

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

def RudolphKocurek2024.MetaDegree.le {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) (d₁ d₂ : MetaDegree I ord i) : Prop

The scale order: deg X ≤ deg Y iff X is not strictly better than Y (well-defined on ∼-classes by strictlyBetter_congr).

Equations

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

@[implicit_reducible]

noncomputable instance RudolphKocurek2024.instLinearOrderMetaDegree {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) : LinearOrder (MetaDegree I ord i)

MetaDegree is a linear order: Fact 12, packaged. Irreflexivity, transitivity, and totality of ⊐ become the order axioms on the quotient.

Equations

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

@[implicit_reducible]

noncomputable instance RudolphKocurek2024.instBoundedOrderMetaDegree {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) : BoundedOrder (MetaDegree I ord i)

Fact 13, packaged: the tautology's degree is ⊤, the contradiction's ⊥.

Equations

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

@[simp]

theorem RudolphKocurek2024.deg_le_deg_iff {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) {X Y : Finset I} (hX : X ⊆ field ord i) (hY : Y ⊆ field ord i) : deg ord i X hX ≤ deg ord i Y hY ↔ ¬strictlyBetter ord i X Y

theorem RudolphKocurek2024.deg_lt_deg_iff {I : Type u_1} [Fintype I] [DecidableEq I] (ord : SemanticOrdering I) (i : I) {X Y : Finset I} (hX : X ⊆ field ord i) (hY : Y ⊆ field ord i) : deg ord i Y hY < deg ord i X hX ↔ strictlyBetter ord i X Y

The strict order on metalinguistic degrees is exactly ⊐ (arguments flipped): Y's degree lies below X's iff X is strictly better.

theorem RudolphKocurek2024.mc_iff_comparativeSem {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} [Fintype I] [DecidableEq I] (interp : I → W → L.Structure E) (ord : SemanticOrdering I) (i : I) (A B : L.CompFormula E) (w : W) : EvalRevised interp (A.comp B) ord i w ↔ Degree.comparativeSem (fun (φ : L.CompFormula E) => formulaDeg interp ord i φ w) A B Core.Order.ScalePolarity.positive

The paper's (59), in the substrate's vocabulary: the revised metalinguistic comparative IS the degree substrate's binary comparative (Degree.comparativeSem, positive direction) over the metalinguistic measure function formulaDeg. Metagradability thereby instantiates the degree substrate's central object — a measure μ : E → D into a bounded linear scale — with E the formulas and D the MetaDegree scale.

Types (shared across models)

inductive RudolphKocurek2024.W : Type

One world.

• w0 : W

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqW : DecidableEq W

Equations

• RudolphKocurek2024.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RudolphKocurek2024.instReprW.repr : W → ℕ → Std.Format

Equations

• RudolphKocurek2024.instReprW.repr RudolphKocurek2024.W.w0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.W.w0")).group prec✝

@[implicit_reducible]

instance RudolphKocurek2024.instReprW : Repr W

Equations

• RudolphKocurek2024.instReprW = { reprPrec := RudolphKocurek2024.instReprW.repr }

@[implicit_reducible]

instance RudolphKocurek2024.instFintypeW : Fintype W

Equations

• RudolphKocurek2024.instFintypeW = { elems := { val := ↑RudolphKocurek2024.W.enumList, nodup := RudolphKocurek2024.W.enumList_nodup }, complete := RudolphKocurek2024.instFintypeW._proof_1 }

inductive RudolphKocurek2024.Pred : Type

Two predicates: linguist and philosopher.

• linguist : Pred
• philosopher : Pred

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqPred : DecidableEq Pred

Equations

• RudolphKocurek2024.instDecidableEqPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RudolphKocurek2024.instReprPred.repr : Pred → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instReprPred : Repr Pred

Equations

• RudolphKocurek2024.instReprPred = { reprPrec := RudolphKocurek2024.instReprPred.repr }

@[implicit_reducible]

instance RudolphKocurek2024.instFintypePred : Fintype Pred

Equations

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

inductive RudolphKocurek2024.Entity : Type

One entity: Ann.

• ann : Entity

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqEntity : DecidableEq Entity

Equations

• RudolphKocurek2024.instDecidableEqEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RudolphKocurek2024.instReprEntity : Repr Entity

Equations

• RudolphKocurek2024.instReprEntity = { reprPrec := RudolphKocurek2024.instReprEntity.repr }

def RudolphKocurek2024.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instFintypeEntity : Fintype Entity

Equations

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

@[reducible, inline]

abbrev RudolphKocurek2024.PredLang : FirstOrder.Language

The monadic language over Pred.

Equations

• RudolphKocurek2024.PredLang = FirstOrder.Language.monadic RudolphKocurek2024.Pred

@[reducible, inline]

abbrev RudolphKocurek2024.La : PredLang.CompFormula Entity

"Ann is a linguist"

Equations

• RudolphKocurek2024.La = FirstOrder.Language.CompFormula.matom RudolphKocurek2024.Pred.linguist RudolphKocurek2024.Entity.ann

@[reducible, inline]

abbrev RudolphKocurek2024.Pa : PredLang.CompFormula Entity

"Ann is a philosopher"

Equations

• RudolphKocurek2024.Pa = FirstOrder.Language.CompFormula.matom RudolphKocurek2024.Pred.philosopher RudolphKocurek2024.Entity.ann

@[reducible, inline]

abbrev RudolphKocurek2024.La_mc_Pa : PredLang.CompFormula Entity

"Ann is more a linguist than a philosopher"

Equations

• RudolphKocurek2024.La_mc_Pa = RudolphKocurek2024.La.comp RudolphKocurek2024.Pa

Model 1: Three interpretations (linear order)

inductive RudolphKocurek2024.I3 : Type

Three interpretations: i₀ < i₁ < i₂.

• i0 : I3
• i1 : I3
• i2 : I3

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqI3 : DecidableEq I3

Equations

• RudolphKocurek2024.instDecidableEqI3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RudolphKocurek2024.instReprI3.repr : I3 → ℕ → Std.Format

Equations

• RudolphKocurek2024.instReprI3.repr RudolphKocurek2024.I3.i0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I3.i0")).group prec✝
• RudolphKocurek2024.instReprI3.repr RudolphKocurek2024.I3.i1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I3.i1")).group prec✝
• RudolphKocurek2024.instReprI3.repr RudolphKocurek2024.I3.i2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I3.i2")).group prec✝

@[implicit_reducible]

instance RudolphKocurek2024.instReprI3 : Repr I3

Equations

• RudolphKocurek2024.instReprI3 = { reprPrec := RudolphKocurek2024.instReprI3.repr }

@[implicit_reducible]

instance RudolphKocurek2024.instFintypeI3 : Fintype I3

Equations

• RudolphKocurek2024.instFintypeI3 = { elems := { val := ↑RudolphKocurek2024.I3.enumList, nodup := RudolphKocurek2024.I3.enumList_nodup }, complete := RudolphKocurek2024.instFintypeI3._proof_1 }

def RudolphKocurek2024.ord₃ : SemanticOrdering I3

Linear ordering: i0 ≤ i1 ≤ i2.

Equations

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

@[implicit_reducible]

def RudolphKocurek2024.interp₃ : I3 → W → PredLang.Structure Entity

Interpretation family (a monadic-structure per interpretation):

• i₀: Ann is a philosopher, not a linguist
• i₁: Ann is a linguist, not a philosopher
• i₂: Ann is both

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableAtomsI3WEntityInterp₃ : FirstOrder.Language.DecidableAtoms interp₃

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableRelI3LeOrd₃ : DecidableRel ord₃.le

Equations

• RudolphKocurek2024.instDecidableRelI3LeOrd₃ x✝¹ x✝ = RudolphKocurek2024.instDecidableRelI3LeOrd₃._aux_1 x✝¹ x✝

Observations on Model 1

theorem RudolphKocurek2024.obs1a_mc_consistent_with_both : Eval interp₃ La_mc_Pa ord₃ I3.i2 W.w0 ∧ Eval interp₃ La ord₃ I3.i2 W.w0 ∧ Eval interp₃ Pa ord₃ I3.i2 W.w0

Observation 1a: MCs are consistent with truth of both constituents. At i₂, Ann is both a linguist and a philosopher, yet "Ann is more a linguist than a philosopher" is true — the (La∧¬Pa)-interpretation i₁ outranks the (Pa∧¬La)-interpretation i₀.

theorem RudolphKocurek2024.obs2_mc_B_entails_A (i : I3) : Eval interp₃ La_mc_Pa ord₃ i W.w0 → Eval interp₃ Pa ord₃ i W.w0 → Eval interp₃ La ord₃ i W.w0

Observation 2: A ≻ B, B ⊨ A. If the MC holds and Ann is a philosopher, she is a linguist.

Model 2: Two interpretations (tied) for borderline cases

inductive RudolphKocurek2024.I2 : Type

Two interpretations for borderline / nonclassicality witnesses.

• j0 : I2
• j1 : I2

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqI2 : DecidableEq I2

Equations

• RudolphKocurek2024.instDecidableEqI2 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RudolphKocurek2024.instReprI2 : Repr I2

Equations

• RudolphKocurek2024.instReprI2 = { reprPrec := RudolphKocurek2024.instReprI2.repr }

def RudolphKocurek2024.instReprI2.repr : I2 → ℕ → Std.Format

Equations

• RudolphKocurek2024.instReprI2.repr RudolphKocurek2024.I2.j0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I2.j0")).group prec✝
• RudolphKocurek2024.instReprI2.repr RudolphKocurek2024.I2.j1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I2.j1")).group prec✝

@[implicit_reducible]

instance RudolphKocurek2024.instFintypeI2 : Fintype I2

Equations

• RudolphKocurek2024.instFintypeI2 = { elems := { val := ↑RudolphKocurek2024.I2.enumList, nodup := RudolphKocurek2024.I2.enumList_nodup }, complete := RudolphKocurek2024.instFintypeI2._proof_1 }

def RudolphKocurek2024.tiedOrd : SemanticOrdering I2

Tied ordering: j0 ≡ j1 (both maximal).

Equations

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

@[implicit_reducible]

def RudolphKocurek2024.interp₂ : I2 → W → PredLang.Structure Entity

j₀: La true, Pa false; j₁: La false, Pa true.

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableAtomsI2WEntityInterp₂ : FirstOrder.Language.DecidableAtoms interp₂

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableRelI2LeTiedOrd : DecidableRel tiedOrd.le

Equations

• RudolphKocurek2024.instDecidableRelI2LeTiedOrd x✝¹ x✝ = RudolphKocurek2024.instDecidableRelI2LeTiedOrd._aux_1 x✝¹ x✝

theorem RudolphKocurek2024.obs5_me_neg_consistent : Eval interp₂ (La.equi La.not) tiedOrd I2.j0 W.w0

Observation 5: A ≈ ¬A is satisfiable (not contradictory). With tied interpretations where one makes La true and the other makes La false, "Ann is (exactly) as much a linguist as not" is coherent — it expresses a borderline case.

@[reducible, inline]

abbrev RudolphKocurek2024.NLa : PredLang.CompFormula Entity

¬La

Equations

• RudolphKocurek2024.NLa = RudolphKocurek2024.La.not

Assertoric Content and Acceptance-Preservation

@[implicit_reducible]

def RudolphKocurek2024.interp₃' : I3 → W → PredLang.Structure Entity

For substantive Obs 3: i₂ is linguist only.

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableAtomsI3WEntityInterp₃' : FirstOrder.Language.DecidableAtoms interp₃'

Equations

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

theorem RudolphKocurek2024.obs3_acceptance : AssertoricContent interp₃' (La.inf Pa.not) ord₃ W.w0 → AssertoricContent interp₃' La_mc_Pa ord₃ W.w0

theorem RudolphKocurek2024.tautology_accepted : AssertoricContent interp₂ (La.sup La.not) tiedOrd W.w0

The tautology La ∨ ¬La has assertoric content 1 on the tied model.

theorem RudolphKocurek2024.mc_disj_not_accepted : AssertoricContent interp₂ ((La.comp La.not).sup (La.not.comp La)) tiedOrd W.w0 = (false = true)

Nonclassical acceptance-preservation: (La ≻ ¬La) ∨ (¬La ≻ La) is not accepted on the tied model — the analogue of informational entailment for epistemic modals ([Yal07]).

Degree Modifiers (§6.1)

def RudolphKocurek2024.dist₃ : DistanceFunction I3 ord₃

Distance function for ord₃: close(i) includes interpretations at the same level or one level below.

• d(i₀) = {i₀}
• d(i₁) = {i₀, i₁}
• d(i₂) = {i₁, i₂}

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableRelI3CloseDist₃ : DecidableRel dist₃.close

Equations

• RudolphKocurek2024.instDecidableRelI3CloseDist₃ x✝¹ x✝ = RudolphKocurek2024.instDecidableRelI3CloseDist₃._aux_1 x✝¹ x✝

theorem RudolphKocurek2024.very_la_at_top : EvalVery interp₃ La ord₃ dist₃ I3.i2 W.w0

very La is true at i₂: all interpretations reasonably close to i₂ (namely i₁ and i₂) make La true.

theorem RudolphKocurek2024.very_la_false_at_mid : ¬EvalVery interp₃ La ord₃ dist₃ I3.i1 W.w0

very La is false at i₁: i₀ is reasonably close to i₁ but makes La false.

theorem RudolphKocurek2024.sorta_la_at_mid : EvalSorta interp₃ La ord₃ dist₃ I3.i1 W.w0

sorta La holds at i₁: some close interpretation (i₁ itself) makes La true, even though another close interpretation (i₀) does not.

theorem RudolphKocurek2024.sorta_la_false_at_bot : ¬EvalSorta interp₃ La ord₃ dist₃ I3.i0 W.w0

sorta La is false at i₀: d(i₀) = {i₀}, and La is false at i₀.

Degree Modifier: mostly (§6.1)

theorem RudolphKocurek2024.mostly_la_at_top : EvalMostly interp₃ La ord₃ dist₃ I3.i2 W.w0

mostly La is true at i₂: there is a reasonably high level (i₁) where La is uniformly true, and the only A-false level (i₀) is below it.

theorem RudolphKocurek2024.mostly_la_false_at_mid : ¬EvalMostly interp₃ La ord₃ dist₃ I3.i1 W.w0

mostly La is false at i₁: i₀ is the only candidate level below i₁ in d(i₁), but La is false at i₀.

Bridge: No Reversal and Ordinary Comparison (§7)

Two-Entity Model: No Reversal (§7)

inductive RudolphKocurek2024.Entity2 : Type

Two entities for gradable adjective models.

• ann : Entity2
• ben : Entity2

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqEntity2 : DecidableEq Entity2

Equations

• RudolphKocurek2024.instDecidableEqEntity2 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RudolphKocurek2024.instReprEntity2 : Repr Entity2

Equations

• RudolphKocurek2024.instReprEntity2 = { reprPrec := RudolphKocurek2024.instReprEntity2.repr }

def RudolphKocurek2024.instReprEntity2.repr : Entity2 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instFintypeEntity2 : Fintype Entity2

Equations

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

inductive RudolphKocurek2024.Pred1 : Type

Single predicate: tall.

• tall : Pred1

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqPred1 : DecidableEq Pred1

Equations

• RudolphKocurek2024.instDecidableEqPred1 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RudolphKocurek2024.instReprPred1.repr : Pred1 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instReprPred1 : Repr Pred1

Equations

• RudolphKocurek2024.instReprPred1 = { reprPrec := RudolphKocurek2024.instReprPred1.repr }

@[implicit_reducible]

instance RudolphKocurek2024.instFintypePred1 : Fintype Pred1

Equations

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

@[implicit_reducible]

def RudolphKocurek2024.interpNR : I3 → W → (FirstOrder.Language.monadic Pred1).Structure Entity2

NR model for "Ann is taller than Ben":

• i₀: neither Ann nor Ben is tall (empty extension)
• i₁: Ann is tall, Ben is not (Ann enters the extension first)
• i₂: both are tall

Satisfies No Reversal: extensions are monotonically nested ({} ⊆ {ann} ⊆ {ann, ben}). Uses the same 3-interpretation linear order ord₃ from Model 1.

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableAtomsI3WEntity2InterpNR : FirstOrder.Language.DecidableAtoms interpNR

Equations

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

@[reducible, inline]

abbrev RudolphKocurek2024.Ta : (FirstOrder.Language.monadic Pred1).CompFormula Entity2

"Ann is tall"

Equations

• RudolphKocurek2024.Ta = FirstOrder.Language.CompFormula.matom RudolphKocurek2024.Pred1.tall RudolphKocurek2024.Entity2.ann

@[reducible, inline]

abbrev RudolphKocurek2024.Tb : (FirstOrder.Language.monadic Pred1).CompFormula Entity2

"Ben is tall"

Equations

• RudolphKocurek2024.Tb = FirstOrder.Language.CompFormula.matom RudolphKocurek2024.Pred1.tall RudolphKocurek2024.Entity2.ben

theorem RudolphKocurek2024.nr_tall_ann_ben : NoReversal interpNR ord₃ Pred1.tall W.w0 Entity2.ann Entity2.ben

No Reversal holds for tall: the extensions are monotonically nested, so Ben never outruns Ann.

theorem RudolphKocurek2024.ann_taller_i1 : Eval interpNR (Ta.comp Tb) ord₃ I3.i1 W.w0

Ann is taller than Ben: the MC tall(ann) ≻ tall(ben) is true at i₁ and i₂. Witness: i₁ (Ann is tall, Ben is not).

theorem RudolphKocurek2024.ben_not_taller (i : I3) : ¬Eval interpNR (Tb.comp Ta) ord₃ i W.w0

The reverse MC — Ben taller than Ann — is false everywhere. There is no interpretation where Ben is tall but Ann is not.

theorem RudolphKocurek2024.nr_tall_ben_ann : NoReversal interpNR ord₃ Pred1.tall W.w0 Entity2.ben Entity2.ann

NR also holds with the roles swapped (vacuously: Ben's extension never outruns Ann's), which is the direction eval_mc_iff_delineation_of_noReversal consumes.

@[implicit_reducible]

def RudolphKocurek2024.interpNR_bad : I3 → W → (FirstOrder.Language.monadic Pred1).Structure Entity2

NR-violating model: Ann and Ben "swap" across interpretations.

• i₀: Ann tall, Ben not
• i₁: Ben tall, Ann not (reversal!)
• i₂: both tall

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableAtomsI3WEntity2InterpNR_bad : FirstOrder.Language.DecidableAtoms interpNR_bad

Equations

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

theorem RudolphKocurek2024.nr_fails_bad : ¬NoReversal interpNR_bad ord₃ Pred1.tall W.w0 Entity2.ben Entity2.ann

No Reversal fails on the violating model (for e₁=ben, e₂=ann): Ben is tall at i₁ and Ann is not, but at i₀ ≤ i₁ where Ann is tall, Ben is not — a reversal.

theorem RudolphKocurek2024.mc_delineation_diverge_without_nr : ¬Eval interpNR_bad (Ta.comp Tb) ord₃ I3.i2 W.w0 ∧ Semantics.Gradability.Delineation.comparativeSem (interpretationDelineation interpNR_bad ord₃ Pred1.tall W.w0 I3.i2) Entity2.ann Entity2.ben

Without NR, MC and delineation diverge: the MC Ta ≻ Tb is FALSE at i₂ (the (Tb∧¬Ta)-witness i₁ outranks the (Ta∧¬Tb)-witness i₀, violating the domination clause), but the simple delineation condition (∃ Fa∧¬Fb) is TRUE (i₀ is a witness).

Metalinguistic Conditional (§6.3)

theorem RudolphKocurek2024.mcond_la_pa_false : ¬EvalMCond interp₃ La Pa ord₃ I3.i2 W.w0

La → Pa fails at i₂ even though both conjuncts are true there: the conditional quantifies over all ranked La-interpretations, so it is not the material conditional.

theorem RudolphKocurek2024.mcond_m1 (i : I3) : EvalMCond interp₃ La (La.comp NLa) ord₃ i W.w0

M1 (§6.3): ⊨ A → (A ≻ ¬A) — "if Pluto is a planet, it's more a planet than not", the analogue of epistemic "if p then probably p" ([Yal07]).

ME transitivity: basic vs revised semantics ([Koc24] §B)

Model 4 is the minimal counterexample: La ≻ Ca holds vacuously in the basic semantics (the (La∧¬Ca)-witness l faces no (Ca∧¬La)-witness), breaking A ≈ B, B ≈ C ⊨ A ≈ C; the revised domination clause blocks the vacuous witness and restores transitivity.

inductive RudolphKocurek2024.Pred3 : Type

Three predicates for the transitivity counterexample.

• linguist : Pred3
• philosopher : Pred3
• psychologist : Pred3

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqPred3 : DecidableEq Pred3

Equations

• RudolphKocurek2024.instDecidableEqPred3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RudolphKocurek2024.instReprPred3.repr : Pred3 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instReprPred3 : Repr Pred3

Equations

• RudolphKocurek2024.instReprPred3 = { reprPrec := RudolphKocurek2024.instReprPred3.repr }

@[implicit_reducible]

instance RudolphKocurek2024.instFintypePred3 : Fintype Pred3

Equations

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

inductive RudolphKocurek2024.I4 : Type

Four interpretations for the transitivity counterexample.

• i : I4
• j : I4
• k : I4
• l : I4

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableEqI4 : DecidableEq I4

Equations

• RudolphKocurek2024.instDecidableEqI4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RudolphKocurek2024.instReprI4.repr : I4 → ℕ → Std.Format

Equations

• RudolphKocurek2024.instReprI4.repr RudolphKocurek2024.I4.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I4.i")).group prec✝
• RudolphKocurek2024.instReprI4.repr RudolphKocurek2024.I4.j prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I4.j")).group prec✝
• RudolphKocurek2024.instReprI4.repr RudolphKocurek2024.I4.k prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I4.k")).group prec✝
• RudolphKocurek2024.instReprI4.repr RudolphKocurek2024.I4.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RudolphKocurek2024.I4.l")).group prec✝

@[implicit_reducible]

instance RudolphKocurek2024.instReprI4 : Repr I4

Equations

• RudolphKocurek2024.instReprI4 = { reprPrec := RudolphKocurek2024.instReprI4.repr }

@[implicit_reducible]

instance RudolphKocurek2024.instFintypeI4 : Fintype I4

Equations

• RudolphKocurek2024.instFintypeI4 = { elems := { val := ↑RudolphKocurek2024.I4.enumList, nodup := RudolphKocurek2024.I4.enumList_nodup }, complete := RudolphKocurek2024.instFintypeI4._proof_1 }

def RudolphKocurek2024.ord₄ : SemanticOrdering I4

Ordering: l < j ≡ k < i (three levels). j and k are tied at the middle level — this is essential for the equatives La ≈ Pa and Pa ≈ Ca to hold (witnesses block each other).

Equations

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

@[implicit_reducible]

def RudolphKocurek2024.interp₄ : I4 → W → (FirstOrder.Language.monadic Pred3).Structure Entity

Counterexample interpretations: i all three; j linguist+psychologist; k philosopher only; l linguist+philosopher.

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableAtomsI4WEntityInterp₄ : FirstOrder.Language.DecidableAtoms interp₄

Equations

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

@[implicit_reducible]

instance RudolphKocurek2024.instDecidableRelI4LeOrd₄ : DecidableRel ord₄.le

Equations

• RudolphKocurek2024.instDecidableRelI4LeOrd₄ x✝¹ x✝ = RudolphKocurek2024.instDecidableRelI4LeOrd₄._aux_1 x✝¹ x✝

@[reducible, inline]

abbrev RudolphKocurek2024.La₄ : (FirstOrder.Language.monadic Pred3).CompFormula Entity

"Ann is a linguist" (3-predicate model)

Equations

• RudolphKocurek2024.La₄ = FirstOrder.Language.CompFormula.matom RudolphKocurek2024.Pred3.linguist RudolphKocurek2024.Entity.ann

@[reducible, inline]

abbrev RudolphKocurek2024.Pa₄ : (FirstOrder.Language.monadic Pred3).CompFormula Entity

"Ann is a philosopher" (3-predicate model)

Equations

• RudolphKocurek2024.Pa₄ = FirstOrder.Language.CompFormula.matom RudolphKocurek2024.Pred3.philosopher RudolphKocurek2024.Entity.ann

@[reducible, inline]

abbrev RudolphKocurek2024.Ca₄ : (FirstOrder.Language.monadic Pred3).CompFormula Entity

"Ann is a psychologist"

Equations

• RudolphKocurek2024.Ca₄ = FirstOrder.Language.CompFormula.matom RudolphKocurek2024.Pred3.psychologist RudolphKocurek2024.Entity.ann

Basic semantics: transitivity fails

theorem RudolphKocurek2024.me_basic_la_pa : Eval interp₄ (La₄.equi Pa₄) ord₄ I4.i W.w0

A ≈ B holds: Ann is as much a linguist as a philosopher. The (La∧¬Pa)-witness j and (Pa∧¬La)-witness k are tied at the middle level, blocking both MC directions.

theorem RudolphKocurek2024.me_basic_pa_ca : Eval interp₄ (Pa₄.equi Ca₄) ord₄ I4.i W.w0

B ≈ C holds: Ann is as much a philosopher as a psychologist. The (Pa∧¬Ca)-witnesses k, l and (Ca∧¬Pa)-witness j are balanced: k is tied with j, blocking both MC directions.

theorem RudolphKocurek2024.me_basic_la_ca_fails : ¬Eval interp₄ (La₄.equi Ca₄) ord₄ I4.i W.w0

A ≈ C FAILS: basic semantics predicts Ann is MORE a linguist than a psychologist. ME transitivity is violated.

theorem RudolphKocurek2024.mc_basic_la_gt_ca : Eval interp₄ (La₄.comp Ca₄) ord₄ I4.i W.w0

The failure mechanism: La ≻ Ca holds in the basic semantics. The (La∧¬Ca)-witness l dominates all (Ca∧¬La)-interpretations vacuously — there are none (Ca is true only at i and j, where La is also true).

Revised semantics: transitivity restored

theorem RudolphKocurek2024.mc_revised_la_ca_blocked : ¬EvalRevised interp₄ (La₄.comp Ca₄) ord₄ I4.i W.w0

Under the revised semantics, La ≻ Ca is blocked: the (La∧¬Ca)- witness l cannot dominate all Ca-interpretations (i and j are above it) or all ¬La-interpretations (k is above it).

theorem RudolphKocurek2024.me_revised_la_ca : EvalRevised interp₄ (La₄.equi Ca₄) ord₄ I4.i W.w0

ME transitivity is restored: A ≈ C holds under the revised semantics, as required by transitivity from A ≈ B and B ≈ C.

theorem RudolphKocurek2024.me_revised_la_pa : EvalRevised interp₄ (La₄.equi Pa₄) ord₄ I4.i W.w0

The revised semantics preserves A ≈ B (no regression).

theorem RudolphKocurek2024.me_revised_pa_ca : EvalRevised interp₄ (Pa₄.equi Ca₄) ord₄ I4.i W.w0

The revised semantics preserves B ≈ C (no regression).

Agreement on Model 1

theorem RudolphKocurek2024.revised_agrees_model1 (x : I3) : Eval interp₃ La_mc_Pa ord₃ x W.w0 ↔ EvalRevised interp₃ La_mc_Pa ord₃ x W.w0

On Model 1 (linear ordering), the revised MC agrees with the basic MC. The two diverge only when the revised semantics' stronger domination clause matters — on a linear ordering with no ties at critical levels, the basic witnesses satisfy the revised conditions too.