Cross-world extremum under entailment

[Fox07] [FH06b] [BR99] [vFFI14] [Rou26]

The cross-world entailment-based "maximally informative" predicate (IsMaxInf) that has no mathlib analogue, plus mathlib bridges for the per-world specialization, plus the MIP_Licensed licensing predicate combining non-constancy with per-world extremum existence.

Two formulations

The mathlib-shape per-world reading is just IsLeast {y | P y w} x (or IsGreatest) — call mathlib directly. The Fox 2007-style cross-world reading is unique to formal semantics:

IsMaxInf P x w := P x w ∧ ∀ y, P y w → ∀ w', P x w' → P y w'

reading: at world w, x is true; and for any other true alternative y at w, the proposition denoted by x entails the proposition denoted by y across every world. Equivalently: x denotes the smallest proposition (in subset order on Set W) among true alternatives at w. Bridge to per-world via mathlib's MonotoneOn.map_isLeast family.

Two predicates fail under different conditions, so the MIP licensing condition is their conjunction:

• AdmitsOptimum P (non-constancy in α; the atelic / homogeneous failure): fails when every alternative denotes the same proposition — no informative distinction among alternatives.
• IsLeast {y | P y w} x (existence of a smallest-true alternative; the no-extremum failure under density): fails when the true set is upward-closed with no minimum (e.g., Set.Ioi a in a dense linear order).

Naming

The shared mathematical structure — extracting the extremal element of an indexed family under an evaluation map — also appears outside semantics (notably as argmax_u (ln P_L0(s | u)) in RSA-style pragmatics; both pick the most informative alternative under their respective evaluation map). The file lives in Semantics/Entailment/ because the cross-world quantifier is the entailment relation between propositions.

Beck-Rullmann attribution

[BR99] introduce answer1(w)(Q) = ⋂{p : Q(w)(p) ∧ p(w)} — the conjunction of all true Hamblin propositions at w. For upward-monotone scalar predicates this reduces to the smallest-true-degree case captured by IsLeast. For non-scalar predicates (their §4.4) it is the literal conjunction and not an extremum. So the IsLeast per-world reading is an ergonomic specialization of Beck-Rullmann answerhood under monotonicity, not their primary formulation.

def Entailment.IsMaxInf {α : Type u_1} {W : Type u_2} (P : α → W → Prop) (x : α) (w : W) : Prop

A scale value x is maximally informative in a degree property P at world w iff P x w is true and P x entails P y (across every world) for every other true P y w.

The unified exhaustivity condition underlying only-implicatures, degree questions, and definite descriptions in the [Fox07] / [vFFI14] tradition. [Rou26] specializes this to numerals in temporal in-adverbials.

Equations

