Rudolph and Kocurek (2024): Metalinguistic Gradability

Truth is relative to a semantic ordering, a total preorder ranking interpretations by the strength of a speaker's commitment to them, together with an interpretation and a world. A more than B holds when some interpretation ranked no higher than the index makes A true and B false and outranks every one that makes B true and A false, and the equative is the failure of both comparatives. Degree modifiers come from a distance function on interpretations, the conditional restricts the ordering to the antecedent's interpretations, and under No Reversal the comparative is Klein's delineation comparative.

The supplement strengthens the comparative so that the equative becomes transitive, and shows that metalinguistic degrees, the classes of sets of interpretations under the revised equative, form a bounded linear order on which the revised comparative is the comparative of degree semantics.

Main results

• comp_trans, accepted_comp_of_accepted: the comparative is transitive, and a sentence with its negated rival entails it for acceptance but not for truth.
• evalVery_iff: very A is truth at every reasonably close interpretation.
• evalRevised_equi_trans: the revised equative is transitive, unlike the basic one.
• mc_iff_formulaDeg_lt: the revised comparative compares metalinguistic degrees.

Implementation notes

• An interpretation is a world-indexed family of first-order structures. The comparative is the strict domination lift of Holliday and Icard on the cone below the index, which much more shares with a coarser dominance relation.
• SemanticOrdering bundles a total preorder as data, since a common ground is a set of pairs of an ordering and a world.
• The supplement's revised comparative and equative are clauses on predicates over the cone (RevisedComp, RevisedEqui). The revised semantics applies them to truth sets and the degree theory to sets of interpretations, the two uses the supplement says mirror each other. Degrees are classes of arbitrary sets, which the clauses read only on the cone.
• Finite models rank interpretations by a map into ℕ and list each predicate's extension.

TODO

• The paper states if A then more A than not (its Observation M1) for every A, but the consequent evaluates A under the restricted ordering; mcond_comp_not proves it for A free of the comparative.
• The supplement's semantics for nontotal orderings and its quantifiers for metalinguistic superlatives are not formalized.

References

• R. E. Rudolph and A. W. Kocurek, Metalinguistic gradability (2024)
• A. W. Kocurek, Supplement to "Metalinguistic gradability" (2024)
• W. H. Holliday and T. F. Icard III, Measure Semantics and Qualitative Semantics for Epistemic Modals (2013)
• E. Klein, A Semantics for Positive and Comparative Adjectives (1980)
• D. Lewis, Counterfactuals (1973)
• A. Kratzer, Modals and Conditionals (2012)
• J. Y. Halpern, Reasoning about Uncertainty (2003)
• S. Yalcin, Epistemic Modals (2007)

Semantic orderings

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

A semantic ordering is a total preorder on interpretations, the paper's ranking of interpretations by strength of interpretive commitment. It is a structure and not a Preorder instance, because a common ground is a set of pairs of an ordering and a world, so orderings are data. The strict part is kept transparent so that finite models decide.

• le : I → I → Prop

  The ranking, where le a b means that a is ranked no higher than b.

• isPreorder : IsPreorder I self.le

  The ranking is reflexive and transitive.

• total : Std.Total self.le

  Any two interpretations are comparable.

theorem RudolphKocurek2024.SemanticOrdering.le_refl {I : Type u_1} (ord : SemanticOrdering I) (a : I) : ord.le a a

theorem RudolphKocurek2024.SemanticOrdering.le_trans {I : Type u_1} (ord : SemanticOrdering I) (a b c : I) : ord.le a b → ord.le b c → ord.le a c

theorem RudolphKocurek2024.SemanticOrdering.le_total {I : Type u_1} (ord : SemanticOrdering I) (a b : I) : ord.le a b ∨ ord.le b a

def RudolphKocurek2024.SemanticOrdering.lt {I : Type u_1} (ord : SemanticOrdering I) (a b : I) : Prop

The strict ordering ranks a strictly below b.

Equations

• ord.lt a b = (ord.le a b ∧ ¬ord.le b a)

@[instance_reducible]

instance RudolphKocurek2024.SemanticOrdering.decRelLt {I : Type u_1} (ord : SemanticOrdering I) [DecidableRel ord.le] : DecidableRel ord.lt

Equations

• ord.decRelLt x✝¹ x✝ = { decide := decide (ord.le x✝¹ x✝) && decide ¬ord.le x✝ x✝¹, reflects_decide := ⋯ }

