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.Quantification.CovertQuantifier (genThreshold dist dpp extendLexicon)

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

def Semantics.Quantification.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.Quantification.CovertQuantifier.covertQ domain restriction scope = domain.all fun (d : D) => !restriction d || scope d

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

Dual formulation: no counterexample exists.

Equations

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

theorem Semantics.Quantification.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.Quantification.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.Quantification.CovertQuantifier.thresholdQ {D : Type} (domain : List D) (restriction scope : D → Bool) (θ : ℚ) : Bool

Threshold-based alternative: measure > θ.

Equations

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

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

Measure is non-negative.

theorem Semantics.Quantification.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.Quantification.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.Quantification.CovertQuantifier.gen (F : Core.Logic.Intensional.Frame) (generally : (F.Entity → Prop) → (F.Entity → Prop) → Prop) : Montague.LexEntry F

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.

noncomputable def Semantics.Quantification.CovertQuantifier.genThreshold (F : Core.Logic.Intensional.Frame) (atoms : List F.Entity) (num denom : ℕ) : Montague.LexEntry F

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.Quantification.CovertQuantifier.dist (F : Core.Logic.Intensional.Frame) (atomsOf : F.Entity → List F.Entity) : Montague.LexEntry F

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.Quantification.CovertQuantifier.dpp (F : Core.Logic.Intensional.Frame) (atoms : List F.Entity) : Montague.LexEntry F

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.Quantification.CovertQuantifier.hab (F : Core.Logic.Intensional.Frame) (h : (F.Entity → Prop) → F.Entity → Prop) : Montague.LexEntry F

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

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

def Semantics.Quantification.CovertQuantifier.exh (F : Core.Logic.Intensional.Frame) (exhOp : (F.Index → Prop) → F.Index → Prop) : Montague.LexEntry F

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. The canonical computational implementation is exhIE from Exhaustification.Innocent (the Set-spec is exhIE in Exhaustification.Operators). Specific instances are plugged in at lexicon construction time with 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.Quantification.CovertQuantifier.exh F exhOp = { ty := Core.Logic.Intensional.Ty.t.intens ⇒ Core.Logic.Intensional.Ty.t.intens, denot := exhOp }

def Semantics.Quantification.CovertQuantifier.extendLexicon {F : Core.Logic.Intensional.Frame} (base : Montague.Lexicon F) (ops : List (String × Montague.LexEntry F)) : Montague.Lexicon F

Extend a lexicon with named covert operators.

Equations

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