Metalinguistic Gradability

@cite{rudolph-kocurek-2024}

Semantic expressivist framework for metalinguistic comparatives ("Ann is more a linguist than a philosopher"), metalinguistic equatives, degree modifiers (very much, sorta, mostly), and metalinguistic conditionals.

Core Idea

Speakers express not only factual commitments (about the world) but also interpretive commitments (about how to interpret language). The common ground is generalized from sets of worlds to sets of ordering-world pairs ⟨≤, w⟩, where ≤ is a total preorder over interpretations (a semantic ordering). Assertions update this enriched common ground.

Formal System

Truth is evaluated relative to a triple ⟨≤, i, w⟩:

• ≤ : semantic ordering (total preorder on interpretations)
• i : the current interpretation
• w : the world of evaluation

An interpretation maps names and predicates to world-indexed extensions. Ordinary sentences ignore ≤; metalinguistic operators quantify over it.

Operators

• A ≻ B (MC): ∃ (A∧¬B)-interp ranked ≤ i, above all (B∧¬A)-interps ≤ i
• A ≈ B (ME): ¬(A ≻ B) ∧ ¬(B ≻ A)
• A ≫ B (much more): like ≻ but with "far below" (≪) instead of <
• very A := A ≫ ¬A — true on all reasonably close interpretations
• sorta A := ¬very(¬A) — true on some reasonably close interpretation
• mostly A := ∃ reasonably high level where A is uniformly true
• A → B (metalinguistic conditional): restricts ordering to A-interps
• evalRevised: revised MC for ME transitivity (Supplement §B) — strengthened domination clause blocks vacuous comparatives

Entailment

Two notions:

• Truth-preservation (⊨): preserves truth at all ⟨≤, i, w⟩
• Acceptance-preservation (⊩): preserves assertoric content |A| (A is true at all ≤-maximal interpretations)

⊩ is nonclassical: A ⊩ A ≻ ¬A and ¬A ⊩ ¬A ≻ A, but A ∨ ¬A ⊮ (A ≻ ¬A) ∨ (¬A ≻ A). This parallels informational entailment for epistemic modals (@cite{yalcin-2007}).

structure Semantics.Comparison.Metalinguistic.Interpretation (W Pred Entity : Type) : Type

An interpretation maps predicate symbols to world-indexed extensions.

For the finite decidable models we work with, an interpretation is simply a function from predicates and entities to Bool at each world.

• ext : Pred → W → Entity → Bool

  Extension of predicate P at world w: the set of entities P applies to.

structure Semantics.Comparison.Metalinguistic.SemanticOrdering (I : Type) : Type

A semantic ordering is a total preorder on a set of interpretations.

Represents a speaker's relative interpretive commitments: le i j means the speaker is at least as committed to j as to i.

le is Prop-valued with DecidableRel for decidable computation. Use ofBool for the common case of defining orderings via pattern matching.

• le : I → I → Prop

  The preorder relation: le i j means i is ranked no higher than j.

• le_refl (i : I) : self.le i i

  Reflexivity

• le_trans (i j k : I) : self.le i j → self.le j k → self.le i k

  Transitivity

• le_total (i j : I) : self.le i j ∨ self.le j i

  Totality: any two interpretations are comparable

• decRel : DecidableRel self.le

  Decidability of the ordering relation

def Semantics.Comparison.Metalinguistic.SemanticOrdering.leB {I : Type} (ord : SemanticOrdering I) (i j : I) : Bool

Bool-valued le for computation (eval, native_decide).

Equations

• ord.leB i j = decide (ord.le i j)

def Semantics.Comparison.Metalinguistic.SemanticOrdering.lt {I : Type} (ord : SemanticOrdering I) (i j : I) : Prop

Strict ordering (Prop): i is ranked strictly below j.

Equations

• ord.lt i j = (ord.le i j ∧ ¬ord.le j i)

@[implicit_reducible]

instance Semantics.Comparison.Metalinguistic.SemanticOrdering.decRelLt {I : Type} (ord : SemanticOrdering I) : DecidableRel ord.lt

Decidability of the strict ordering.

Equations

• ord.decRelLt i j = inferInstance

def Semantics.Comparison.Metalinguistic.SemanticOrdering.ltB {I : Type} (ord : SemanticOrdering I) (i j : I) : Bool

Bool-valued strict ordering for computation.

Equations

• ord.ltB i j = (ord.leB i j && !ord.leB j i)

def Semantics.Comparison.Metalinguistic.SemanticOrdering.equiv {I : Type} (ord : SemanticOrdering I) (i j : I) : Prop

