Metalinguistic Degrees #
@cite{rudolph-kocurek-2024}
Degree-theoretic formulation of metalinguistic gradability (Supplement §C).
The revised semantics (evalRevised) induces a degree structure on
sentences: the metalinguistic degree of a sentence A (relative to
an index ⟨≤, i, w⟩) is the equivalence class of its denotation set
⟦A⟧_i = {j ≤ i | ⟦A⟧^{j,w} = 1} under a matching relation ∼.
Key Results #
- ∼ is an equivalence relation (Fact 8): reflexive ✓, symmetric ✓, transitive ✓ (⊆ field)
- ⊐ properties (Facts 11–12): irreflexive ✓, transitive ✓, total ✓, respects ∼ ✓ (⊆ field)
- A ≈ B iff deg(A) = deg(B) (Fact 9) ✓: ME = same metalinguistic degree
- A ≻ B iff deg(A) ⊐ deg(B) (Fact 10) ✓: revised MC = degree ordering
This connects the expressivist framework to a proper algebraic structure
backed by Mathlib's Setoid, Quotient, and order theory. The metalinguistic
degree construction parallels @cite{klein-1980}'s emergent degrees
(see Hierarchy.lean:nondistinct_iff_equal_measure), but operates on
interpretations rather than entities.
Convert a SemanticOrdering to a Mathlib Preorder.
A def (not an instance) to avoid global instance pollution —
use letI := ord.toPreorder locally to bring ≤/< into scope.
Equations
- Semantics.Comparison.MetalinguisticDegree.SemanticOrdering.toPreorder ord = { le := ord.le, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
Instances For
The field I_i: the set of interpretations ranked at or below i.
Equations
- Semantics.Comparison.MetalinguisticDegree.field ord i = {j : I | ord.le j i}
Instances For
The denotation of a formula: the set of interpretations in I_i where the formula is true (under the revised semantics).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The complement of a set relative to the field I_i.
Equations
Instances For
Condition (i) of the ∼ equivalence: every element of X\Y is matched by an element of Y\X at least as high, and vice versa.
This is the same as the basic ME matching condition applied to interpretation sets rather than formulas.
Equations
- Semantics.Comparison.MetalinguisticDegree.equivCond1 ord i X Y = ((∀ i' ∈ X \ Y, ∃ i'' ∈ Y \ X, ord.le i' i'') ∧ ∀ i' ∈ Y \ X, ∃ i'' ∈ X \ Y, ord.le i' i'')
Instances For
Condition (ii) of the ∼ equivalence: every element of the symmetric difference (X ∪ Y) \ (X ∩ Y) is dominated by both an element of X ∩ Y and an element of X̄ ∩ Ȳ (relative to I_i).
This handles the "Figure 1" situation where A ↔ ¬B always holds at top-ranked interpretations: if every A-or-B-but-not-both interpretation is matched by both an A∧B and a ¬A∧¬B interpretation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Metalinguistic degree equivalence: X ∼_i Y.
Two interpretation sets have the same metalinguistic degree iff either (i) their symmetric difference elements are pairwise matched in rank, or (ii) every unmatched element is dominated by both an element in the overlap and an element outside both sets.
This mirrors the revised ME truth conditions (Supplement §B) applied to sets rather than formulas.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bool-valued decidable version of equivCond1.
Equations
- Semantics.Comparison.MetalinguisticDegree.equivCond1B ord i X Y = (decide (∀ i' ∈ X \ Y, ∃ i'' ∈ Y \ X, ord.le i' i'') && decide (∀ i' ∈ Y \ X, ∃ i'' ∈ X \ Y, ord.le i' i''))
Instances For
Bool-valued decidable version of equivCond2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bool-valued decidable version of degreeEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fact 8a: ∼ is reflexive. X \ X = ∅, so all conditions are vacuously satisfied.
Fact 8b: ∼ is symmetric. Both conditions are symmetric in X and Y: condition (i) swaps the two conjuncts, and condition (ii) is invariant under X ↔ Y since X ∩ Y = Y ∩ X and X ∪ Y = Y ∪ X.
X ⊐ Y: interpretation set X is strictly better than Y.
Mirrors the revised MC truth conditions (Supplement §B): ∃ i' ∈ I_i such that i' ∈ X \ Y and either (a) all elements of X ∩ Y are strictly below i', or (b) all elements of I_i \ (X ∪ Y) are strictly below i', and in both cases all elements of Y \ X are strictly below i'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bool-valued decidable version of strictlyBetter.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fact 12a: ⊐ is irreflexive on sets. i' ∈ X \ X is impossible, so no witness exists.
If X ∼ Y, then ¬(X ⊐ Y). Under equivCond1, any witness i' ∈ X\Y is matched by i'' ∈ Y\X with i' ≤ i'', contradicting i'' < i'. Under equivCond2, the witness is dominated by an X∩Y or field(X∪Y) element, contradicting the inner disjunct of ⊐.
Fact 11: ⊐ respects ∼ on the right. If X ⊐ Y and Y ∼ Z (with all sets in the field), then X ⊐ Z. Under left inner: m dominates all of Y, m ∉ Z is forced, and matching through Y∼Z extends domination to Z\Y. Under right inner: m dominates field\X; if m ∉ Z, Z\X ⊆ field\X; if m ∈ Z, use Y∼Z to find alternative witness in X\Z.
Fact 11: ⊐ respects ∼ on the left. If X ⊐ Y and X ∼ Z (with all sets in the field), then Z ⊐ Y. Under left inner: m dominates all of Y; use X∼Z to find a witness in Z\Y (either m itself or a matched element). Under right inner: m dominates field\X; m ∈ Z is forced (matching m ∈ X\Z through X∼Z yields z ∈ field\X < m, contradicting le m z); elements of Y\Z ∩ X use X∼Z matching to field\X for domination.
Fact 12b: ⊐ is transitive on sets. Given witnesses m₁ (X⊐Y) and m₂ (Y⊐Z), split on which is higher. If m₂ ≤ m₁: m₁ cannot be in Z (else m₁ ∈ Z\Y with ¬(m₁ < m₂)), so m₁ ∈ X\Z is the witness for X⊐Z. If m₁ ≤ m₂: m₂ must be in X (else m₂ ∈ Y\X with ¬(m₂ < m₁)), so m₂ ∈ X\Z is the witness for X⊐Z.
Fact 12c: ⊐ is total on nonequivalent sets. For any X, Y ⊆ I_i, either X ∼ Y or X ⊐ Y or Y ⊐ X.
The proof finds the maximum element m of the symmetric difference (X\Y)∪(Y\X), then case-splits on whether all elements on the other side are strictly below m. If yes, we get ⊐; if no, we get ∼ via one of the two equivalence conditions.
Fact 8c: ∼ is transitive (for sets in the field). Indirect proof: if ¬(X∼Z), totality gives X⊐Z or Z⊐X.
- X⊐Z: respects_right(X,Z,Y) with Z∼Y gives X⊐Y, contradicting X∼Y.
- Z⊐X: respects_right(Z,X,Y) with X∼Y gives Z⊐Y, contradicting Y∼Z. This avoids the direct Schröder-Bernstein bouncing chain argument.
The metalinguistic setoid: ∼ as a Mathlib Setoid on field-subsets.
The carrier is {X : Finset I // X ⊆ field ord i} because
transitivity requires the ⊆ field hypothesis (via totality).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The type of metalinguistic degrees: equivalence classes of interpretation sets under ∼.
A metalinguistic degree is a set of sets of interpretations —
all the interpretation sets that are "ranked as high" as each other.
The degree of a sentence A is deg(⟦A⟧_i).
Equations
Instances For
Compute the metalinguistic degree of an interpretation set.
Equations
- Semantics.Comparison.MetalinguisticDegree.deg ord i X hX = ⟦⟨X, hX⟩⟧
Instances For
The metalinguistic degree of a formula's denotation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fact 10: revised MC holds iff denotation of A ⊐ denotation of B. ⟦A ≻ B⟧^{≤,i,w}_revised = 1 iff ⟦A⟧_i ⊐ ⟦B⟧_i.
Fact 9: ME holds iff denotations have the same degree.
⟦A ≈ B⟧^{≤,i,w}_revised = 1 iff ⟦A⟧_i ∼ ⟦B⟧_i.
This connects the Boolean evaluation function evalRevised to the
algebraic degree structure. Forward direction uses strictlyBetter_total.
Fact 13a: the full field I_i is the maximum degree. deg(⊤) = {I_i}: the tautology's denotation is the whole field, and nothing is strictly better than I_i.
Fact 13b: the empty set is the minimum degree. deg(⊥) = {∅}: the contradiction's denotation is empty, and nothing is strictly worse than ∅.