Parameterized Update

Framework-agnostic infrastructure for semantics and pragmatics with parameter uncertainty: meaning depends on a parameter (threshold, compositional context, comparison class, variable assignment) and truth at a world involves quantifying over available parameters.

The Fiber Bundle

A fragment set F ⊆ P × W is a fiber bundle over worlds W. The fiber at w is F_w = {p : F(p, w)} — the parameters available at that world. An assertion φ with parameterized semantics ⟦φ⟧ : P → W → Prop acts as a fiberwise filter: F' = {(p, w) ∈ F : ⟦φ⟧(p, w)}.

Different linguistic theories differ in how they project from the bundle back to worlds, using the ∃ ⊣ Δ ⊣ ∀ adjunction:

• ∃-projection (@cite{caie-2023}, Barker 2002): w survives iff ∃ p ∈ F_w, ⟦φ⟧(p, w)
• ∀-projection (supervaluation, Fine 1975): w survives iff ∀ p ∈ F_w, ⟦φ⟧(p, w)
• Σ-projection (RSA, @cite{lassiter-goodman-2017}): score(w) = Σ_p weight(p) · ⟦φ⟧(p, w)

The first two are De Morgan duals (not_forall): ¬(∀p.φ) ↔ ∃p.¬φ. The third is a soft interpolation (not formalized here; see RSA).

Instances

Theory	P (parameter)	Projection
Caie 2023	compositional context	∃
Supervaluation	precisification	∀
RSA (L&G 2017)	threshold θ	Σ
CCP	variable assignment	∃
Klein 1980	comparison class	∃ (comp.)

Monotone Collapse

When semantics is antitone in the parameter (e.g., d > θ for degree semantics), the projections collapse to extremal checks:

• ∃ p ∈ F_w, sem(p, w) ↔ sem(min(F_w), w)
• ∀ p ∈ F_w, sem(p, w) ↔ sem(max(F_w), w)

The gap between min and max is the borderline region: worlds where ∃-projection and ∀-projection disagree.

Contextual Pruning

Sequential assertion with pruning — the mechanism by which earlier assertions constrain which parameters are available for later ones — reduces to a single update checking both conditions. This holds for both ∃ and ∀ projection.

@[reducible, inline]

abbrev Core.Semantics.ParameterizedUpdate.FragmentSet (P : Type u_3) (W : Type u_4) : Type (max u_3 u_4)

A fragment set: a relation between parameters and worlds. F(p, w) holds iff parameter p is available at world w. The fiber at w is F_w = {p : F p w}.

Generalizes InterpAssignment C W from @cite{caie-2023} (argument order swapped).

Equations

• Core.Semantics.ParameterizedUpdate.FragmentSet P W = (P → W → Prop)

def Core.Semantics.ParameterizedUpdate.fiberwiseFilter {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) : FragmentSet P W

Fiberwise filter: restrict a fragment set to parameter–world pairs where the semantics holds.

Generalizes Contextual Pruning (@cite{caie-2023}): after asserting α, only parameters that made α true remain available.

Equations

• Core.Semantics.ParameterizedUpdate.fiberwiseFilter F sem p w = (F p w ∧ sem p w)

def Core.Semantics.ParameterizedUpdate.existentialProjection {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) : Set W

Existential projection: w survives iff some parameter in F_w makes the semantics true.

This is @cite{caie-2023}'s disjunctive updating and Barker 2002's dynamics of vagueness.

Equations

• Core.Semantics.ParameterizedUpdate.existentialProjection F sem w = ∃ (p : P), F p w ∧ sem p w

def Core.Semantics.ParameterizedUpdate.universalProjection {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) : Set W

Universal projection: w survives iff all parameters in F_w make the semantics true.

This is super-truth (Fine 1975): truth under all admissible precisifications.

Equations

• Core.Semantics.ParameterizedUpdate.universalProjection F sem w = ∀ (p : P), F p w → sem p w

def Core.Semantics.ParameterizedUpdate.existentialUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) : Set W

Existential update: restrict to the context set, then ∃-project.