theorem RudolphKocurek2024.SemanticOrdering.lt_of_le_of_lt {I : Type u_1} (ord : SemanticOrdering I) {a b c : I} (h : ord.le a b) (h' : ord.lt b c) : ord.lt a c

theorem RudolphKocurek2024.SemanticOrdering.lt_of_lt_of_le {I : Type u_1} (ord : SemanticOrdering I) {a b c : I} (h : ord.lt a b) (h' : ord.le b c) : ord.lt a c

theorem RudolphKocurek2024.SemanticOrdering.lt_irrefl {I : Type u_1} (ord : SemanticOrdering I) (a : I) : ¬ord.lt a a

theorem RudolphKocurek2024.SemanticOrdering.le_of_not_lt {I : Type u_1} (ord : SemanticOrdering I) {a b : I} (h : ¬ord.lt a b) : ord.le b a

If a is not strictly below b, then b is ranked no higher than a.

theorem RudolphKocurek2024.SemanticOrdering.exists_le_max {I : Type u_1} (ord : SemanticOrdering I) {S : Set I} (hS : S.Finite) (hne : S.Nonempty) : ∃ m ∈ S, ∀ s ∈ S, ord.le s m

Every nonempty finite set of interpretations has a top-ranked member.

@[reducible, inline]

abbrev RudolphKocurek2024.SemanticOrdering.equiv {I : Type u_1} (ord : SemanticOrdering I) (a b : I) : Prop

Two interpretations are equivalent when each is ranked no higher than the other.

Equations

• ord.equiv a b = AntisymmRel ord.le a b

@[instance_reducible]

instance RudolphKocurek2024.SemanticOrdering.decRelEquiv {I : Type u_1} (ord : SemanticOrdering I) [DecidableRel ord.le] : DecidableRel ord.equiv

Equations

• ord.decRelEquiv x✝¹ x✝ = { decide := decide (ord.le x✝¹ x✝) && decide (ord.le x✝ x✝¹), reflects_decide := ⋯ }

def RudolphKocurek2024.SemanticOrdering.ofRank {I : Type u_1} {α : Type u_2} [LinearOrder α] (r : I → α) : SemanticOrdering I

The semantic ordering that ranks interpretations by a map into a linear order, the convenient form for a concrete finite model.

Equations

• RudolphKocurek2024.SemanticOrdering.ofRank r = { le := fun (a b : I) => r a ≤ r b, isPreorder := ⋯, total := ⋯ }

@[instance_reducible]

instance RudolphKocurek2024.SemanticOrdering.instDecidableRelLeOfRank {I : Type u_1} {α : Type u_2} [LinearOrder α] (r : I → α) : DecidableRel (ofRank r).le

Equations

• RudolphKocurek2024.SemanticOrdering.instDecidableRelLeOfRank r a b = RudolphKocurek2024.SemanticOrdering.instDecidableRelLeOfRank._aux_1 r a b

def RudolphKocurek2024.SemanticOrdering.IsMaximal {I : Type u_1} (ord : SemanticOrdering I) (x : I) : Prop

An interpretation is top-ranked when none is ranked strictly above it.

Equations

• ord.IsMaximal x = ∀ (y : I), ¬ord.lt x y

@[instance_reducible]

instance RudolphKocurek2024.SemanticOrdering.instDecidableIsMaximalOfFintypeOfDecidableRelLe {I : Type u_1} (ord : SemanticOrdering I) [Fintype I] [DecidableRel ord.le] (x : I) : Decidable (ord.IsMaximal x)

Equations

• ord.instDecidableIsMaximalOfFintypeOfDecidableRelLe x = id inferInstance

def RudolphKocurek2024.SemanticOrdering.AcceptedAt {I : Type u_1} (ord : SemanticOrdering I) (A : I → Prop) : Prop

A predicate is accepted when it holds throughout the top-ranked interpretations.

Equations

• ord.AcceptedAt A = ∀ (x : I), ord.IsMaximal x → A x

@[instance_reducible]

instance RudolphKocurek2024.SemanticOrdering.instDecidableAcceptedAtOfFintypeOfDecidableRelLeOfDecidablePred {I : Type u_1} (ord : SemanticOrdering I) [Fintype I] [DecidableRel ord.le] (A : I → Prop) [DecidablePred A] : Decidable (ord.AcceptedAt A)

Equations

• ord.instDecidableAcceptedAtOfFintypeOfDecidableRelLeOfDecidablePred A = id inferInstance

The comparative language

def RudolphKocurek2024.ConeStrictLift {W : Type u_1} (le below : W → W → Prop) (P Q : W → Prop) (i : W) : Prop

The ∃∀ clause of Lewis's comparative possibility, localized to the cone below an index and comparing difference sets, which is the shape of Kratzer's revised lifting. The dominance relation is a parameter, so that the comparative is the clause at the strict ordering and much more is the clause at "far below".

Equations

• RudolphKocurek2024.ConeStrictLift le below P Q i = ∃ (a : W), le a i ∧ P a ∧ ¬Q a ∧ ∀ (b : W), le b i → Q b → ¬P b → below b a

@[instance_reducible]

instance RudolphKocurek2024.instDecidableConeStrictLiftOfFintypeOfDecidableRelOfDecidablePred {W : Type u_1} (le below : W → W → Prop) (P Q : W → Prop) (i : W) [Fintype W] [DecidableRel le] [DecidableRel below] [DecidablePred P] [DecidablePred Q] : Decidable (ConeStrictLift le below P Q i)

Equations

• RudolphKocurek2024.instDecidableConeStrictLiftOfFintypeOfDecidableRelOfDecidablePred le below P Q i = id inferInstance

def RudolphKocurek2024.coneDiff {W : Type u_1} (le : W → W → Prop) (P Q : W → Prop) (i : W) : Set W

The cone difference set at i consists of the members of the cone where P holds and Q fails.

Equations

• RudolphKocurek2024.coneDiff le P Q i = {x : W | le x i ∧ P x ∧ ¬Q x}

theorem RudolphKocurek2024.strict_lewisLift_iff_below {W : Type u_1} {ge_w below : W → W → Prop} (hTotal : ∀ (a b : W), ge_w a b ∨ ge_w b a) (hBelow : ∀ (a b : W), below a b ↔ ge_w b a ∧ ¬ge_w a b) (A B : Set W) : ComparativeProbability.Strict (ComparativeProbability.LewisLift ge_w) A B ↔ ∃ a ∈ A, ∀ b ∈ B, below b a

Whenever below is the strict form of the total ge_w, strict domination lifting is an ∃∀ clause in below.

theorem RudolphKocurek2024.coneStrictLift_iff_strict_lewisLift {W : Type u_1} {ge_w le below : W → W → Prop} (hTotal : ∀ (a b : W), ge_w a b ∨ ge_w b a) (hBelow : ∀ (a b : W), below a b ↔ ge_w b a ∧ ¬ge_w a b) (P Q : W → Prop) (i : W) : ConeStrictLift le below P Q i ↔ ComparativeProbability.Strict (ComparativeProbability.LewisLift ge_w) (coneDiff le P Q i) (coneDiff le Q P i)

Whenever below is the strict form of the total ge_w, the cone-localized clause is the strict domination lift on the cone difference sets.

def RudolphKocurek2024.RevisedComp {W : Type u_1} (le : W → W → Prop) (P Q : W → Prop) (i : W) : Prop

The revised comparative clause of the supplement. Some member of the cone below i makes P true and Q false, ranks strictly above every member making Q true and P false, and ranks strictly above either every member making both true or every member making both false.

Equations

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

def RudolphKocurek2024.RevisedEqui {W : Type u_1} (le : W → W → Prop) (P Q : W → Prop) (i : W) : Prop

The revised equative clause of the supplement. Either every member of the cone below i making exactly one of P and Q true is matched, at least as high, by one making only the other true, or every such member is matched, at least as high, both by one making both true and by one making both false.

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instDecidableRevisedCompOfFintypeOfDecidableRelOfDecidablePred {W : Type u_1} (le : W → W → Prop) (P Q : W → Prop) (i : W) [Fintype W] [DecidableRel le] [DecidablePred P] [DecidablePred Q] : Decidable (RevisedComp le P Q i)

Equations

• RudolphKocurek2024.instDecidableRevisedCompOfFintypeOfDecidableRelOfDecidablePred le P Q i = id inferInstance

theorem RudolphKocurek2024.revisedComp_iff {W : Type u_1} {le : W → W → Prop} {P Q : W → Prop} {i : W} : RevisedComp le P Q i ↔ ∃ (a : W), le a i ∧ P a ∧ ¬Q a ∧ ((∀ (b : W), le b i → Q b → ComparativeProbability.Strict le b a) ∨ ∀ (b : W), le b i → ¬P b → ComparativeProbability.Strict le b a)

The revised comparative simplifies: its witness ranks strictly above every member making Q true or above every member making P false.

theorem RudolphKocurek2024.coneStrictLift_iff_revisedComp {W : Type u_1} {le : W → W → Prop} {P Q : W → Prop} {i : W} : ConeStrictLift le (ComparativeProbability.Strict le) P Q i ↔ RevisedComp le (fun (a : W) => P a ∧ ¬Q a) (fun (a : W) => Q a ∧ ¬P a) i

The basic comparative is the revised comparative of the two difference sets.

theorem RudolphKocurek2024.revisedComp_iff_coneStrictLift {W : Type u_1} {le : W → W → Prop} {P Q : W → Prop} {i : W} : RevisedComp le P Q i ↔ ConeStrictLift le (ComparativeProbability.Strict le) (fun (a : W) => P a ∧ ¬Q a) (fun (a : W) => ¬P a) i ∨ ConeStrictLift le (ComparativeProbability.Strict le) (fun (a : W) => P a ∧ ¬Q a) Q i

The revised comparative is a disjunction of two basic comparatives, with the difference set P ∧ ¬Q compared against ¬P and against Q.

theorem RudolphKocurek2024.RevisedComp.congr {W : Type u_1} {le : W → W → Prop} {P Q : W → Prop} {i : W} {P' Q' : W → Prop} (hP : ∀ (a : W), le a i → (P a ↔ P' a)) (hQ : ∀ (a : W), le a i → (Q a ↔ Q' a)) : RevisedComp le P Q i ↔ RevisedComp le P' Q' i

The revised clauses at i read their arguments only on the cone below i.

theorem RudolphKocurek2024.RevisedEqui.congr {W : Type u_1} {le : W → W → Prop} {P Q : W → Prop} {i : W} {P' Q' : W → Prop} (hP : ∀ (a : W), le a i → (P a ↔ P' a)) (hQ : ∀ (a : W), le a i → (Q a ↔ Q' a)) : RevisedEqui le P Q i ↔ RevisedEqui le P' Q' i

theorem RudolphKocurek2024.not_revisedComp_self {W : Type u_1} {le : W → W → Prop} {P : W → Prop} {i : W} : ¬RevisedComp le P P i

theorem RudolphKocurek2024.RevisedEqui.refl {W : Type u_1} {le : W → W → Prop} {P : W → Prop} {i : W} : RevisedEqui le P P i

theorem RudolphKocurek2024.RevisedEqui.symm {W : Type u_1} {le : W → W → Prop} {P Q : W → Prop} {i : W} (h : RevisedEqui le P Q i) : RevisedEqui le Q P i

theorem RudolphKocurek2024.RevisedEqui.not_revisedComp {W : Type u_1} {le : W → W → Prop} {P Q : W → Prop} {i : W} (h : RevisedEqui le P Q i) : ¬RevisedComp le P Q i

The revised equative excludes the revised comparative.

theorem RudolphKocurek2024.RevisedComp.trans {W : Type u_1} {P Q : W → Prop} {i : W} {ord : SemanticOrdering W} {R : W → Prop} (h₁ : RevisedComp ord.le P Q i) (h₂ : RevisedComp ord.le Q R i) : RevisedComp ord.le P R i

The revised comparative is transitive, the supplement's Fact 4: whichever witness ranks higher witnesses the composite.

theorem RudolphKocurek2024.RevisedComp.of_revisedEqui_right {W : Type u_1} {P Q : W → Prop} {i : W} {ord : SemanticOrdering W} {R : W → Prop} (h : RevisedComp ord.le P Q i) (hQR : RevisedEqui ord.le Q R i) : RevisedComp ord.le P R i

The revised comparative respects the revised equative on the right, the supplement's Fact 11.

theorem RudolphKocurek2024.RevisedComp.of_revisedEqui_left {W : Type u_1} {P Q : W → Prop} {i : W} {ord : SemanticOrdering W} {R : W → Prop} (h : RevisedComp ord.le P Q i) (hPR : RevisedEqui ord.le P R i) : RevisedComp ord.le R Q i

theorem RudolphKocurek2024.revisedEqui_or_revisedComp_or_revisedComp {W : Type u_1} [Finite W] (ord : SemanticOrdering W) (P Q : W → Prop) (i : W) : RevisedEqui ord.le P Q i ∨ RevisedComp ord.le P Q i ∨ RevisedComp ord.le Q P i

Over finitely many interpretations, two predicates are revised-equal or one is revised-more than the other.

theorem RudolphKocurek2024.RevisedEqui.trans {W : Type u_1} {P Q : W → Prop} {i : W} {ord : SemanticOrdering W} {R : W → Prop} [Finite W] (h₁ : RevisedEqui ord.le P Q i) (h₂ : RevisedEqui ord.le Q R i) : RevisedEqui ord.le P R i

The revised equative is transitive, the supplement's Fact 6.

def RudolphKocurek2024.ext₁ {L : FirstOrder.Language} {E : Type u_3} (S : L.Structure E) (R : L.Relations 1) : Set E

The extension of a unary relation symbol in a structure carried as a term.

Equations

• RudolphKocurek2024.ext₁ S R = {e : E | FirstOrder.Language.Structure.RelMap R ![e]}

@[simp]

theorem RudolphKocurek2024.mem_ext₁ {L : FirstOrder.Language} {E : Type u_3} {S : L.Structure E} {R : L.Relations 1} {e : E} : e ∈ ext₁ S R ↔ FirstOrder.Language.Structure.RelMap R ![e]

@[instance_reducible]

instance RudolphKocurek2024.instDecidableMemSetExt₁OfRelMapVecConsVecEmpty {L : FirstOrder.Language} {E : Type u_3} (S : L.Structure E) (R : L.Relations 1) (e : E) [h : Decidable (FirstOrder.Language.Structure.RelMap R ![e])] : Decidable (e ∈ ext₁ S R)

Equations

• RudolphKocurek2024.instDecidableMemSetExt₁OfRelMapVecConsVecEmpty S R e = h

@[reducible, inline]

abbrev RudolphKocurek2024.DecidableAtoms {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) : Type (max (max (max u_1 u_2) u_3) u_5)

Pointwise decidability of atoms across an interpretation family, the hook that makes decide available on finite models.

Equations

• RudolphKocurek2024.DecidableAtoms interp = ((i : I) → (w : W) → (n : ℕ) → (r : L.Relations n) → (x : Fin n → E) → Decidable (FirstOrder.Language.Structure.RelMap r x))

inductive RudolphKocurek2024.ComparativeFormula (L : FirstOrder.Language) (E : Type u_4) : Type (max (max u_4 u_5) u_6)

A formula is an embedded classical formula with free variables valued by domain elements, a boolean combination, or a comparative A ≻ B (comp).

• ofFormula {L : FirstOrder.Language} {E : Type u_4} : L.Formula E → ComparativeFormula L E
• not {L : FirstOrder.Language} {E : Type u_4} : ComparativeFormula L E → ComparativeFormula L E
• inf {L : FirstOrder.Language} {E : Type u_4} : ComparativeFormula L E → ComparativeFormula L E → ComparativeFormula L E
• sup {L : FirstOrder.Language} {E : Type u_4} : ComparativeFormula L E → ComparativeFormula L E → ComparativeFormula L E
• comp {L : FirstOrder.Language} {E : Type u_4} : ComparativeFormula L E → ComparativeFormula L E → ComparativeFormula L E

@[reducible, inline]

abbrev RudolphKocurek2024.ComparativeFormula.matom {L : FirstOrder.Language} {E : Type u_3} (R : L.Relations 1) (e : E) : ComparativeFormula L E

Ground unary predication R(e), as an embedded formula.

Equations

• RudolphKocurek2024.ComparativeFormula.matom R e = RudolphKocurek2024.ComparativeFormula.ofFormula (R.formula₁ (FirstOrder.Language.var e))

def RudolphKocurek2024.ComparativeFormula.equi {L : FirstOrder.Language} {E : Type u_3} (A B : ComparativeFormula L E) : ComparativeFormula L E

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

Equations

• A.equi B = (A.comp B).not.inf (B.comp A).not

def RudolphKocurek2024.ComparativeFormula.weak {L : FirstOrder.Language} {E : Type u_3} (A B : ComparativeFormula L E) : ComparativeFormula L E

The weak comparative A ≽ B := (A ≻ B) ∨ (A ≈ B).

Equations

• A.weak B = (A.comp B).sup (A.equi B)

def RudolphKocurek2024.ComparativeFormula.ComparativeFree {L : FirstOrder.Language} {E : Type u_3} : ComparativeFormula L E → Prop

Formulas free of the comparative, whose truth does not consult the ordering.

Equations

• (RudolphKocurek2024.ComparativeFormula.ofFormula a).ComparativeFree = True
• A.not.ComparativeFree = A.ComparativeFree
• (A.inf B).ComparativeFree = (A.ComparativeFree ∧ B.ComparativeFree)
• (A.sup B).ComparativeFree = (A.ComparativeFree ∧ B.ComparativeFree)
• (a.comp a_1).ComparativeFree = False

def RudolphKocurek2024.ComparativeFormula.Realize {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) : ComparativeFormula L E → (I → I → Prop) → I → W → Prop

Truth at an index of an ordered interpretation family, relative to a raw ordering relation, since restricted orderings need not be total. The comparative holds when some interpretation in the cone making A true and B false strictly dominates every one making B true and A false.

Equations

• One or more equations did not get rendered due to their size.
• RudolphKocurek2024.ComparativeFormula.Realize interp (RudolphKocurek2024.ComparativeFormula.ofFormula ψ) x✝² x✝¹ x✝ = ψ.RealizeAt (interp x✝¹) x✝ id
• RudolphKocurek2024.ComparativeFormula.Realize interp A.not x✝² x✝¹ x✝ = ¬RudolphKocurek2024.ComparativeFormula.Realize interp A x✝² x✝¹ x✝

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.
• RudolphKocurek2024.ComparativeFormula.instDec interp le (RudolphKocurek2024.ComparativeFormula.ofFormula ψ) x✝¹ x✝ = ψ.decidableRealize id
• RudolphKocurek2024.ComparativeFormula.instDec interp le A.not x✝¹ x✝ = instDecidableNot
• RudolphKocurek2024.ComparativeFormula.instDec interp le (A.inf B) x✝¹ x✝ = instDecidableAnd
• RudolphKocurek2024.ComparativeFormula.instDec interp le (A.sup B) x✝¹ x✝ = instDecidableOr

theorem RudolphKocurek2024.ComparativeFormula.realize_comp_iff {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {A B : ComparativeFormula L E} {ord : SemanticOrdering I} {i : I} {w : W} : Realize interp (A.comp B) ord.le i w ↔ ∃ (i' : I), ord.le i' i ∧ Realize interp A ord.le i' w ∧ ¬Realize interp B ord.le i' w ∧ ∀ (i'' : I), ord.le i'' i → Realize interp B ord.le i'' w → ¬Realize interp A ord.le i'' w → ord.lt i'' i'

The comparative clause over a total preorder, with the domination conjunction packaged as ord.lt.

@[simp]

theorem RudolphKocurek2024.ComparativeFormula.realize_matom {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {le : I → I → Prop} {i : I} {w : W} (R : L.Relations 1) (e : E) : Realize interp (matom R e) le i w ↔ FirstOrder.Language.Structure.RelMap R ![e]

Realization of a ground unary atom.

theorem RudolphKocurek2024.ComparativeFormula.ComparativeFree.realize_congr {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {φ : ComparativeFormula L E} : φ.ComparativeFree → ∀ {le le' : I → I → Prop} {i : I} {w : W}, Realize interp φ le i w ↔ Realize interp φ le' i w

Comparative-free formulas are ordering-invariant.

theorem RudolphKocurek2024.ComparativeFormula.realize_comp_iff_strict_lewisLift {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {A B : ComparativeFormula L E} {ord : SemanticOrdering I} {i : I} {w : W} : Realize interp (A.comp B) ord.le i w ↔ ComparativeProbability.Strict (ComparativeProbability.LewisLift (flip ord.le)) (coneDiff ord.le (fun (x : I) => Realize interp A ord.le x w) (fun (x : I) => Realize interp B ord.le x w) i) (coneDiff ord.le (fun (x : I) => Realize interp B ord.le x w) (fun (x : I) => Realize interp A ord.le x w) i)

The comparative is the strict domination lift of Holliday and Icard, Lewis's lifting, applied to the cone at the evaluation index.

theorem RudolphKocurek2024.ComparativeFormula.not_realize_comp_self {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {A : ComparativeFormula L E} {le : I → I → Prop} {i : I} {w : W} : ¬Realize interp (A.comp A) le i w

The comparative is irreflexive, since a witness would make A both true and false.

theorem RudolphKocurek2024.ComparativeFormula.realize_equi_self {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {A : ComparativeFormula L E} {le : I → I → Prop} {i : I} {w : W} : Realize interp (A.equi A) le i w

The equative is reflexive.

theorem RudolphKocurek2024.ComparativeFormula.realize_equi_comm {W : Type u_1} {L : FirstOrder.Language} {I : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {A B : ComparativeFormula L E} {le : I → I → Prop} {i : I} {w : W} : Realize interp (A.equi B) le i w ↔ Realize interp (B.equi A) le i w

The equative is symmetric.

Truth and acceptance

@[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) (φ : ComparativeFormula L E) (ord : SemanticOrdering I) (i : I) (w : W) : Prop

Truth at an index ⟨≤, i, w⟩.

Equations

• RudolphKocurek2024.Eval interp φ ord i w = RudolphKocurek2024.ComparativeFormula.Realize interp φ ord.le i w

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] (φ : ComparativeFormula L E) (ord : SemanticOrdering I) (w : W) : Prop

The assertoric content of a sentence is its truth at every top-ranked interpretation.

Equations

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

@[instance_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] [DecidableAtoms interp] (φ : ComparativeFormula L E) (ord : SemanticOrdering I) [DecidableRel ord.le] (w : W) : Decidable (AssertoricContent interp φ ord w)

Equations

• RudolphKocurek2024.instDecidableAssertoricContentOfFintypeOfDecidableEqOfDecidableAtomsOfDecidableRelLe interp φ ord w = id inferInstance

Entailment

theorem RudolphKocurek2024.eval_of_comp {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {i : I} {w : W} {A B : ComparativeFormula L E} (h : Eval interp (A.comp B) ord i w) (hB : Eval interp B ord i w) : Eval interp A ord i w

The comparative with its right constituent entails the left, since an interpretation making B true and A false would have to lie strictly below one ranked no higher than itself.

theorem RudolphKocurek2024.comp_asymm {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {i : I} {w : W} {A B : ComparativeFormula L E} (h : Eval interp (A.comp B) ord i w) : ¬Eval interp (B.comp A) ord i w

The comparative is asymmetric.

theorem RudolphKocurek2024.comp_trans {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {i : I} {w : W} {A B C : ComparativeFormula L E} (h₁ : Eval interp (A.comp B) ord i w) (h₂ : Eval interp (B.comp C) ord i w) : Eval interp (A.comp C) ord i w

The comparative is transitive, since whichever of the two witnesses is ranked higher witnesses the composite, and the two domination clauses cover the rivals of the composite.

theorem RudolphKocurek2024.comp_not_not_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} {i : I} {w : W} {A B : ComparativeFormula L E} : Eval interp (B.not.comp A.not) ord i w ↔ Eval interp (A.comp B) ord i w

The comparative contraposes.

theorem RudolphKocurek2024.comp_sup {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {i : I} {w : W} {A B C : ComparativeFormula L E} (h : Eval interp (A.comp (B.sup C)) ord i w) : Eval interp (A.comp B) ord i w ∧ Eval interp (A.comp C) ord i w

The comparative distributes over a disjunction on the right.

theorem RudolphKocurek2024.inf_comp {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {i : I} {w : W} {A B C : ComparativeFormula L E} (h : Eval interp ((A.inf B).comp C) ord i w) : Eval interp (A.comp C) ord i w ∧ Eval interp (B.comp C) ord i w

The comparative distributes over a conjunction on the left.

theorem RudolphKocurek2024.equi_not_not {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {i : I} {w : W} {A B : ComparativeFormula L E} (h : Eval interp (A.equi B) ord i w) : Eval interp (A.not.equi B.not) ord i w

The equative is preserved by negating both sides.

theorem RudolphKocurek2024.eval_weak_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} {i : I} {w : W} {A B : ComparativeFormula L E} : Eval interp (A.weak B) ord i w ↔ ¬Eval interp (B.comp A) ord i w

The weak comparative is the negation of the converse comparative.

theorem RudolphKocurek2024.eval_comp_or_equi {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {i : I} {w : W} {A B : ComparativeFormula L E} : Eval interp (((A.comp B).sup (B.comp A)).sup (A.equi B)) ord i w

Any two sentences are comparable, so one is more than the other or they are equal.

theorem RudolphKocurek2024.eval_comp_not_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} {i : I} {w : W} {A : ComparativeFormula L E} : Eval interp (A.comp A.not) ord i w ↔ ∀ (j : I), ord.equiv j i → Eval interp A ord j w

More A than not, the supplement's ⊟A, holds at an index iff A holds at every interpretation tied with it (the supplement's Fact 1), so at a top-ranked index it says that A is accepted.

theorem RudolphKocurek2024.accepted_mono {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {w : W} {A B : ComparativeFormula L E} [Fintype I] (h : ∀ (i : I), Eval interp A ord i w → Eval interp B ord i w) (hA : AssertoricContent interp A ord w) : AssertoricContent interp B ord w

Truth preservation implies acceptance preservation.

theorem RudolphKocurek2024.accepted_comp_of_accepted {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {w : W} {A B : ComparativeFormula L E} [Fintype I] (hA : AssertoricContent interp A ord w) (hB : AssertoricContent interp B.not ord w) : AssertoricContent interp (A.comp B) ord w

Accepting A and ¬B means accepting A ≻ B. Every top-ranked interpretation makes A true and B false, so an interpretation making B true and A false is not top-ranked and lies strictly below each of them.

theorem RudolphKocurek2024.accepted_of_accepted_equi {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} {w : W} {A B : ComparativeFormula L E} [Fintype I] (h : AssertoricContent interp (A.equi B) ord w) (hA : AssertoricContent interp A ord w) : AssertoricContent interp B ord w

Accepting A ≈ B and A means accepting B.

Distance functions and degree modifiers

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

A distance function says which interpretations count as reasonably close to each one. It is the parameter behind very, sorta and mostly.

• close : I → I → Prop

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

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

  The function is centered, so i ∈ d(i).

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

  The function is top-bounded, so 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''

  The function is convex, so 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'

  The function is noncontractive, so 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 holds when 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)

@[instance_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✝ = { decide := decide (ord.le x✝¹ x✝) && decide ¬d.close x✝ x✝¹, reflects_decide := ⋯ }

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

The relation ≪ is asymmetric, since centeredness and noncontractivity force points related by ≤ in both directions 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

The relation "not far below" is total, which 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) (φ ψ : ComparativeFormula L E) (ord : SemanticOrdering I) (below : I → I → Prop) (i : I) (w : W) : Prop

The paper's comparative template is ConeStrictLift at the truth sets of the formulas. It is the clause of ≻ with an arbitrary dominance relation in place of < (eval_comp_iff_compWith), and ≫ 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) (φ ψ : ComparativeFormula L E) (ord : SemanticOrdering I) (i : I) (w : W) : Eval interp (φ.comp ψ) ord i w ↔ EvalCompWith interp φ ψ ord ord.lt 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) (φ ψ : ComparativeFormula L E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Prop

Much more, A ≫ B, is 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) (φ : ComparativeFormula L E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Prop

very A is A ≫ ¬A, under which 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) (φ : ComparativeFormula L E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Prop

sorta A is ¬ very ¬A, under which 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) (φ : ComparativeFormula L E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : Prop

Mostly A holds when some reasonably high level strictly below the top makes A uniformly true and every A-false level below the current interpretation sits below it. It is compatible with A and with ¬A, unlike very, entails sorta A, and mostly A ∧ mostly ¬A is contradictory.

Equations

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

@[instance_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) (φ : ComparativeFormula L E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) [Fintype I] [Fintype E] [DecidableEq E] [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_lewisLift {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (φ ψ : ComparativeFormula L E) (ord : SemanticOrdering I) (d : DistanceFunction I ord) (i : I) (w : W) : EvalMuchMore interp φ ψ ord d i w ↔ ComparativeProbability.Strict (ComparativeProbability.LewisLift fun (a b : I) => ¬FarBelow ord d a b) (coneDiff ord.le (fun (x : I) => Eval interp φ ord x w) (fun (x : I) => Eval interp ψ ord x w) i) (coneDiff ord.le (fun (x : I) => Eval interp ψ ord x w) (fun (x : I) => Eval interp φ ord x w) i)

≫ is the strict l-lifting under the coarser total preorder "not far below". The axioms on the distance function are exactly what make that relation total, so the lift of Holliday and Icard applies with ≪ in the role of <.

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

mostly is the strict l-lifting comparing levels that are uniform for φ, the classes of ord.equiv, mathlib's AntisymmRel.setoid. Some reasonably high level where φ holds throughout, strictly below the index, dominates every level below it where φ fails throughout.

theorem RudolphKocurek2024.evalVery_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} (d : DistanceFunction I ord) {i : I} {w : W} {φ : ComparativeFormula L E} : EvalVery interp φ ord d i w ↔ ∀ (i' : I), d.close i i' → Eval interp φ ord i' w

very A is truth at every reasonably close interpretation, since a witness strictly above a close falsifier would, by noncontractivity, have it close too.

theorem RudolphKocurek2024.eval_of_very {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} (d : DistanceFunction I ord) {i : I} {w : W} {φ : ComparativeFormula L E} (h : EvalVery interp φ ord d i w) : Eval interp φ ord i w

very A entails A, since every interpretation is close to itself.

theorem RudolphKocurek2024.evalSorta_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} (d : DistanceFunction I ord) {i : I} {w : W} {φ : ComparativeFormula L E} : EvalSorta interp φ ord d i w ↔ ∃ (i' : I), d.close i i' ∧ Eval interp φ ord i' w

sorta A is truth at some reasonably close interpretation.

theorem RudolphKocurek2024.sorta_of_eval {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} (d : DistanceFunction I ord) {i : I} {w : W} {φ : ComparativeFormula L E} (h : Eval interp φ ord i w) : EvalSorta interp φ ord d i w

A entails sorta A.

theorem RudolphKocurek2024.sorta_of_mostly {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} (d : DistanceFunction I ord) {i : I} {w : W} {φ : ComparativeFormula L E} (h : EvalMostly interp φ ord d i w) : EvalSorta interp φ ord d i w

mostly A entails sorta A.

theorem RudolphKocurek2024.not_mostly_not_of_mostly {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {ord : SemanticOrdering I} (d : DistanceFunction I ord) {i : I} {w : W} {φ : ComparativeFormula L E} (h : EvalMostly interp φ ord d i w) : ¬EvalMostly interp φ.not ord d i w

mostly A and mostly ¬A are contradictory, since each witness level would lie strictly below the other.

No Reversal and the delineation bridge

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 says that below any interpretation separating a from b, every extension admitting b admits a. It is the order-restricted analogue of Klein's monotone delineation.

Equations

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

@[instance_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] [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) : Degree.Delineation E

The delineation induced by a ranked interpretation family takes the extensions of R in the ≤-cone as the admissible comparison classes, and x is R in C iff x ∈ C. It instantiates Klein's comparison-class parameter.

Equations

• RudolphKocurek2024.interpretationDelineation interp ord R w i = { toFun := fun (C : Set E) => {x : E | (∃ (i' : I), ord.le i' i ∧ C = RudolphKocurek2024.ext₁ (interp i' w) R) ∧ x ∈ C} }

theorem RudolphKocurek2024.delineation_comparative_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) : (interpretationDelineation interp ord R w i).Comparative a b ↔ ∃ (i' : I), ord.le i' i ∧ a ∈ ext₁ (interp i' w) R ∧ b ∉ ext₁ (interp i' w) R

The delineation comparative over the induced delineation is the existential witness clause of the metalinguistic comparative, under which 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 ((ComparativeFormula.matom R a).comp (ComparativeFormula.matom R b)) ord i w ↔ (interpretationDelineation interp ord R w i).Comparative a b

Under No Reversal, the metalinguistic comparative for a gradable predicate is Klein's delineation comparative (Delineation.Comparative) over the delineation that the interpretations induce, since No Reversal makes the domination clause of the comparative redundant.

The revised semantics

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

Truth under the revised semantics of the supplement, whose comparative is RevisedComp. The basic equative fails transitivity, and the revision strengthens the comparative so that the equative it defines is transitive.

Equations

• One or more equations did not get rendered due to their size.
• RudolphKocurek2024.EvalRevised interp (RudolphKocurek2024.ComparativeFormula.ofFormula ψ) x✝² x✝¹ x✝ = ψ.RealizeAt (interp x✝¹) x✝ id
• RudolphKocurek2024.EvalRevised interp A.not x✝² x✝¹ x✝ = ¬RudolphKocurek2024.EvalRevised interp A x✝² x✝¹ x✝
• RudolphKocurek2024.EvalRevised interp (A.inf B) x✝² x✝¹ x✝ = (RudolphKocurek2024.EvalRevised interp A x✝² x✝¹ x✝ ∧ RudolphKocurek2024.EvalRevised interp B x✝² x✝¹ x✝)
• RudolphKocurek2024.EvalRevised interp (A.sup B) x✝² x✝¹ x✝ = (RudolphKocurek2024.EvalRevised interp A x✝² x✝¹ x✝ ∨ RudolphKocurek2024.EvalRevised interp B x✝² x✝¹ x✝)

@[instance_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 : DecidableAtoms interp] (ord : SemanticOrdering I) [DecidableRel ord.le] (φ : ComparativeFormula L E) (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 ord (RudolphKocurek2024.ComparativeFormula.ofFormula ψ) x✝¹ x✝ = ψ.decidableRealize id
• RudolphKocurek2024.EvalRevised.instDec interp ord A.not x✝¹ x✝ = instDecidableNot
• RudolphKocurek2024.EvalRevised.instDec interp ord (A.inf B) x✝¹ x✝ = instDecidableAnd
• RudolphKocurek2024.EvalRevised.instDec interp ord (A.sup B) x✝¹ x✝ = instDecidableOr

theorem RudolphKocurek2024.evalRevised_comp_trans {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {A B C : ComparativeFormula L E} {ord : SemanticOrdering I} {i : I} {w : W} (h₁ : EvalRevised interp (A.comp B) ord i w) (h₂ : EvalRevised interp (B.comp C) ord i w) : EvalRevised interp (A.comp C) ord i w

The revised comparative is transitive.

theorem RudolphKocurek2024.evalRevised_equi_iff {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {A B : ComparativeFormula L E} {ord : SemanticOrdering I} {i : I} {w : W} [Finite I] : EvalRevised interp (A.equi B) ord i w ↔ RevisedEqui ord.le (fun (x : I) => EvalRevised interp A ord x w) (fun (x : I) => EvalRevised interp B ord x w) i

The equative ¬(A ≻ B) ∧ ¬(B ≻ A) of the revised semantics is the supplement's revised equative clause.

theorem RudolphKocurek2024.evalRevised_equi_trans {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) {A B C : ComparativeFormula L E} {ord : SemanticOrdering I} {i : I} {w : W} [Finite I] (h₁ : EvalRevised interp (A.equi B) ord i w) (h₂ : EvalRevised interp (B.equi C) ord i w) : EvalRevised interp (A.equi C) ord i w

The revised equative is transitive, unlike the basic one (equi_not_trans).

The metalinguistic conditional

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 : ComparativeFormula L E) (le : I → I → Prop) (w : W) : I → I → Prop

The restriction of an ordering relation to the A-interpretations drops the other interpretations. The result is reflexive at A-interpretations and transitive but not total, which is why the consequent of a conditional is evaluated through EvalGen and not Eval.

Equations

• RudolphKocurek2024.restrictLE interp A le w i j = (le i j ∧ RudolphKocurek2024.ComparativeFormula.Realize interp A le i w ∧ RudolphKocurek2024.ComparativeFormula.Realize interp A le j w)

@[instance_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) (A : ComparativeFormula L E) [Fintype I] [Fintype E] [DecidableEq E] [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 : ComparativeFormula L E) (ord : SemanticOrdering I) (i : I) (w : W) : Prop

The metalinguistic conditional evaluates the antecedent with the full ordering and the consequent with the ordering restricted to A. For A and B that are not metagradable it reduces to strict implication over interpretations. Conditionals entail weak comparatives, A → (A ≻ ¬A) is valid (mcond_m1), and modus tollens fails for acceptance.

Equations

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

@[instance_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) (A B : ComparativeFormula L E) (ord : SemanticOrdering I) (i : I) (w : W) [Fintype I] [Fintype E] [DecidableEq E] [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 : ComparativeFormula L E) (ord : SemanticOrdering I) (i : I) (w : W) (hB : B.ComparativeFree) : EvalMCond interp A B ord i w ↔ {x : I | ord.le x i ∧ ComparativeFormula.Realize interp A ord.le x w} ⊆ {x : I | ComparativeFormula.Realize interp B ord.le x w}

For a consequent free of the comparative, the metalinguistic conditional is Stalnakerian entailment (⊆) of the consequent by the ranked cone of the antecedent. This is strictly weaker than the paper's reduction, which also assumes the antecedent free of the comparative. The antecedent may contain ≻ freely, since it is always evaluated at the full ordering and a consequent free of the comparative never consults the restricted one.

theorem RudolphKocurek2024.weak_of_mcond {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A B : ComparativeFormula L E) (ord : SemanticOrdering I) (i : I) (w : W) (hB : B.ComparativeFree) (h : EvalMCond interp A B ord i w) : Eval interp (B.weak A) ord i w

A conditional with a consequent free of the comparative conveys the weak comparative, since every ranked interpretation of the antecedent makes the consequent true, so none witnesses A ≻ B.

theorem RudolphKocurek2024.comp_of_mcond_sup {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A B : ComparativeFormula L E) (ord : SemanticOrdering I) (i : I) (w : W) (hA : A.ComparativeFree) (hB : B.ComparativeFree) (h₁ : EvalMCond interp (A.sup B) A ord i w) (h₂ : ¬EvalMCond interp (A.sup B) B ord i w) : Eval interp (A.comp B) ord i w

If A or B, then A, but not if A or B, then B, conveys the strict comparative A ≻ B for constituents free of the comparative. The failure of the second conditional is a ranked witness for A and against B, and the first leaves it no rival.

theorem RudolphKocurek2024.mcond_comp_not {L : FirstOrder.Language} {I : Type u_1} {W : Type u_2} {E : Type u_3} (interp : I → W → L.Structure E) (A : ComparativeFormula L E) (ord : SemanticOrdering I) (i : I) (w : W) (hA : A.ComparativeFree) : EvalMCond interp A (A.comp A.not) ord i w

If A, then more A than not is valid for A free of the comparative, since under the restricted ordering every ranked interpretation makes A true, so the rival set of the consequent is empty.

The common ground

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

The proposition that a sentence expresses over the enriched index consists of the pairs of an ordering and a world at which its assertoric content holds. The common ground is a set of such pairs, and an assertion removes the pairs outside this proposition.

Equations

• RudolphKocurek2024.assertoricProp interp φ = {p : RudolphKocurek2024.SemanticOrdering I × W | RudolphKocurek2024.AssertoricContent interp φ p.1 p.2}

Metalinguistic degrees

The supplement's degree theory. Its equivalence X ∼ Y and ordering X ⊐ Y of sets of interpretations are the revised equative and comparative of their membership predicates, so the degree of a formula is the ∼-class of its denotation and the comparative compares degrees.

def RudolphKocurek2024.metalinguisticSetoid {I : Type u_1} (ord : SemanticOrdering I) (i : I) [Finite I] : Setoid (Set I)

The equivalence X ∼ Y of sets of interpretations ranked no higher than i, an equivalence relation by the supplement's Fact 8.

Equations

• RudolphKocurek2024.metalinguisticSetoid ord i = { r := fun (X Y : Set I) => RudolphKocurek2024.RevisedEqui ord.le (fun (x : I) => x ∈ X) (fun (x : I) => x ∈ Y) i, iseqv := ⋯ }

def RudolphKocurek2024.MetaDegree {I : Type u_1} (ord : SemanticOrdering I) (i : I) [Finite I] : Type u_1

Metalinguistic degrees at i are the ∼-classes of sets of interpretations.

Equations

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

def RudolphKocurek2024.deg {I : Type u_1} (ord : SemanticOrdering I) (i : I) [Finite I] (X : Set I) : MetaDegree ord i

The metalinguistic degree of a set of interpretations.

Equations

• RudolphKocurek2024.deg ord i X = ⟦X⟧

theorem RudolphKocurek2024.deg_eq_deg_iff {I : Type u_1} (ord : SemanticOrdering I) (i : I) [Finite I] {X Y : Set I} : deg ord i X = deg ord i Y ↔ RevisedEqui ord.le (fun (x : I) => x ∈ X) (fun (x : I) => x ∈ Y) i

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

deg X ≤ deg Y iff X ⊐ Y fails, well defined since ⊐ respects ∼ on both sides.

Equations

• RudolphKocurek2024.MetaDegree.le ord i d₁ d₂ = Quotient.lift₂ (fun (X Y : Set I) => ¬RudolphKocurek2024.RevisedComp ord.le (fun (x : I) => x ∈ X) (fun (x : I) => x ∈ Y) i) ⋯ d₁ d₂

@[instance_reducible]

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

The degrees form a linear order, the supplement's Fact 12: irreflexivity, transitivity and trichotomy of ⊐ become the order axioms on the quotient.

Equations

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

@[instance_reducible]

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

The top degree is that of the cone I_i and the bottom degree that of ∅, the supplement's Fact 13.

Equations

• RudolphKocurek2024.instBoundedOrderMetaDegree ord i = { top := RudolphKocurek2024.deg ord i {j : I | ord.le j i}, le_top := ⋯, bot := RudolphKocurek2024.deg ord i ∅, bot_le := ⋯ }

@[simp]

theorem RudolphKocurek2024.deg_le_deg_iff {I : Type u_1} (ord : SemanticOrdering I) (i : I) [Finite I] {X Y : Set I} : deg ord i X ≤ deg ord i Y ↔ ¬RevisedComp ord.le (fun (x : I) => x ∈ X) (fun (x : I) => x ∈ Y) i

theorem RudolphKocurek2024.deg_lt_deg_iff {I : Type u_1} (ord : SemanticOrdering I) (i : I) [Finite I] {X Y : Set I} : deg ord i Y < deg ord i X ↔ RevisedComp ord.le (fun (x : I) => x ∈ X) (fun (x : I) => x ∈ Y) i

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

The denotation ⟦φ⟧ᵢ of a formula, the interpretations ranked no higher than i at which it is true under the revised semantics.

Equations

• RudolphKocurek2024.denotation ord i interp φ w = {j : I | ord.le j i ∧ RudolphKocurek2024.EvalRevised interp φ ord j w}

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

The metalinguistic degree of a formula is the degree of its denotation.

Equations

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

theorem RudolphKocurek2024.evalRevised_comp_iff_denotation {I : Type u_1} {ord : SemanticOrdering I} {i : I} {L : FirstOrder.Language} {W : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {A B : ComparativeFormula L E} {w : W} : EvalRevised interp (A.comp B) ord i w ↔ RevisedComp ord.le (fun (x : I) => x ∈ denotation ord i interp A w) (fun (x : I) => x ∈ denotation ord i interp B w) i

The revised comparative compares the denotations, the supplement's Fact 10.

theorem RudolphKocurek2024.evalRevised_equi_iff_formulaDeg_eq {I : Type u_1} {ord : SemanticOrdering I} {i : I} {L : FirstOrder.Language} {W : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {A B : ComparativeFormula L E} {w : W} [Finite I] : EvalRevised interp (A.equi B) ord i w ↔ formulaDeg ord i interp A w = formulaDeg ord i interp B w

The revised equative holds iff the two formulas have the same degree, the supplement's Fact 9.

theorem RudolphKocurek2024.mc_iff_formulaDeg_lt {I : Type u_1} {ord : SemanticOrdering I} {i : I} {L : FirstOrder.Language} {W : Type u_2} {E : Type u_3} {interp : I → W → L.Structure E} {A B : ComparativeFormula L E} {w : W} [Finite I] : EvalRevised interp (A.comp B) ord i w ↔ formulaDeg ord i interp B w < formulaDeg ord i interp A w

The revised metalinguistic comparative is the point-standard comparative of degree semantics over the metalinguistic measure function formulaDeg, which is the paper's (59). Metagradability thereby instantiates the central object of degree semantics, a measure μ : E → D into a bounded linear scale, with the formulas as E and the MetaDegree scale as D.

Finite models

inductive RudolphKocurek2024.W : Type

One world.

• w0 : W

@[instance_reducible]

instance RudolphKocurek2024.instDecidableEqW : DecidableEq W

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instReprW : Repr W

Equations

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

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✝

@[instance_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.Entity : Type

The model has one entity, Ann.

• ann : Entity

@[instance_reducible]

instance RudolphKocurek2024.instDecidableEqEntity : DecidableEq Entity

Equations

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

@[instance_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.

@[instance_reducible]

instance RudolphKocurek2024.instFintypeEntity : Fintype Entity

Equations

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

inductive RudolphKocurek2024.I3 : Type

Three interpretations.

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

@[instance_reducible]

instance RudolphKocurek2024.instDecidableEqI3 : DecidableEq I3

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instReprI3 : Repr I3

Equations

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

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✝

@[instance_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.rank₃ : I3 → ℕ

The rank of each of the three interpretations.

Equations

• RudolphKocurek2024.rank₃ RudolphKocurek2024.I3.i0 = 0
• RudolphKocurek2024.rank₃ RudolphKocurek2024.I3.i1 = 1
• RudolphKocurek2024.rank₃ RudolphKocurek2024.I3.i2 = 2

def RudolphKocurek2024.ord₃ : SemanticOrdering I3

The linear ordering i0 < i1 < i2.

Equations

• RudolphKocurek2024.ord₃ = RudolphKocurek2024.SemanticOrdering.ofRank RudolphKocurek2024.rank₃

@[instance_reducible]

instance RudolphKocurek2024.instDecidableRelI3LeOrd₃ : DecidableRel ord₃.le

Equations

• RudolphKocurek2024.instDecidableRelI3LeOrd₃ = RudolphKocurek2024.instDecidableRelI3LeOrd₃._aux_1

@[instance_reducible]

def RudolphKocurek2024.interpOf {Sym : Type u_1} {I : Type u_2} {E : Type u_3} (ext : I → Sym → Finset E) : I → W → (FirstOrder.Language.monadic Sym).Structure E

An interpretation family over a monadic language, from the extension of each predicate at each interpretation.

Equations

• RudolphKocurek2024.interpOf ext i x✝ = FirstOrder.Language.monadic.structure fun (P : Sym) (e : E) => e ∈ ext i P

@[instance_reducible]

instance RudolphKocurek2024.instDecidableAtomsWInterpOfOfDecidableEq {Sym : Type u_1} {I : Type u_2} {E : Type u_3} [DecidableEq E] (ext : I → Sym → Finset E) : DecidableAtoms (interpOf ext)

Equations

• RudolphKocurek2024.instDecidableAtomsWInterpOfOfDecidableEq ext = inferInstance

inductive RudolphKocurek2024.Pred : Type

The predicates linguist and philosopher.

• linguist : Pred
• philosopher : Pred

@[instance_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.

@[instance_reducible]

instance RudolphKocurek2024.instReprPred : Repr Pred

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instFintypePred : Fintype Pred

Equations

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

@[reducible, inline]

abbrev RudolphKocurek2024.La : ComparativeFormula (FirstOrder.Language.monadic Pred) Entity

Ann is a linguist.

Equations

• RudolphKocurek2024.La = RudolphKocurek2024.ComparativeFormula.matom RudolphKocurek2024.Pred.linguist RudolphKocurek2024.Entity.ann

@[reducible, inline]

abbrev RudolphKocurek2024.Pa : ComparativeFormula (FirstOrder.Language.monadic Pred) Entity

Ann is a philosopher.

Equations

• RudolphKocurek2024.Pa = RudolphKocurek2024.ComparativeFormula.matom RudolphKocurek2024.Pred.philosopher RudolphKocurek2024.Entity.ann

@[instance_reducible]

def RudolphKocurek2024.both : I3 → W → (FirstOrder.Language.monadic Pred).Structure Entity

Ann is a philosopher at i0, a linguist at i1, both at i2.

Equations

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

@[instance_reducible]

def RudolphKocurek2024.neither : I3 → W → (FirstOrder.Language.monadic Pred).Structure Entity

Ann is a philosopher at i0, a linguist at i1, neither at i2.

Equations

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

theorem RudolphKocurek2024.comp_consistent_with_both_and_neither : (Eval both (La.comp Pa) ord₃ I3.i2 W.w0 ∧ Eval both La ord₃ I3.i2 W.w0 ∧ Eval both Pa ord₃ I3.i2 W.w0) ∧ Eval neither (La.comp Pa) ord₃ I3.i2 W.w0 ∧ ¬Eval neither La ord₃ I3.i2 W.w0 ∧ ¬Eval neither Pa ord₃ I3.i2 W.w0

Ann is more a linguist than a philosopher is consistent with her being both and with her being neither, Observation 1.

inductive RudolphKocurek2024.I2 : Type

Two tied interpretations.

• j0 : I2
• j1 : I2

@[instance_reducible]

instance RudolphKocurek2024.instDecidableEqI2 : DecidableEq I2

Equations

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

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✝

@[instance_reducible]

instance RudolphKocurek2024.instReprI2 : Repr I2

Equations

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

@[instance_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

The ordering with j0 and j1 tied at the top.

Equations

• RudolphKocurek2024.tiedOrd = RudolphKocurek2024.SemanticOrdering.ofRank fun (x : RudolphKocurek2024.I2) => 0

@[instance_reducible]

instance RudolphKocurek2024.instDecidableRelI2LeTiedOrd : DecidableRel tiedOrd.le

Equations

• RudolphKocurek2024.instDecidableRelI2LeTiedOrd = RudolphKocurek2024.instDecidableRelI2LeTiedOrd._aux_1

@[instance_reducible]

def RudolphKocurek2024.tied : I2 → W → (FirstOrder.Language.monadic Pred).Structure Entity

Ann is a linguist at j0 and a philosopher at j1.

Equations

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

theorem RudolphKocurek2024.equi_not_consistent : Eval tied (La.equi La.not) tiedOrd I2.j0 W.w0

Ann is as much a linguist as not is consistent, a borderline case, Observation 5.

theorem RudolphKocurek2024.accepted_sup_not_accepted_comp : AssertoricContent tied (La.sup La.not) tiedOrd W.w0 ∧ ¬AssertoricContent tied ((La.comp La.not).sup (La.not.comp La)) tiedOrd W.w0

Acceptance is nonclassical, since the tautology is accepted on the tied model while the disjunction of the two comparatives it splits into is not, as with Yalcin's informational entailment.

theorem RudolphKocurek2024.modus_tollens_not_accepted : AssertoricContent tied (La.comp La.not).not tiedOrd W.w0 ∧ ¬AssertoricContent tied La.not tiedOrd W.w0

Modus tollens fails for acceptance, since if A then more A than not is valid and the negation of its consequent is accepted on the tied model, yet ¬A is not.

def RudolphKocurek2024.dist₃ : DistanceFunction I3 ord₃

The distance function on ord₃ whose thresholds reach one level down.

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instDecidableRelI3CloseDist₃ : DecidableRel dist₃.close

Equations

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

theorem RudolphKocurek2024.sorta_mostly_consistent_with_not : ¬Eval neither La ord₃ I3.i2 W.w0 ∧ EvalSorta neither La ord₃ dist₃ I3.i2 W.w0 ∧ EvalMostly neither La ord₃ dist₃ I3.i2 W.w0

sorta A and mostly A are consistent with ¬A, since at the top of the model where Ann is neither, a close lower level makes her a linguist.

theorem RudolphKocurek2024.not_very_of_eval : Eval both La ord₃ I3.i1 W.w0 ∧ ¬EvalVery both La ord₃ dist₃ I3.i1 W.w0

A does not entail very A, since a close interpretation may falsify it.

theorem RudolphKocurek2024.mcond_not_material : ¬EvalMCond both La Pa ord₃ I3.i2 W.w0

The metalinguistic conditional is not the material conditional, since if Ann is a linguist, she is a philosopher fails at the top of the model where she is both.

No Reversal

inductive RudolphKocurek2024.Entity2 : Type

Two entities for a gradable predicate.

• ann : Entity2
• ben : Entity2

@[instance_reducible]

instance RudolphKocurek2024.instDecidableEqEntity2 : DecidableEq Entity2

Equations

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

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

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instReprEntity2 : Repr Entity2

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instFintypeEntity2 : Fintype Entity2

Equations

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

inductive RudolphKocurek2024.Pred1 : Type

The predicate tall.

• tall : Pred1

@[instance_reducible]

instance RudolphKocurek2024.instDecidableEqPred1 : DecidableEq Pred1

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instReprPred1 : Repr Pred1

Equations

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

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

Equations

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

@[instance_reducible]

instance RudolphKocurek2024.instFintypePred1 : Fintype Pred1

Equations

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

@[reducible, inline]

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

Ann is tall.

Equations

• RudolphKocurek2024.Ta = RudolphKocurek2024.ComparativeFormula.matom RudolphKocurek2024.Pred1.tall RudolphKocurek2024.Entity2.ann

@[reducible, inline]

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

Ben is tall.

Equations

• RudolphKocurek2024.Tb = RudolphKocurek2024.ComparativeFormula.matom RudolphKocurek2024.Pred1.tall RudolphKocurek2024.Entity2.ben

@[instance_reducible]

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

The nested extensions of tall have nobody at i0, Ann at i1 and both at i2.

Equations

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

theorem RudolphKocurek2024.noReversal_nested : NoReversal nested ord₃ Pred1.tall W.w0 Entity2.ben Entity2.ann

No Reversal holds for the nested extensions, in the direction the bridge consumes.

theorem RudolphKocurek2024.ann_taller_nested : Eval nested (Ta.comp Tb) ord₃ I3.i1 W.w0 ∧ ∀ (i : I3), ¬Eval nested (Tb.comp Ta) ord₃ i W.w0

Ann is taller than Ben holds from i1 up and its converse nowhere.

@[instance_reducible]

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

The reversing extensions of tall have Ann at i0, Ben at i1 and both at i2.

Equations

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

theorem RudolphKocurek2024.diverge_without_noReversal : ¬NoReversal reversing ord₃ Pred1.tall W.w0 Entity2.ben Entity2.ann ∧ ¬Eval reversing (Ta.comp Tb) ord₃ I3.i2 W.w0 ∧ (interpretationDelineation reversing ord₃ Pred1.tall W.w0 I3.i2).Comparative Entity2.ann Entity2.ben

Without No Reversal the comparative and the delineation comparative come apart, since the reversing model violates it, the comparative fails at the top, and the delineation comparative holds there.

Equative transitivity

inductive RudolphKocurek2024.Pred3 : Type

Three predicates.

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

@[instance_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.

@[instance_reducible]

instance RudolphKocurek2024.instReprPred3 : Repr Pred3

Equations

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

@[instance_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.

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

@[instance_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✝

@[instance_reducible]

instance RudolphKocurek2024.instReprI4 : Repr I4

Equations

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

@[instance_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.rank₄ : I4 → ℕ

The ranks of the supplement's Figure 1, with i, j and k tied above l.

Equations

• RudolphKocurek2024.rank₄ RudolphKocurek2024.I4.l = 0
• RudolphKocurek2024.rank₄ x✝ = 1

def RudolphKocurek2024.ord₄ : SemanticOrdering I4

The ordering of the supplement's Figure 1.

Equations

• RudolphKocurek2024.ord₄ = RudolphKocurek2024.SemanticOrdering.ofRank RudolphKocurek2024.rank₄

@[instance_reducible]

instance RudolphKocurek2024.instDecidableRelI4LeOrd₄ : DecidableRel ord₄.le

Equations

• RudolphKocurek2024.instDecidableRelI4LeOrd₄ = RudolphKocurek2024.instDecidableRelI4LeOrd₄._aux_1

@[instance_reducible]

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

The model of the supplement's Figure 1. Ann is a linguist and a philosopher at i, only a philosopher at j, a linguist and a psychologist at k, and a philosopher and a psychologist at l.

Equations

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

@[reducible, inline]

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

Ann is a linguist, a philosopher, a psychologist.

Equations

• RudolphKocurek2024.La₄ = RudolphKocurek2024.ComparativeFormula.matom RudolphKocurek2024.Pred3.linguist RudolphKocurek2024.Entity.ann

@[reducible, inline]

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

Equations

• RudolphKocurek2024.Pa₄ = RudolphKocurek2024.ComparativeFormula.matom RudolphKocurek2024.Pred3.philosopher RudolphKocurek2024.Entity.ann

@[reducible, inline]

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

Equations

• RudolphKocurek2024.Ca₄ = RudolphKocurek2024.ComparativeFormula.matom RudolphKocurek2024.Pred3.psychologist RudolphKocurek2024.Entity.ann

theorem RudolphKocurek2024.equi_not_trans : Eval counterexample (La₄.equi Pa₄) ord₄ I4.i W.w0 ∧ Eval counterexample (Pa₄.equi Ca₄) ord₄ I4.i W.w0 ∧ Eval counterexample (La₄.comp Ca₄) ord₄ I4.i W.w0

The basic equative is not transitive. At the top of Figure 1 Ann is as much a linguist as a philosopher and as much a philosopher as a psychologist, but she is more a linguist than a psychologist, since the one interpretation making her a psychologist and not a linguist lies below i, which makes her a linguist and not a psychologist.

theorem RudolphKocurek2024.evalRevised_equi_counterexample : EvalRevised counterexample (La₄.equi Pa₄) ord₄ I4.i W.w0 ∧ EvalRevised counterexample (Pa₄.equi Ca₄) ord₄ I4.i W.w0 ∧ EvalRevised counterexample (La₄.equi Ca₄) ord₄ I4.i W.w0

The revised semantics makes Ann as much a linguist as a psychologist at the top of Figure 1, since i is tied with k, which makes her both, and with j, which makes her neither.