• Entailment.IsMaxInf P x w = (P x w ∧ ∀ (y : α), P y w → ∀ (w' : W), P x w' → P y w')

def Entailment.HasMaxInf {α : Type u_1} {W : Type u_2} (P : α → W → Prop) (w : W) : Prop

A degree property has a maximally informative element at world w.

Equations

• Entailment.HasMaxInf P w = ∃ (x : α), Entailment.IsMaxInf P x w

def Entailment.InformationCollapse {α : Type u_1} {W : Type u_2} (P : α → W → Prop) : Prop

Information collapse: no element is maximally informative at any world. [FH06b]: this is why degree questions fail over dense complements, why only + "more than n" is contradictory, and why definite descriptions over dense open sets lack a presupposition-satisfying referent.

Equations

• Entailment.InformationCollapse P = ∀ (w : W), ¬Entailment.HasMaxInf P w

theorem Entailment.isMaxInf_of_isLeast_upward {α : Type u_1} [LinearOrder α] {W : Type u_2} {P : α → W → Prop} (hUp : Degree.IsUpwardMonotone P) (w : W) (x : α) (h : IsLeast {y : α | P y w} x) : IsMaxInf P x w

For an upward-monotone family, a per-world smallest-true value is cross-world maximally informative. The converse requires threshold-witness assumptions on the world space (one direction only).

theorem Entailment.isMaxInf_of_isGreatest_downward {α : Type u_1} [LinearOrder α] {W : Type u_2} {P : α → W → Prop} (hDown : Degree.IsDownwardMonotone P) (w : W) (x : α) (h : IsGreatest {y : α | P y w} x) : IsMaxInf P x w

Dually for downward-monotone families: the per-world largest-true value is cross-world maximally informative.

def Entailment.MIP_Licensed {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) : Prop

Maximal Informativity Principle licensing for upward-monotone derived properties (e.g., E-TIA telic in [Rou26]). The conjunction captures both failure modes:

• AdmitsOptimum P (non-constancy): the family distinguishes alternatives at all (failure mode for atelic / homogeneous predicates).
• IsLeast {y | P y w} x at some w: a smallest true value exists (failure mode under density without minimum).

Equations

• Entailment.MIP_Licensed P = (Degree.AdmitsOptimum P ∧ ∃ (w : W) (x : α), IsLeast {y : α | P y w} x)

def Entailment.MIP_LicensedDown {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) : Prop

Dual MIP licensing for downward-monotone derived properties (e.g., G-TIA in negative perfects).

Equations

• Entailment.MIP_LicensedDown P = (Degree.AdmitsOptimum P ∧ ∃ (w : W) (x : α), IsGreatest {y : α | P y w} x)

Applications of IsMaxInf to the canonical degree predicates Comparison.{ge,gt,le}.over (defined in Core/Order/Comparison.lean, monotonicity in Semantics/Degree/Predicate.lean). The IsMaxInf-flavored consequences live here as a downstream entailment-theoretic application.

theorem Entailment.atLeast_hasMaxInf {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (w : W) : HasMaxInf (Core.Order.Comparison.ge.over μ) w

"At least d" always has a maximally informative element: d₀ = μ(w).

This holds on ANY scale — dense or discrete — because the actual value μ(w) is always in the domain and "at least μ(w)" entails "at least d" for all d ≤ μ(w) by transitivity.

This is why bare numerals generate scalar implicatures regardless of scale density: the ≥ relation creates a closed set with a natural maximum at the true value.

theorem Entailment.moreThan_noMaxInf {α : Type u_1} [LinearOrder α] {W : Type u_2} [DenselyOrdered α] (μ : W → α) (hSurj : Function.Surjective μ) (w : W) : ¬HasMaxInf (Core.Order.Comparison.gt.over μ) w

Implicature asymmetry ([Fox07], [FH06b]): on a dense scale, "more than n" has NO maximally informative element.

For any candidate d₀ < μ(w), density gives d' ∈ (d₀, μ(w)). A witness world w₁ with μ(w₁) ∈ (d₀, d') has "more than d₀" true but "more than d'" false — so d₀ does not entail d'.

The hSurj hypothesis says every degree value is realized by some possible world.

theorem Entailment.isMaxInf_atLeast_of_hit {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (m : α) (w : W) (hHit : ∃ (w' : W), μ w' = m) : IsMaxInf (Core.Order.Comparison.ge.over μ) m w ↔ μ w = m

Kennedy / [FH06b] bridge (point-realization form): IsMaxInf of the "at least" degree property at value m and world w holds iff μ w = m, given only that m itself is in the image of μ. This is strictly weaker than full Function.Surjective μ and is the hypothesis actually used in the proof.

theorem Entailment.isMaxInf_atLeast_iff_eq {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : IsMaxInf (Core.Order.Comparison.ge.over μ) m w ↔ μ w = m

Kennedy / [FH06b] bridge: IsMaxInf of the "at least" degree property at value m and world w holds iff the measure at w equals m, under full surjectivity. Corollary of isMaxInf_atLeast_of_hit.

theorem Entailment.moreThan_nat_hasMaxInf {W : Type u_2} (μ : W → ℕ) (w : W) (hw : w ∈ Core.Order.Comparison.gt.over μ 0) : HasMaxInf (Core.Order.Comparison.gt.over μ) w

On ℕ, "more than m" has HasMaxInf: the discrete collapse rescues maximality. Contrast with moreThan_noMaxInf: on dense scales, HasMaxInf fails.

theorem Entailment.atMost_hasMaxInf {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (w : W) : HasMaxInf (Core.Order.Comparison.le.over μ) w

"At most d" always has a maximally informative element: d₀ = μ(w). Symmetric to atLeast_hasMaxInf.

theorem Entailment.isMaxInf_atMost_iff_eq {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : IsMaxInf (Core.Order.Comparison.le.over μ) m w ↔ μ w = m

Kennedy / [Rou26] bridge: IsMaxInf of "at most d" at value m and world w holds iff the measure at w equals m. Symmetric to isMaxInf_atLeast_iff_eq: the MIP derives exact meaning from "at most" just as it does from "at least".

Kennedy's de-Fregean type-shift is the MIP applied to a monotone degree property: for both "at least" (Kennedy direction) and "at most" ([Rou26] direction), max⊨ at world w = μ(w), the true value. So the MIP universally derives exact meaning from monotone degree properties, regardless of monotonicity direction.

theorem Entailment.mip_atLeast_is_exact {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : IsMaxInf (Core.Order.Comparison.ge.over μ) m w ↔ w ∈ Core.Order.Comparison.eq.over μ m

MIP derives exact meaning from "at least" (Kennedy's direction).

theorem Entailment.mip_atMost_is_exact {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : IsMaxInf (Core.Order.Comparison.le.over μ) m w ↔ w ∈ Core.Order.Comparison.eq.over μ m

MIP derives exact meaning from "at most" (Rouillard's direction).

theorem Entailment.mip_direction_invariant {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (m : α) (w : W) (hSurj : Function.Surjective μ) : IsMaxInf (Core.Order.Comparison.ge.over μ) m w ↔ IsMaxInf (Core.Order.Comparison.le.over μ) m w

The MIP is direction-invariant: "at least" and "at most" yield the same exact meaning under maximal informativity. Kennedy's type-shift and Rouillard's MIP are literally the same operation.

The bundled form: DirectedMeasure.degreeProperty

DirectedMeasure.degreeProperty derives "at least" or "at most" from the stored direction; under maximal informativity either direction yields exact meaning at the true measure value. This ties the algebraic constructor layer (numeral, adjective, epistemic thresholds) to the entailment-theoretic MIP layer.

theorem Degree.DirectedMeasure.isMaxInf_degreeProperty_iff {α : Type u_1} [LinearOrder α] {W : Type u_2} (dm : DirectedMeasure α W) (m : α) (w : W) (hSurj : Function.Surjective dm.μ) : Entailment.IsMaxInf dm.degreeProperty m w ↔ dm.μ w = m

The maximally informative degree of a directed measure's derived property is the true measure value, whichever the direction.

theorem Degree.DirectedMeasure.isMaxInf_degreeProperty_congr {α : Type u_1} [LinearOrder α] {W : Type u_2} (dm₁ dm₂ : DirectedMeasure α W) (hμ : dm₁.μ = dm₂.μ) (m : α) (w : W) (hSurj : Function.Surjective dm₁.μ) : Entailment.IsMaxInf dm₁.degreeProperty m w ↔ Entailment.IsMaxInf dm₂.degreeProperty m w

Direction-invariance, bundled: two directed measures sharing a measure function agree on maximal informativity regardless of direction or boundedness — the constructor-level form of mip_direction_invariant.