existentialUpdate cs F sem w ↔ w ∈ cs ∧ ∃ p ∈ F_w, sem(p, w).

Equations

• Core.Semantics.ParameterizedUpdate.existentialUpdate cs F sem w = (cs w ∧ Core.Semantics.ParameterizedUpdate.existentialProjection F sem w)

def Core.Semantics.ParameterizedUpdate.universalUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) : Set W

Universal update: restrict to the context set, then ∀-project.

universalUpdate cs F sem w ↔ w ∈ cs ∧ ∀ p ∈ F_w, sem(p, w).

Equations

• Core.Semantics.ParameterizedUpdate.universalUpdate cs F sem w = (cs w ∧ Core.Semantics.ParameterizedUpdate.universalProjection F sem w)

theorem Core.Semantics.ParameterizedUpdate.deMorgan_existential_universal {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) (w : W) : existentialProjection F sem w ↔ ¬universalProjection F (fun (p : P) (w : W) => ¬sem p w) w

De Morgan duality (∃-side): ∃-projection of sem ↔ negation of ∀-projection of the negation.

theorem Core.Semantics.ParameterizedUpdate.deMorgan_universal_existential {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) (w : W) : universalProjection F sem w ↔ ¬existentialProjection F (fun (p : P) (w : W) => ¬sem p w) w

De Morgan duality (∀-side): ∀-projection of sem ↔ negation of ∃-projection of the negation.

theorem Core.Semantics.ParameterizedUpdate.monotoneCollapse_exists {P : Type u_1} {W : Type u_2} [Preorder P] (F : FragmentSet P W) (sem : P → W → Prop) (w : W) (p₀ : P) (h_least : IsLeast {p : P | F p w} p₀) (h_anti : Antitone fun (p : P) => sem p w) : existentialProjection F sem w ↔ sem p₀ w

Monotone collapse (∃): when sem is Antitone in p and F_w has a least element, ∃-projection reduces to checking the minimum.

The Antitone condition on fun p => sem p w means p₁ ≤ p₂ → sem p₂ w → sem p₁ w — truth propagates downward in the parameter ordering. This is the standard situation in degree semantics: ⟦tall⟧(θ, w) = degree(w) > θ is antitone in θ.

theorem Core.Semantics.ParameterizedUpdate.monotoneCollapse_forall {P : Type u_1} {W : Type u_2} [Preorder P] (F : FragmentSet P W) (sem : P → W → Prop) (w : W) (p₀ : P) (h_greatest : IsGreatest {p : P | F p w} p₀) (h_anti : Antitone fun (p : P) => sem p w) : universalProjection F sem w ↔ sem p₀ w

Monotone collapse (∀): when sem is Antitone in p and F_w has a greatest element, ∀-projection reduces to checking the maximum.

For degree semantics: the ∀-projection ∀ θ ∈ Θ, degree(w) > θ collapses to degree(w) > max(Θ).

theorem Core.Semantics.ParameterizedUpdate.projections_agree_iff_clear {P : Type u_1} {W : Type u_2} [Preorder P] (F : FragmentSet P W) (sem : P → W → Prop) (w : W) (p_min p_max : P) (h_least : IsLeast {p : P | F p w} p_min) (h_greatest : IsGreatest {p : P | F p w} p_max) (h_anti : Antitone fun (p : P) => sem p w) : (existentialProjection F sem w ↔ universalProjection F sem w) ↔ sem p_max w ∨ ¬sem p_min w

Corollary: when sem is antitone and F_w has both a least and greatest element, the ∃ and ∀ projections agree iff w is outside the borderline region — either sem holds at the hardest parameter (clearly in) or fails at the easiest (clearly out).

The borderline region where projections disagree is precisely sem p_min w ∧ ¬ sem p_max w.

theorem Core.Semantics.ParameterizedUpdate.sequential_existentialUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem₁ sem₂ : P → W → Prop) : existentialUpdate (existentialUpdate cs F sem₁) (fiberwiseFilter F sem₁) sem₂ = existentialUpdate cs F fun (p : P) (w : W) => sem₁ p w ∧ sem₂ p w

