Linglib.Core.Logic.NaturalLogic

inductive Core.NaturalLogic.NLRelation :

The seven basic set-theoretic relations between denotations (@cite{maccartney-manning-2009}, @cite{icard-2012} §1).

Symbol	Name	Set relation	Example
≡	equivalence	A = B	couch / sofa
⊑	forward	A ⊂ B	dog / animal
⊒	reverse	A ⊃ B	animal / dog
^	negation	A ∩ B = ∅, A ∪ B = U	happy / unhappy
\|	alternation	A ∩ B = ∅	cat / dog
⌣	cover	A ∪ B = U	animal / nondog
#	independent	all other cases	hungry / tall

equiv : NLRelation
forward : NLRelation
reverse : NLRelation
negation : NLRelation
alternation : NLRelation
cover : NLRelation
independent : NLRelation

Instances For

source

instance Core.NaturalLogic.instDecidableEqNLRelation :

DecidableEq NLRelation

Equations

Core.NaturalLogic.instDecidableEqNLRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Core.NaturalLogic.instBEqNLRelation :

BEq NLRelation

Equations

Core.NaturalLogic.instBEqNLRelation = { beq := Core.NaturalLogic.instBEqNLRelation.beq }

source

def Core.NaturalLogic.instBEqNLRelation.beq :

NLRelation → NLRelation → Bool

Equations

Core.NaturalLogic.instBEqNLRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.NaturalLogic.instReprNLRelation :

Repr NLRelation

Equations

Core.NaturalLogic.instReprNLRelation = { reprPrec := Core.NaturalLogic.instReprNLRelation.repr }

source

def Core.NaturalLogic.instReprNLRelation.repr :

NLRelation → ℕ → Std.Format

Equations

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

Instances For

source

def Core.NaturalLogic.NLRelation.refines :

NLRelation → NLRelation → Bool

Informativity ordering on NL relations.

R ≤ R' means R is at least as informative as R'. The lattice has ≡ at the bottom (most informative) and # at the top (least informative).

Key: ^ (negation) refines both | (alternation) and ⌣ (cover), because knowing sets are complementary tells you both that they're disjoint (|) and exhaustive (⌣).

Equations

Instances For

source

instance Core.NaturalLogic.NLRelation.instLE :

LE NLRelation

Equations

Core.NaturalLogic.NLRelation.instLE = { le := fun (a b : Core.NaturalLogic.NLRelation) => a.refines b = true }

source

instance Core.NaturalLogic.NLRelation.instPreorder :

Preorder NLRelation

Equations

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

source

instance Core.NaturalLogic.NLRelation.instPartialOrder :

PartialOrder NLRelation

Equations

Core.NaturalLogic.NLRelation.instPartialOrder = { toPreorder := Core.NaturalLogic.NLRelation.instPreorder, le_antisymm := ⋯ }

source

instance Core.NaturalLogic.NLRelation.instBot :

Bot NLRelation

Equations

Core.NaturalLogic.NLRelation.instBot = { bot := Core.NaturalLogic.NLRelation.equiv }

source

instance Core.NaturalLogic.NLRelation.instTop :

Top NLRelation

Equations

Core.NaturalLogic.NLRelation.instTop = { top := Core.NaturalLogic.NLRelation.independent }

source

instance Core.NaturalLogic.NLRelation.instOrderBot :

OrderBot NLRelation

Equations

Core.NaturalLogic.NLRelation.instOrderBot = { toBot := Core.NaturalLogic.NLRelation.instBot, bot_le := Core.NaturalLogic.NLRelation.instOrderBot._proof_1 }

source

instance Core.NaturalLogic.NLRelation.instOrderTop :

OrderTop NLRelation

Equations

Core.NaturalLogic.NLRelation.instOrderTop = { toTop := Core.NaturalLogic.NLRelation.instTop, le_top := Core.NaturalLogic.NLRelation.instOrderTop._proof_1 }

source

instance Core.NaturalLogic.NLRelation.instBoundedOrder :

BoundedOrder NLRelation

Equations

Core.NaturalLogic.NLRelation.instBoundedOrder = { toOrderTop := inferInstanceAs (OrderTop Core.NaturalLogic.NLRelation), toOrderBot := inferInstanceAs (OrderBot Core.NaturalLogic.NLRelation) }

source

def Core.NaturalLogic.NLRelation.join :

NLRelation → NLRelation → NLRelation