Equivalence: i and j are ranked at the same level.

Equations

• ord.equiv i j = (ord.le i j ∧ ord.le j i)

def Semantics.Comparison.Metalinguistic.SemanticOrdering.equivB {I : Type} (ord : SemanticOrdering I) (i j : I) : Bool

Bool-valued equivalence for computation.

Equations

• ord.equivB i j = (ord.leB i j && ord.leB j i)

theorem Semantics.Comparison.Metalinguistic.SemanticOrdering.le_of_not_lt {I : Type} (ord : SemanticOrdering I) {a b : I} : ¬ord.lt a b → ord.le b a

¬(a < b) → b ≤ a (by totality).

def Semantics.Comparison.Metalinguistic.SemanticOrdering.ofBool {I : Type} (f : I → I → Bool) (h_refl : ∀ (i : I), f i i = true) (h_trans : ∀ (i j k : I), f i j = true → f j k = true → f i k = true) (h_total : ∀ (i j : I), f i j = true ∨ f j i = true) : SemanticOrdering I

Construct a SemanticOrdering from a Bool-valued function. Convenient for defining concrete orderings via pattern matching.

Equations

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

inductive Semantics.Comparison.Metalinguistic.MFormula (Pred Entity : Type) : Type

A metalinguistic formula over predicates and entities.

The language includes atomic predication, boolean connectives, and the metalinguistic comparative ≻ (.mc).

• atom {Pred Entity : Type} : Pred → Entity → MFormula Pred Entity
• neg {Pred Entity : Type} : MFormula Pred Entity → MFormula Pred Entity
• conj {Pred Entity : Type} : MFormula Pred Entity → MFormula Pred Entity → MFormula Pred Entity
• disj {Pred Entity : Type} : MFormula Pred Entity → MFormula Pred Entity → MFormula Pred Entity
• mc {Pred Entity : Type} : MFormula Pred Entity → MFormula Pred Entity → MFormula Pred Entity

@[implicit_reducible]

instance Semantics.Comparison.Metalinguistic.instDecidableEqMFormula {Pred✝ Entity✝ : Type} [DecidableEq Pred✝] [DecidableEq Entity✝] : DecidableEq (MFormula Pred✝ Entity✝)

Equations

• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula = Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq

def Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq {Pred✝ Entity✝ : Type} [DecidableEq Pred✝] [DecidableEq Entity✝] (x✝ x✝¹ : MFormula Pred✝ Entity✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (Semantics.Comparison.Metalinguistic.MFormula.atom a a_1) a_2.neg = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (Semantics.Comparison.Metalinguistic.MFormula.atom a a_1) (a_2.conj a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (Semantics.Comparison.Metalinguistic.MFormula.atom a a_1) (a_2.disj a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (Semantics.Comparison.Metalinguistic.MFormula.atom a a_1) (a_2.mc a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq a.neg (Semantics.Comparison.Metalinguistic.MFormula.atom a_1 a_2) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq a.neg (a_1.conj a_2) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq a.neg (a_1.disj a_2) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq a.neg (a_1.mc a_2) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.conj a_1) (Semantics.Comparison.Metalinguistic.MFormula.atom a_2 a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.conj a_1) a_2.neg = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.conj a_1) (a_2.disj a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.conj a_1) (a_2.mc a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.disj a_1) (Semantics.Comparison.Metalinguistic.MFormula.atom a_2 a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.disj a_1) a_2.neg = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.disj a_1) (a_2.conj a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.disj a_1) (a_2.mc a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.mc a_1) (Semantics.Comparison.Metalinguistic.MFormula.atom a_2 a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.mc a_1) a_2.neg = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.mc a_1) (a_2.conj a_3) = isFalse ⋯
• Semantics.Comparison.Metalinguistic.instDecidableEqMFormula.decEq (a.mc a_1) (a_2.disj a_3) = isFalse ⋯

def Semantics.Comparison.Metalinguistic.MFormula.impl {Pred Entity : Type} (A B : MFormula Pred Entity) : MFormula Pred Entity

Material conditional (within the object language).

Equations

• A.impl B = A.neg.disj B

def Semantics.Comparison.Metalinguistic.MFormula.me {Pred Entity : Type} (A B : MFormula Pred Entity) : MFormula Pred Entity

Metalinguistic equative: A ≈ B := ¬(A ≻ B) ∧ ¬(B ≻ A).

Equations

• A.me B = (A.mc B).neg.conj (B.mc A).neg

def Semantics.Comparison.Metalinguistic.MFormula.wmc {Pred Entity : Type} (A B : MFormula Pred Entity) : MFormula Pred Entity

