Covert Operators: Theory and Compositional Interface

@cite{krifka-etal-1995} @cite{carlson-1977} @cite{guerrini-2026}

Covert operators (Gen, DIST, Hab, DPP) are semantically contentful LF nodes with no overt realization. This module provides:

1. Abstract quantifier theory (covertQ, measure, thresholdQ) — domain-polymorphic semantics with eliminability proofs. GEN and HAB are both instances.

2. Montague-typed constructors (gen, genThreshold, dist, dpp, hab) — LexEntry values that compose via FA in evalTree. These package the theory-layer semantics for tree-based interpretation.

Usage

open Semantics.Lexical.CovertQuantifier (genThreshold dist dpp extendLexicon)

def myLex : Lexicon myModel :=
  extendLexicon baseLex
    [("Gen",  genThreshold myModel atoms 2 3),
     ("DIST", dist myModel atomsOf)]

def Semantics.Lexical.CovertQuantifier.covertQ {D : Type} (domain : List D) (restriction scope : D → Bool) : Bool

A covert quantifier: ∀d ∈ domain. restriction(d) → scope(d). GEN instantiates with D = Situation, restriction = normal ∧ restrictor. HAB instantiates with D = Occasion, restriction = characteristic.

Equations

• Semantics.Lexical.CovertQuantifier.covertQ domain restriction scope = domain.all fun (d : D) => !restriction d || scope d

def Semantics.Lexical.CovertQuantifier.covertQ_dual {D : Type} (domain : List D) (restriction scope : D → Bool) : Bool

Dual formulation: no counterexample exists.

Equations

• Semantics.Lexical.CovertQuantifier.covertQ_dual domain restriction scope = !domain.any fun (d : D) => restriction d && !scope d

theorem Semantics.Lexical.CovertQuantifier.covertQ_equiv {D : Type} (domain : List D) (restriction scope : D → Bool) : covertQ domain restriction scope = covertQ_dual domain restriction scope

The two formulations are equivalent (De Morgan).

def Semantics.Lexical.CovertQuantifier.measure {D : Type} (domain : List D) (restriction scope : D → Bool) : ℚ

Measure: proportion of restriction-satisfying cases where scope holds.

Equations

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

def Semantics.Lexical.CovertQuantifier.thresholdQ {D : Type} (domain : List D) (restriction scope : D → Bool) (θ : ℚ) : Bool

Threshold-based alternative: measure > θ.

Equations

• Semantics.Lexical.CovertQuantifier.thresholdQ domain restriction scope θ = decide (Semantics.Lexical.CovertQuantifier.measure domain restriction scope > θ)

theorem Semantics.Lexical.CovertQuantifier.measure_nonneg {D : Type} (domain : List D) (restriction scope : D → Bool) : measure domain restriction scope ≥ 0

Measure is non-negative.

theorem Semantics.Lexical.CovertQuantifier.measure_le_one {D : Type} (domain : List D) (restriction scope : D → Bool) (hNonEmpty : (List.filter restriction domain).length > 0) : measure domain restriction scope ≤ 1

Measure is at most 1 (when restriction domain is non-empty).

theorem Semantics.Lexical.CovertQuantifier.reduces_to_threshold {D : Type} (domain : List D) (restriction scope : D → Bool) (hNonEmpty : (List.filter restriction domain).length > 0) : ∃ (θ : ℚ), covertQ domain restriction scope = thresholdQ domain restriction scope θ

Any covert quantifier configuration can be matched by threshold semantics.

Note: this is a degeneracy result — the existential threshold is either -1 (if Q holds) or 1 (if Q fails). It shows eliminability in principle, not that the threshold is informative. The RSA treatment adds substance by making the threshold uncertain and pragmatically inferred.

def Semantics.Lexical.CovertQuantifier.gen (m : Montague.Model) (generally : (m.Entity → Bool) → (m.Entity → Bool) → Bool) : Montague.LexEntry m

Gen: (e→t) → (e→t) → t. Dyadic generic quantifier.

generally encodes the truth conditions — different theories instantiate it differently (threshold, normalcy, probabilistic). traditionalGEN (in Generics.lean) and thresholdQ (above) are specific instantiations.

Equations

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

def Semantics.Lexical.CovertQuantifier.genThreshold (m : Montague.Model) (atoms : List m.Entity) (num denom : ℕ) : Montague.LexEntry m

Gen with threshold: true iff ≥ num/denom of restrictor-satisfying atoms also satisfy scope. Montague-typed counterpart of thresholdQ.

Equations

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

def Semantics.Lexical.CovertQuantifier.dist (m : Montague.Model) (atomsOf : m.Entity → List m.Entity) : Montague.LexEntry m

DIST: (e→t) → (e→t). Distributive operator.

atomsOf x returns the atomic parts of x — for atomic entities it returns [x], for plural/kind entities their parts. Montague-typed counterpart of Distributivity.distMaximal.

Equations

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

def Semantics.Lexical.CovertQuantifier.dpp (m : Montague.Model) (atoms : List m.Entity) : Montague.LexEntry m

DPP: (e→t) → (e→t) → t. Derived Property Predication.

DPP(P)(Q) = ∃x[P(x) ∧ Q(x)]. An existential type-shift for kind-denoting NPs combining with stage-level predicates. @cite{guerrini-2026} structure (105b).

Equations

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

def Semantics.Lexical.CovertQuantifier.hab (m : Montague.Model) (h : (m.Entity → Bool) → m.Entity → Bool) : Montague.LexEntry m

Hab: (e→t) → (e→t). Habitual aspectual operator.

h maps a predicate to its habitual counterpart. Montague-typed counterpart of traditionalHAB (in Habituals.lean).

Equations

• Semantics.Lexical.CovertQuantifier.hab m h = { ty := (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t) ⇒ Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t, denot := h }

def Semantics.Lexical.CovertQuantifier.exh (m : Montague.Model) (exhOp : (m.World → Bool) → m.World → Bool) : Montague.LexEntry m

EXH: (s→t) → (s→t). Exhaustivity operator (proposition modifier).

exhOp maps a proposition to its exhaustified version — typically asserting the prejacent and negating innocently excludable alternatives. Specific implementations (exhB from InnocentExclusion, applyIEBool from Operators) are plugged in at lexicon construction time with their alternatives and world domain baked into the closure.

Unlike Gen/DIST/Hab (which quantify over entities), EXH operates on propositions (s→t). Both compose via FA in the same tree — the Montague type system handles the dispatch:

• Gen: (e→t) → (e→t) → t — FA with entity predicates
• EXH: (s→t) → (s→t) — FA with propositions

Equations

• Semantics.Lexical.CovertQuantifier.exh m exhOp = { ty := (Semantics.Montague.Ty.s ⇒ Semantics.Montague.Ty.t) ⇒ Semantics.Montague.Ty.s ⇒ Semantics.Montague.Ty.t, denot := exhOp }

def Semantics.Lexical.CovertQuantifier.extendLexicon {m : Montague.Model} (base : Montague.Lexicon m) (ops : List (String × Montague.LexEntry m)) : Montague.Lexicon m

Extend a lexicon with named covert operators.

Equations

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