Join operation ⋈ (@cite{icard-2012}, Lemma 1.5).

Given xRy and yR'z, determines the strongest relation x(R⋈R')z. This is the "join" in the relation algebra sense (not lattice join).

Equations

Instances For

source

theorem Core.NaturalLogic.NLRelation.join_identity_left (r : NLRelation) :

equiv.join r = r

≡ is the identity for join.

source

theorem Core.NaturalLogic.NLRelation.join_identity_right (r : NLRelation) :

r.join equiv = r

source

inductive Core.NaturalLogic.EntailmentSig :

Type

Entailment signature.

An entailment signature classifies a function by its algebraic properties with respect to ∨ and ∧. This unifies the separate monotonicity and additivity hierarchies into one 9-element lattice.

Symbol	Name	Properties
•	all	Preserves all 7 relations
+	mono	Monotone (= UE)
−	anti	Antitone (= DE)
⊕	additive	f(A∨B)=f(A)∨f(B), f(⊤)=⊤
◇	antiAdd	f(A∨B)=f(A)∧f(B)
⊞	mult	f(A∧B)=f(A)∧f(B), f(⊥)=⊥
⊟	antiMult	f(A∧B)=f(A)∨f(B), f(⊥)=⊤
⊕⊞	addMult	Additive + Multiplicative
◇⊟	antiAddMult	Anti-additive + Anti-mult

all : EntailmentSig
mono : EntailmentSig
anti : EntailmentSig
additive : EntailmentSig
antiAdd : EntailmentSig
mult : EntailmentSig
antiMult : EntailmentSig
addMult : EntailmentSig
antiAddMult : EntailmentSig

Instances For

source

instance Core.NaturalLogic.instDecidableEqEntailmentSig :

DecidableEq EntailmentSig

Equations

Core.NaturalLogic.instDecidableEqEntailmentSig x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Core.NaturalLogic.instBEqEntailmentSig.beq :

EntailmentSig → EntailmentSig → Bool

Equations

Core.NaturalLogic.instBEqEntailmentSig.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.NaturalLogic.instBEqEntailmentSig :

BEq EntailmentSig

Equations

Core.NaturalLogic.instBEqEntailmentSig = { beq := Core.NaturalLogic.instBEqEntailmentSig.beq }

source

instance Core.NaturalLogic.instReprEntailmentSig :

Repr EntailmentSig

Equations

Core.NaturalLogic.instReprEntailmentSig = { reprPrec := Core.NaturalLogic.instReprEntailmentSig.repr }

source

def Core.NaturalLogic.instReprEntailmentSig.repr :

EntailmentSig → ℕ → Std.Format

Equations

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

Instances For

source

def Core.NaturalLogic.EntailmentSig.refines :

EntailmentSig → EntailmentSig → Bool

Refinement ordering on entailment signatures.

The lattice has all at the bottom (most specific) and mono/anti at the top of their respective halves.

Equations

Instances For

source

instance Core.NaturalLogic.EntailmentSig.instLE :

LE EntailmentSig

Equations

Core.NaturalLogic.EntailmentSig.instLE = { le := fun (a b : Core.NaturalLogic.EntailmentSig) => a.refines b = true }

source

instance Core.NaturalLogic.EntailmentSig.instPreorder :

Preorder EntailmentSig

Equations

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

source

instance Core.NaturalLogic.EntailmentSig.instPartialOrder :

PartialOrder EntailmentSig

Equations

Core.NaturalLogic.EntailmentSig.instPartialOrder = { toPreorder := Core.NaturalLogic.EntailmentSig.instPreorder, le_antisymm := ⋯ }

source

instance Core.NaturalLogic.EntailmentSig.instBot :

Bot EntailmentSig

Equations

Core.NaturalLogic.EntailmentSig.instBot = { bot := Core.NaturalLogic.EntailmentSig.all }

source

instance Core.NaturalLogic.EntailmentSig.instOrderBot :

OrderBot EntailmentSig

Equations

Core.NaturalLogic.EntailmentSig.instOrderBot = { toBot := Core.NaturalLogic.EntailmentSig.instBot, bot_le := Core.NaturalLogic.EntailmentSig.instOrderBot._proof_1 }

source

def Core.NaturalLogic.EntailmentSig.project :

NLRelation → EntailmentSig → NLRelation

Projection of a NL relation through a function of given signature (@cite{icard-2012}, Lemma 2.4).