Weak metalinguistic comparative: A ≥ B := (A ≻ B) ∨ (A ≈ B).

Equations

• A.wmc B = (A.mc B).disj (A.me B)

def Semantics.Comparison.Metalinguistic.eval {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (φ : MFormula Pred Entity) (ord : SemanticOrdering I) (i : I) (w : W) : Bool

Evaluate a formula at an index ⟨≤, i, w⟩.

• Atomic: true iff the entity is in the predicate's extension at w under i.
• MC (A ≻ B): true iff ∃ i' ≤ i with (A∧¬B) true at i', and ∀ i'' ≤ i, (B∧¬A) true at i'' implies i'' < i'.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Comparison.Metalinguistic.eval interpFn (Semantics.Comparison.Metalinguistic.MFormula.atom P e) ord i w = (interpFn i).ext P w e
• Semantics.Comparison.Metalinguistic.eval interpFn A.neg ord i w = !Semantics.Comparison.Metalinguistic.eval interpFn A ord i w

def Semantics.Comparison.Metalinguistic.isMaximal {I : Type} [Fintype I] (ord : SemanticOrdering I) (i : I) : Bool

Is interpretation i maximal in the ordering?

Equations

• Semantics.Comparison.Metalinguistic.isMaximal ord i = Semantics.Comparison.Metalinguistic.bAll✝ I fun (i' : I) => !ord.ltB i i'

def Semantics.Comparison.Metalinguistic.assertoricContent {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (φ : MFormula Pred Entity) (ord : SemanticOrdering I) (w : W) : Bool

Assertoric content: A is true at all ≤-maximal interpretations.

|A|^{≤,w} = 1 iff ∀ i, i is maximal → ⟦A⟧^{≤,i,w} = 1. A speaker accepts A iff on every ordering-world pair they leave open, A is true at every top-ranked interpretation.

Equations

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

def Semantics.Comparison.Metalinguistic.truthPreserves {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (premises : List (MFormula Pred Entity)) (conclusion : MFormula Pred Entity) : Prop

Truth-preservation (⊨): for all ⟨≤, i, w⟩, if premises are true then conclusion is true. Classical; validates Observations 1, 2, 4, 5.

Equations

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

def Semantics.Comparison.Metalinguistic.acceptancePreserves {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (premises : List (MFormula Pred Entity)) (conclusion : MFormula Pred Entity) : Prop

Acceptance-preservation (⊩): for all ⟨≤, w⟩, if assertoric content of all premises holds, then assertoric content of conclusion holds. Nonclassical; validates Observation 3 (A ∧ ¬B ⊩ A ≻ B).

Equations

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

structure Semantics.Comparison.Metalinguistic.DistanceFunction (I : Type) (ord : SemanticOrdering I) : Type

A distance function for a semantic ordering.

Maps each interpretation to the set of interpretations "reasonably close" to it. Used to define very much, sorta, mostly.

• close : I → I → Bool

  d(i) = the set of interpretations reasonably close to i. close i i' means i' is reasonably close to i.

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

  Centered: i ∈ d(i)

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

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

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

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

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

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

def Semantics.Comparison.Metalinguistic.farBelow {I : Type} (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i j : I) : Bool

"Far below": i ≪ j iff i ≤ j and i ∉ d(j). i is ranked below j and not even reasonably close.

Equations

• Semantics.Comparison.Metalinguistic.farBelow ord d i j = (ord.leB i j && !d.close j i)

def Semantics.Comparison.Metalinguistic.evalMuchMore {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (φ ψ : MFormula Pred Entity) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Bool

Much more (A ≫ B): like A ≻ B but with ≪ instead of <.

⟦A ≫ B⟧ = 1 iff ∃ i' ≤ i with (A∧¬B) true at i', and ∀ i'' ≤ i with (B∧¬A) true at i'', i'' ≪ i'.

Equations

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

def Semantics.Comparison.Metalinguistic.evalVery {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (φ : MFormula Pred Entity) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Bool

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

Reduces to: ∀ i' ∈ d(i), ⟦A⟧^{i',w} = 1.

Equations

• Semantics.Comparison.Metalinguistic.evalVery interpFn φ ord d i w = Semantics.Comparison.Metalinguistic.evalMuchMore interpFn φ φ.neg ord d i w

def Semantics.Comparison.Metalinguistic.evalSorta {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (φ : MFormula Pred Entity) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Bool

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

Reduces to: ∃ i' ∈ d(i), ⟦A⟧^{i',w} = 1.

Equations

• Semantics.Comparison.Metalinguistic.evalSorta interpFn φ ord d i w = !Semantics.Comparison.Metalinguistic.evalVery interpFn φ.neg ord d i w

def Semantics.Comparison.Metalinguistic.evalMostly {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (φ : MFormula Pred Entity) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Bool

mostly A (eq. 97 of @cite{rudolph-kocurek-2024}). True iff there is a reasonably high level (strictly below the top, within the distance threshold) where A is uniformly true, and all A-false levels below the current interpretation are ranked below it.

mostly A is compatible with A and with ¬A (unlike very). It entails sorta A. And mostly A ∧ mostly ¬A is contradictory.

Equations

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

def Semantics.Comparison.Metalinguistic.noReversal {I W Pred Entity : Type} (interpFn : I → Interpretation W Pred Entity) (ord : SemanticOrdering I) (P : Pred) (w : W) (e1 e2 : Entity) : Prop

No Reversal constraint (van Benthem 1990; §7 of @cite{rudolph-kocurek-2024}).

If entity e₁ is in the extension of P and e₂ is not at interpretation i, then for all i' ≤ i where e₂ enters the extension, e₁ must also be in the extension.

When NR holds for gradable adjectives, the MC Fa ≻ Gb simplifies to the delineation comparative: ∃ i' ≤ i with Fa∧¬Gb — the second clause of the MC semantics (about dominating all (B∧¬A)-witnesses) becomes redundant. This connects metalinguistic comparatives to @cite{klein-1980} and @cite{kamp-1975}. See Theories/Semantics/Comparison/Delineation.lean for the delineation framework.

Equations

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

def Semantics.Comparison.Metalinguistic.evalRevised {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (φ : MFormula Pred Entity) (ord : SemanticOrdering I) (i : I) (w : W) : Bool

Evaluate a formula under the revised MC semantics (Supplement §B of @cite{rudolph-kocurek-2024}).

The basic semantics (eval) fails ME transitivity: A ≈ B, B ≈ C ⊭ A ≈ C. The revised semantics strengthens the MC: the (A∧¬B)-witness must dominate either all B-interpretations or all ¬A-interpretations, not merely all (B∧¬A)-interpretations. This prevents cases where the basic MC holds vacuously due to the absence of (B∧¬A)-witnesses while (A∧B) or (¬A∧¬B) interpretations remain undominated.

Formally (simplified form): A ≻ B iff ∃ i' ≤ i with A∧¬B at i', and either (a) ∀ i'' ≤ i: ⟦B⟧^{i''} → i'' < i', or (b) ∀ i'' ≤ i: ⟦¬A⟧^{i''} → i'' < i'.

Properties (Supplement §B):

• All basic entailment patterns (Fact 3 a-n) are preserved (Fact 5)
• ME transitivity is validated: A ≈ B, B ≈ C ⊨ A ≈ C (Fact 6)
• Interdefinable with basic semantics (Fact 7): A >_basic B = (A∧¬B) >_revised (B∧¬A)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Comparison.Metalinguistic.evalRevised interpFn (Semantics.Comparison.Metalinguistic.MFormula.atom P e) ord i w = (interpFn i).ext P w e
• Semantics.Comparison.Metalinguistic.evalRevised interpFn A.neg ord i w = !Semantics.Comparison.Metalinguistic.evalRevised interpFn A ord i w

def Semantics.Comparison.Metalinguistic.evalGen {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (φ : MFormula Pred Entity) (le : I → I → Bool) (i : I) (w : W) : Bool

Evaluate a formula with a raw ordering relation.

Like eval, but takes le : I → I → Bool directly rather than a SemanticOrdering. Needed for metalinguistic conditionals, where the consequent is evaluated relative to a restricted ordering ≤_A that may not satisfy totality (since non-A interpretations are dropped). Agrees with eval when given ord.le.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Comparison.Metalinguistic.evalGen interpFn (Semantics.Comparison.Metalinguistic.MFormula.atom P e) le i w = (interpFn i).ext P w e
• Semantics.Comparison.Metalinguistic.evalGen interpFn A.neg le i w = !Semantics.Comparison.Metalinguistic.evalGen interpFn A le i w

def Semantics.Comparison.Metalinguistic.restrictLE {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (A : MFormula Pred Entity) (le : I → I → Bool) (w : W) : I → I → Bool

Restrict an ordering relation to A-interpretations (§6.3).

≤_A = {⟨i, j⟩ | i ≤ j ∧ ⟦A⟧^{≤,i,w} = 1 ∧ ⟦A⟧^{≤,j,w} = 1}

Drops non-A interpretations from the ordering. The resulting relation satisfies reflexivity (at A-interps) and transitivity, but not totality — hence the consequent is evaluated via evalGen rather than eval.

Equations

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

def Semantics.Comparison.Metalinguistic.evalMCond {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (A B : MFormula Pred Entity) (ord : SemanticOrdering I) (i : I) (w : W) : Bool

Metalinguistic conditional (eq. 120 of @cite{rudolph-kocurek-2024}).

⟦A → B⟧^{≤,i,w} = 1 iff ∀ i' ≤ i : ⟦A⟧^{≤,i',w} = 1 → ⟦B⟧^{≤_A,i',w} = 1

The antecedent A is evaluated with the full ordering ≤. The consequent B is evaluated with the A-restricted ordering ≤_A. When A and B are non-metagradable (contain no ≻), ⟦B⟧^{≤_A} = ⟦B⟧^{≤}, so the conditional reduces to interpretation-strict implication: every ranked A-interpretation is a B-interpretation.

Key properties:

• C1: (A → B) ⊨ (B ≥ A) — conditionals entail weak comparatives
• M1: ⊨ A → (A ≻ ¬A) — classically valid
• M2: A → B, ¬B ⊮ ¬A — modus tollens fails for acceptance

Equations

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

structure Semantics.Comparison.Metalinguistic.OrderingWorldPair (I W : Type) : Type

An ordering-world pair: the enriched index for metalinguistic CG.

The common ground is a set of ordering-world pairs ⟨≤, w⟩ compatible with speakers' factual AND interpretive commitments.

• ord : SemanticOrdering I
• world : W

@[reducible, inline]

abbrev Semantics.Comparison.Metalinguistic.MetalinguisticCG (I W : Type) : Type

The metalinguistic common ground: a set of ordering-world pairs.

Generalizes Stalnaker's context set (= set of worlds) to include interpretive commitments. Projects to a classical context set via existential quantification over orderings.

Equations

• Semantics.Comparison.Metalinguistic.MetalinguisticCG I W = (Semantics.Comparison.Metalinguistic.OrderingWorldPair I W → Prop)

def Semantics.Comparison.Metalinguistic.MetalinguisticCG.toContextSet {I W : Type} (cg : MetalinguisticCG I W) : Core.CommonGround.ContextSet W

Project to a classical context set by existentially quantifying over semantic orderings. A world w is in the context set iff some ordering paired with w is in the metalinguistic CG.

Equations

• cg.toContextSet w = ∃ (ord : Semantics.Comparison.Metalinguistic.SemanticOrdering I), cg { ord := ord, world := w }

def Semantics.Comparison.Metalinguistic.MetalinguisticCG.updateAssertoric {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (cg : MetalinguisticCG I W) (φ : MFormula Pred Entity) : MetalinguisticCG I W

Update with assertoric content: keep pairs where |A| holds.

Equations

• Semantics.Comparison.Metalinguistic.MetalinguisticCG.updateAssertoric interpFn cg φ pair = (cg pair ∧ Semantics.Comparison.Metalinguistic.assertoricContent interpFn φ pair.ord pair.world = true)

@[implicit_reducible]

instance Semantics.Comparison.Metalinguistic.instHasContextSetMetalinguisticCG {I W : Type} : Core.CommonGround.HasContextSet (MetalinguisticCG I W) W

MetalinguisticCG projects to a ContextSet via HasContextSet.

Equations

• Semantics.Comparison.Metalinguistic.instHasContextSetMetalinguisticCG = { toContextSet := Semantics.Comparison.Metalinguistic.MetalinguisticCG.toContextSet }

theorem Semantics.Comparison.Metalinguistic.evalRevised_mc_iff {I W Pred Entity : Type} [Fintype I] (interpFn : I → Interpretation W Pred Entity) (A B : MFormula Pred Entity) (ord : SemanticOrdering I) (i : I) (w : W) : evalRevised interpFn (A.mc B) ord i w = true ↔ ∃ (i' : I), ord.le i' i ∧ evalRevised interpFn A ord i' w = true ∧ evalRevised interpFn B ord i' w = false ∧ ((∀ (i'' : I), ord.le i'' i → evalRevised interpFn B ord i'' w = true → ord.lt i'' i') ∨ ∀ (i'' : I), ord.le i'' i → evalRevised interpFn A ord i'' w = false → ord.lt i'' i')

Prop-level characterization of revised MC (evalRevised on .mc A B). Converts Boolean bAny/bAll wrappers to standard Prop quantifiers.