Documentation

Linglib.Semantics.Polarity.Witnesses

Model witnesses for the licensing-context table #

Each witnessed row of LicensingContext.properties carries a model operator realizing its signatures: the classical row via Signature.SoundFor, the Strawson row via Signature.StrawsonSoundFor. This converts the table's strawsonSignature/classicalSignature annotations into derived facts about denotations — the licensing analogue of the derive-don't-stipulate rule.

Coverage is incremental (contextWitness? is Option-valued): the witnessed rows are those whose operators exist in the zoo — negation (complementation), the quantifier rows (every_sem/no_sem/few_sem sections, atMost2_student), conditional antecedents (condNecessity), and the four Strawson-only rows (onlyFull, sorryFull, superlativeAssert, sinceFull). The none rows await operators (without, deny, doubt, before, too…to, the comparatives) or concern rows whose content is the licensing mechanism rather than the signature (the FC/mono rows, questions).

Each witness carries a strength certificate for its classical row (DEStrength.HoldsFor, from Semantics/Polarity/Strength.lean), and ContextWitness.holdsFor_of_licenses grounds the keystone: at a witnessed presupposition-free row, strength-matched licensing means the operator really holds the strength the item requires.

structure Polarity.ContextWitness (c : LicensingContext) :

Type (max (u_1 + 1) (u_2 + 1))

A model-theoretic witness for a licensing-context row: an operator (with its definedness/presupposition function) realizing the row's Strawson signature, and its classical signature when one exists.

W : Type u_1
β : Type u_2
f : Set self.W → self.β
The context function.
defined : Set self.W → self.β
Definedness: where the argument's presupposition is satisfied.
latticeβ : Lattice self.β
boundedβ : BoundedOrder self.β
strawson : c.properties.strawsonSignature.StrawsonSoundFor self.f self.defined
The Strawson row is Strawson-sound for f.
classical (σ : NaturalLogic.Signature) : σ ∈ c.properties.classicalSignature → σ.SoundFor self.f
The classical row, when present, is classically sound for f.
strength (σ : NaturalLogic.Signature) : σ ∈ c.properties.classicalSignature → ∀ s ∈ σ.toDEStrength, s.HoldsFor self.f
The classical row's Zwarts strength holds semantically of f (vacuous at Strawson-only rows).

Instances For

The at-most operator #

The model operator for the .atMost row: antitone in scope but not anti-additive — the strictness witness separating weak DE from anti-additivity.

def Polarity.atMost (n : ℕ) (restr scope : Set (Fin 4)) :

"At most n A's are B" - true if at most n worlds satisfy both. Uses an existential over a sublist witness so the def is decidable only when the predicates are decidable, but stays in Prop.

Equations

Polarity.atMost n restr scope = ∀ (ws : List (Fin 4)), ws.Nodup → (∀ w ∈ ws, restr w ∧ scope w) → ws.length ≤ n

Instances For

theorem Polarity.atMost_mono (n : ℕ) (restr p q : Set (Fin 4)) (hpq : ∀ (w : Fin 4), p w → q w) (h : atMost n restr q) :

atMost n restr p

Monotonicity: if p ⊆ q (entailment) and q has at most n witnesses, so does p.

def Polarity.atMost2_student :

Set (Fin 4) → Set (Fin 4)

"At most 2 students ___" with fixed restrictor.

Equations

Polarity.atMost2_student scope x✝ = Polarity.atMost 2 {0, 1} scope

Instances For

theorem Polarity.atMost_antitone_scope :

Antitone atMost2_student

"At most n" is antitone in scope.

def Polarity.atMost1_student :

Set (Fin 4) → Set (Fin 4)

"At most 1 student ___" with fixed restrictor.

Equations

Polarity.atMost1_student scope x✝ = Polarity.atMost 1 {0, 1} scope

Instances For

theorem Polarity.atMost1_antitone_scope :

Antitone atMost1_student

"At most 1" is still antitone.

theorem Polarity.atMost_not_antiAdditive :

¬IsAntiAdditive atMost1_student

"At most n" is not anti-additive (counterexample): the strictness witness for DE ⊊ anti-additive.

Classical rows #

def Polarity.negationWitness :

ContextWitness LicensingContext.negation

Negation: complementation realizes the anti-morphism row.

Equations

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

Instances For

noncomputable def Polarity.universalRestrictorWitness :

ContextWitness LicensingContext.universalRestrictor

Universal restrictor: the restrictor section of every_sem is completely anti-additive (toy scope falsifying the unit condition's vacuity).

Equations

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

Instances For

noncomputable def Polarity.nobodyWitness :

ContextWitness LicensingContext.nobody

Nobody: the scope section of no_sem is completely anti-additive.

Equations

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

Instances For

noncomputable def Polarity.fewWitness :

ContextWitness LicensingContext.few

Few: the scope section of few_sem is antitone (weak DE — and not anti-additive, matching its .anti row).

Equations

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

Instances For

def Polarity.atMostWitness :

ContextWitness LicensingContext.atMost

At most n: atMost2_student is antitone; the strictness witness atMost_not_antiAdditive is why this row is .anti, not .antiAdd.

Equations

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

Instances For

def Polarity.conditionalAntecedentWitness :

ContextWitness LicensingContext.conditionalAntecedent

Conditional antecedents: the antecedent section of condNecessity is classically antitone with the modal base held constant.

Equations

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

Instances For

Strawson-only rows (`classicalSignature = none`) #

def Polarity.onlyFocusWitness :

ContextWitness LicensingContext.onlyFocus

Only: Strawson-.anti with its existence presupposition; classically nothing (onlyFull_not_de).

Equations

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

Instances For

def Polarity.adversativeWitness :

ContextWitness LicensingContext.adversative

Adversatives: Strawson-.anti with doxastic factivity; classically nothing (sorryFull_not_de).

Equations

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

Instances For

def Polarity.sinceTemporalWitness :

ContextWitness LicensingContext.sinceTemporal

Temporal since: Strawson-.anti with the past-event presupposition.

Equations

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

Instances For

def Polarity.superlativeWitness :

ContextWitness LicensingContext.superlative

Superlatives: Strawson-.anti in the restriction with the designated-subject presupposition.

Equations

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

Instances For

The table #

noncomputable def Polarity.contextWitness? (c : LicensingContext) :

Option (ContextWitness c)

The witness table, populated incrementally; none rows are recorded in the module docstring.

Equations

Instances For

Grounded strength licensing #

@[instance_reducible]

instance Polarity.instLatticeβ {c : LicensingContext} (w : ContextWitness c) :

Lattice w.β

Equations

Polarity.instLatticeβ w = w.latticeβ

@[instance_reducible]

instance Polarity.instBoundedOrderβ {c : LicensingContext} (w : ContextWitness c) :

BoundedOrder w.β

Equations

Polarity.instBoundedOrderβ w = w.boundedβ

theorem Polarity.ContextWitness.holdsFor_of_licenses {c : LicensingContext} (w : ContextWitness c) (hcl : c.properties.classicalSignature = some c.properties.strawsonSignature) {e : Item} (hlic : zwartsScale.licenses e c) (r : DEStrength) :

r ∈ e.licensor → r.HoldsFor w.f

At a witnessed presupposition-free row, keystone strength licensing is semantically real: the witness operator holds the strength the item requires. Strawson-only rows are exempt — their antitonicity holds only on the definedness region.