If xRy and f has signature φ, then f(x) [R]^φ f(y). Returns the ≪-maximal relation guaranteed to hold between f(x) and f(y).

The table follows from the algebraic definitions:

Additive: f(x∨y) = f(x)∨f(y), f(1)=1 → preserves ∨ → [∧]^⊕ = ∼ (cover from x∨y=1)
Multiplicative: f(x∧y) = f(x)∧f(y), f(0)=0 → preserves ∧ → [|]^⊞ = | (disjoint from x∧y=0)
Anti-additive: f(x∨y) = f(x)∧f(y), f(1)=0 → [∼]^◇ = | (from x∨y=1 ⟹ f(x)∧f(y)=0)
Anti-multiplicative: f(x∧y) = f(x)∨f(y), f(0)=1 → [|]^⊟ = ∼ (from x∧y=0 ⟹ f(x)∨f(y)=1)
Mono/anti alone: only preserves ⊑/⊒; ^, |, ∼ all weaken to #

Equations

Instances For

source

theorem Core.NaturalLogic.EntailmentSig.project_equiv (φ : EntailmentSig) :

project NLRelation.equiv φ = NLRelation.equiv

Projection preserves equiv for all signatures.

source

theorem Core.NaturalLogic.EntailmentSig.project_independent (φ : EntailmentSig) :

project NLRelation.independent φ = NLRelation.independent

Projection preserves independent for all signatures.

source

def Core.NaturalLogic.EntailmentSig.compose (ψ φ : EntailmentSig) :

EntailmentSig

Composition of entailment signatures (@cite{icard-2012}, Lemma 2.7).

Derived from project: compose(ψ, φ) is the unique signature whose projection table matches projecting through φ then ψ. This makes projection_composition hold by finite verification rather than requiring two independently maintained tables to agree.

The signature is identified by probing with forward and negation, which suffice to distinguish all 9 signatures (with all handled separately as the identity element).

Equations

One or more equations did not get rendered due to their size.
ψ.compose Core.NaturalLogic.EntailmentSig.all = ψ
Core.NaturalLogic.EntailmentSig.all.compose φ = φ

Instances For

source

theorem Core.NaturalLogic.EntailmentSig.compose_identity_left (s : EntailmentSig) :

all.compose s = s

all is the identity for composition.

source

theorem Core.NaturalLogic.EntailmentSig.compose_identity_right (s : EntailmentSig) :

s.compose all = s

source

theorem Core.NaturalLogic.EntailmentSig.compose_assoc (a b c : EntailmentSig) :

(a.compose b).compose c = a.compose (b.compose c)

Composition is associative.

source

instance Core.NaturalLogic.EntailmentSig.instMul :

Mul EntailmentSig

Equations

Core.NaturalLogic.EntailmentSig.instMul = { mul := Core.NaturalLogic.EntailmentSig.compose }

source

instance Core.NaturalLogic.EntailmentSig.instOne :

One EntailmentSig

Equations

Core.NaturalLogic.EntailmentSig.instOne = { one := Core.NaturalLogic.EntailmentSig.all }

source

instance Core.NaturalLogic.EntailmentSig.instMonoid :

Monoid EntailmentSig

Equations

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

source

inductive Core.NaturalLogic.DEStrength :

Type

Strength of downward entailingness.

Names the three levels of the DE hierarchy:

.weak = DE only (licenses weak NPIs: ever, any)
.antiAdditive = DE + ∨→∧ distributive (licenses strong NPIs: lift a finger)
.antiMorphic = AA + ∧→∨ distributive (= negation)

weak : DEStrength
antiAdditive : DEStrength
antiMorphic : DEStrength

Instances For

source

instance Core.NaturalLogic.instDecidableEqDEStrength :

DecidableEq DEStrength

Equations

Core.NaturalLogic.instDecidableEqDEStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Core.NaturalLogic.instBEqDEStrength.beq :

DEStrength → DEStrength → Bool

Equations

Core.NaturalLogic.instBEqDEStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.NaturalLogic.instBEqDEStrength :

BEq DEStrength

Equations

Core.NaturalLogic.instBEqDEStrength = { beq := Core.NaturalLogic.instBEqDEStrength.beq }

source

def Core.NaturalLogic.instReprDEStrength.repr :

DEStrength → ℕ → Std.Format

Equations

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

Instances For

source

instance Core.NaturalLogic.instReprDEStrength :

Repr DEStrength

Equations