Sequential ∃-update with pruning: asserting α then β (where β's parameters are pruned by α) equals a single ∃-update checking both α and β.

This is the general form of Contextual Pruning (@cite{caie-2023}): the two-step process (update context set by α, prune parameters by α, then update by β) is equivalent to a single update requiring both α and β under the same parameter.

theorem Core.Semantics.ParameterizedUpdate.sequential_universalUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem₁ sem₂ : P → W → Prop) : universalUpdate (universalUpdate cs F sem₁) (fiberwiseFilter F sem₁) sem₂ = universalUpdate cs F fun (p : P) (w : W) => sem₁ p w ∧ sem₂ p w

Sequential ∀-update with pruning: asserting α then β (where β's parameters are pruned by α) equals a single ∀-update checking both α and β.

The ∀ case works because: if all parameters satisfy α (first step), then "pruned parameters" = "all parameters", so requiring β for pruned parameters = requiring β for all parameters.

theorem Core.Semantics.ParameterizedUpdate.existentialProjection_mono {P : Type u_1} {W : Type u_2} (F₁ F₂ : FragmentSet P W) (sem : P → W → Prop) (h : ∀ (p : P) (w : W), F₁ p w → F₂ p w) (w : W) : existentialProjection F₁ sem w → existentialProjection F₂ sem w

∃-projection is Monotone in the fragment set: expanding available parameters can only add surviving worlds. The FragmentSet P W type P → W → Prop carries the pointwise → ordering, and ∃-projection preserves it.

theorem Core.Semantics.ParameterizedUpdate.universalProjection_anti {P : Type u_1} {W : Type u_2} (F₁ F₂ : FragmentSet P W) (sem : P → W → Prop) (h : ∀ (p : P) (w : W), F₁ p w → F₂ p w) (w : W) : universalProjection F₂ sem w → universalProjection F₁ sem w

∀-projection is Antitone in the fragment set: expanding available parameters can only remove surviving worlds (more to check).

theorem Core.Semantics.ParameterizedUpdate.existentialUpdate_restricts {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) (w : W) : existentialUpdate cs F sem w → cs w

∃-update only removes worlds from the context set.

theorem Core.Semantics.ParameterizedUpdate.universalUpdate_restricts {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) (w : W) : universalUpdate cs F sem w → cs w

∀-update only removes worlds from the context set.

theorem Core.Semantics.ParameterizedUpdate.fiberwiseFilter_sub {P : Type u_1} {W : Type u_2} (F : FragmentSet P W) (sem : P → W → Prop) (p : P) (w : W) : fiberwiseFilter F sem p w → F p w

Fiberwise filter only removes parameters.

theorem Core.Semantics.ParameterizedUpdate.universalUpdate_implies_existentialUpdate {P : Type u_1} {W : Type u_2} (cs : Set W) (F : FragmentSet P W) (sem : P → W → Prop) (w : W) (h_ne : ∃ (p : P), F p w) : universalUpdate cs F sem w → existentialUpdate cs F sem w

∀-update implies ∃-update when the fiber is non-empty. Super-truth implies disjunctive survival.

theorem Core.Semantics.ParameterizedUpdate.singleton_projections_agree {P : Type u_1} {W : Type u_2} (p₀ : P) (sem : P → W → Prop) (w : W) : existentialProjection (fun (p : P) (x : W) => p = p₀) sem w ↔ universalProjection (fun (p : P) (x : W) => p = p₀) sem w

When F_w is a singleton {p₀}, both projections agree with a direct check of sem(p₀, w). No parameter uncertainty.

theorem Core.Semantics.ParameterizedUpdate.existentialUpdate_singleton {P : Type u_1} {W : Type u_2} (cs : Set W) (p₀ : P) (sem : P → W → Prop) : existentialUpdate cs (fun (p : P) (x : W) => p = p₀) sem = fun (w : W) => cs w ∧ sem p₀ w

Singleton ∃-update reduces to propositional filtering.