Core.NaturalLogic.instReprDEStrength = { reprPrec := Core.NaturalLogic.instReprDEStrength.repr }

source

inductive Core.NaturalLogic.UEStrength :

Type

Strength of upward entailingness (dual of DEStrength).

Names the three levels of the UE hierarchy:

.weak = plain UE (monotone)
.multiplicative = UE + ∧-distributive
.additive = UE + ∨-distributive (strongest)

weak : UEStrength
multiplicative : UEStrength
additive : UEStrength

Instances For

source

instance Core.NaturalLogic.instDecidableEqUEStrength :

DecidableEq UEStrength

Equations

Core.NaturalLogic.instDecidableEqUEStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Core.NaturalLogic.instBEqUEStrength.beq :

UEStrength → UEStrength → Bool

Equations

Core.NaturalLogic.instBEqUEStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.NaturalLogic.instBEqUEStrength :

BEq UEStrength

Equations

Core.NaturalLogic.instBEqUEStrength = { beq := Core.NaturalLogic.instBEqUEStrength.beq }

source

def Core.NaturalLogic.instReprUEStrength.repr :

UEStrength → ℕ → Std.Format

Equations

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

Instances For

source

instance Core.NaturalLogic.instReprUEStrength :

Repr UEStrength

Equations

Core.NaturalLogic.instReprUEStrength = { reprPrec := Core.NaturalLogic.instReprUEStrength.repr }

source

def Core.NaturalLogic.strengthSufficient (contextStrength requiredStrength : DEStrength) :

Bool

Check if a context's DE strength is sufficient for an NPI.

strengthSufficient contextStrength requiredStrength returns true when contextStrength ≥ requiredStrength in the Zwarts hierarchy.

Equations

Instances For

source

def Core.NaturalLogic.EntailmentSig.toDEStrength (φ : EntailmentSig) :

Option DEStrength

Map an entailment signature to DE strength, derived from project.

A signature is DE iff it reverses forward entailment: [⊑]^φ = ⊒. Within the DE side, anti-additivity is detected by [∼]^φ = | (the ∨→∧ swap: x∨y=1 ⟹ f(x)∧f(y)=0), and anti-morphism additionally requires [|]^φ = ∼ (the ∧→∨ swap).

Returns none for UE-side signatures.

Equations

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

Instances For

source

def Core.NaturalLogic.EntailmentSig.toUEStrength (φ : EntailmentSig) :

Option UEStrength

Map an entailment signature to UE strength, derived from project.

A signature is UE iff it preserves forward entailment: [⊑]^φ = ⊑. Additivity is detected by [∼]^φ = ∼ (∨-preservation: x∨y=1 ⟹ f(x)∨f(y)=1), and multiplicativity by [|]^φ = | (∧-preservation: x∧y=0 ⟹ f(x)∧f(y)=0).

Returns none for DE-side signatures.

Equations

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

Instances For

source

inductive Core.NaturalLogic.ContextPolarity :

Type

Whether a context preserves or reverses entailment direction.

This is a coarsening of EntailmentSig: all UE-side signatures collapse to .upward, all DE-side signatures collapse to .downward. Contexts that are neither monotone nor antitone (e.g., "exactly n") are .nonMonotonic.

Used by:

NeoGricean: determines which alternatives count as "stronger"
RSA: polarity-sensitive inference
Any theory computing scalar implicatures

upward : ContextPolarity
downward : ContextPolarity
nonMonotonic : ContextPolarity

Instances For

source

instance Core.NaturalLogic.instDecidableEqContextPolarity :

DecidableEq ContextPolarity

Equations

Core.NaturalLogic.instDecidableEqContextPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Core.NaturalLogic.instBEqContextPolarity :

BEq ContextPolarity

Equations

Core.NaturalLogic.instBEqContextPolarity = { beq := Core.NaturalLogic.instBEqContextPolarity.beq }

source

def Core.NaturalLogic.instBEqContextPolarity.beq :

ContextPolarity → ContextPolarity → Bool

Equations

Core.NaturalLogic.instBEqContextPolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

def Core.NaturalLogic.instReprContextPolarity.repr :

ContextPolarity → ℕ → Std.Format

Equations

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

Instances For

source

instance Core.NaturalLogic.instReprContextPolarity :

Repr ContextPolarity

Equations

Core.NaturalLogic.instReprContextPolarity = { reprPrec := Core.NaturalLogic.instReprContextPolarity.repr }

source

def Core.NaturalLogic.ContextPolarity.compose :

ContextPolarity → ContextPolarity → ContextPolarity

Compose context polarities.

This is the coarse composition table derived from the EntailmentSig monoid: UE ∘ UE = UE, DE ∘ DE = UE (double negation), UE ∘ DE = DE, DE ∘ UE = DE. Any composition involving nonMonotonic yields nonMonotonic.

Equations

Instances For

source

def Core.NaturalLogic.EntailmentSig.toContextPolarity (φ : EntailmentSig) :

ContextPolarity

Map an entailment signature to the coarser ContextPolarity type, derived from project.

A signature is UE iff it preserves forward entailment ([⊑]^φ = ⊑), DE iff it reverses it ([⊑]^φ = ⊒).

Equations

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

Instances For

source

theorem Core.NaturalLogic.EntailmentSig.toContextPolarity_compose (φ ψ : EntailmentSig) :

(φ * ψ).toContextPolarity = φ.toContextPolarity.compose ψ.toContextPolarity

toContextPolarity is a monoid homomorphism: composing signatures then coarsening gives the same result as coarsening then composing polarities.

This theorem connects the fine-grained EntailmentSig monoid to the coarse ContextPolarity composition, ensuring the two systems can never disagree.

source

def Core.NaturalLogic.EntailmentSig.contextProjectivity (path : List EntailmentSig) :

EntailmentSig

Compute the projectivity signature of a context from the signatures along the path from the target position to the root (@cite{icard-2012}, Definition 2.9).

Given a parse tree and a target position (e.g., "dangerous" in "Every job that involves a giant squid is dangerous"), the path collects the top signature of each node from the target up to the root. The composed signature is List.prod, using the Monoid instance.

Example from Icard §3.2: path = [⊞, ⊕, ◇] (top(is) ∘ top(involves) ∘ top(every_restrictor)) contextProjectivity path = ◇ (anti-additive)

Equations

Core.NaturalLogic.EntailmentSig.contextProjectivity path = path.prod

Instances For

source

def Core.NaturalLogic.EntailmentSig.projectThrough (R : NLRelation) (path : List EntailmentSig) :

NLRelation

Project a NL relation through a context given by its signature path. Combines contextProjectivity with project.

Equations

Core.NaturalLogic.EntailmentSig.projectThrough R path = Core.NaturalLogic.EntailmentSig.project R (Core.NaturalLogic.EntailmentSig.contextProjectivity path)

Instances For

source

theorem Core.NaturalLogic.projection_composition (R : NLRelation) (φ ψ : EntailmentSig) :

EntailmentSig.project (EntailmentSig.project R φ) ψ = EntailmentSig.project R (ψ.compose φ)

Projection composition (@cite{icard-2012}, Corollary 2.12).

Projecting through f then g is the same as projecting through g∘f. This is the compositionality principle: nested function application corresponds to signature composition.

Since compose is derived from project (via fromProjectionPair), the only content of this theorem is that the two probe relations (forward, negation) suffice to determine the full projection table.

source

theorem Core.NaturalLogic.de_signature_licenses_weak_npi (σ : EntailmentSig) :

σ.toContextPolarity = ContextPolarity.downward → σ.toDEStrength.isSome = true

Any DE-side signature licenses weak NPIs.

This connects Icard's signature lattice to @cite{ladusaw-1980}: a signature on the DE side (anti, antiAdd, antiMult, antiAddMult) creates a DE context, which is sufficient for weak NPI licensing.

source

theorem Core.NaturalLogic.strong_npi_requires_antiadditive (σ : EntailmentSig) :

σ.toDEStrength = some DEStrength.antiAdditive ∨ σ.toDEStrength = some DEStrength.antiMorphic → σ.toContextPolarity = ContextPolarity.downward

Anti-additive or stronger signature licenses strong NPIs.

Strong NPIs (lift a finger, in weeks) require anti-additive contexts. In Icard's system, this corresponds to signatures antiAdd, antiAddMult — but NOT plain anti or antiMult.

source

def Core.NaturalLogic.negationSig :

EntailmentSig

Negation has the anti-morphism signature ◇⊟ (strongest DE signature).

Equations

Core.NaturalLogic.negationSig = Core.NaturalLogic.EntailmentSig.antiAddMult

Instances For

Documentation

Linglib.Core.Logic.NaturalLogic

Natural Logic Relations and Entailment Signatures #

Contents #

Key operations #

Algebraic structure #