Documentation

Linglib.Logic.Natural.Basic

The natural-logic relation algebra #

This file defines the seven natural-logic relations between denotations (≡, ⊑, ⊒, ^, |, ⌣, #) and the nine entailment signatures of [Ica12], with the operations of the projectivity calculus: chaining two relations, projecting a relation through a function of known signature, and composing signatures.

A relation is read non-strictly, as the conjunction of its constraint atoms: distinct relations overlap, and R ≤ R' iff R entails R', by reverse inclusion of constraint sets. The mutually exclusive seven of [MCM09] are the strict refinements. Signatures are ordered likewise by reverse inclusion of property sets; # and • are the tops, and there is no bottom.

Main declarations #

Relation: the seven relations, a monoid under Relation.join with identity equiv and absorbing element independent.
Relation.constraints: a relation as a conjunction of atomic lattice constraints; the source of the implication order.
Signature: the nine signatures, a monoid under Signature.compose with identity addMult and absorbing element all.
Signature.project: projection of a relation through a signature — an action of the signature monoid on the relations (MulAction Signature Relation).
Signature.contextProjectivity: the signature of a position, as the monoid product along its path.
Signature.sign: the coarse upward/downward quotient, a SignType, and a monoid homomorphism (Signature.signHom); negation's signature has the sign of the negative Polarity (Signature.sign_antiAddMult).

Implementation notes #

compose is derived from project by probing at the relations forward and negation, so projection_composition holds by construction. Associativity of join is printed in neither source and is verified by decide. The tables are certified semantically in Logic/Natural/Soundness.lean (Relation.Holds.join, the soundFor_* rows) and shown tight in Logic/Natural/Completeness.lean, which also derives the seven relations as the nondegenerately realizable constraint conjunctions.

References #

[Ica12] — the projectivity calculus: the relations, signatures, and tables this file implements.
[MCM09] — the extended natural-logic model; its §3 join is exact relation composition, union-valued outside the seven.

The seven relations #

inductive NaturalLogic.Relation :

The seven natural-logic relations between denotations.

equiv : Relation
Equivalence ≡ holds when the denotations coincide (couch / sofa).
forward : Relation
Forward entailment ⊑ holds when A ⊆ B (dog / animal).
reverse : Relation
Reverse entailment ⊒ holds when A ⊇ B (animal / dog).
negation : Relation
Negation ^ holds when the denotations are disjoint and exhaustive (happy / unhappy).
alternation : Relation
Alternation | holds when the denotations are disjoint (cat / dog).
cover : Relation
Cover ⌣ holds when the denotations are exhaustive (animal / nondog).
independent : Relation
Independence # imposes no constraint (hungry / tall).

Instances For

@[instance_reducible]

instance NaturalLogic.instDecidableEqRelation :

DecidableEq Relation

Equations

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

@[instance_reducible]

instance NaturalLogic.instFintypeRelation :

Fintype Relation

Equations

NaturalLogic.instFintypeRelation = { elems := { val := ↑NaturalLogic.Relation.enumList, nodup := NaturalLogic.Relation.enumList_nodup }, complete := NaturalLogic.instFintypeRelation._proof_1 }

@[instance_reducible]

instance NaturalLogic.instReprRelation :

Equations

NaturalLogic.instReprRelation = { reprPrec := NaturalLogic.instReprRelation.repr }

def NaturalLogic.instReprRelation.repr :

Relation → ℕ → Std.Format

Equations

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

Instances For

inductive NaturalLogic.Relation.Atom :

The atomic lattice constraints a relation can impose ([Ica12] Definition 1.2).

le : Atom
x ≤ y.
ge : Atom
y ≤ x.
disjoint : Atom
x ⊓ y = ⊥.
codisjoint : Atom
x ⊔ y = ⊤.

Instances For

@[instance_reducible]

instance NaturalLogic.Relation.instDecidableEqAtom :

DecidableEq Atom

Equations

NaturalLogic.Relation.instDecidableEqAtom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NaturalLogic.Relation.instFintypeAtom :

Fintype Atom

Equations

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

def NaturalLogic.Relation.instReprAtom.repr :

Atom → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance NaturalLogic.Relation.instReprAtom :

Repr Atom

Equations

NaturalLogic.Relation.instReprAtom = { reprPrec := NaturalLogic.Relation.instReprAtom.repr }

def NaturalLogic.Relation.constraints :

Relation → Finset Atom

The constraint set of a relation: each relation is the conjunction of its atoms (≡ = {le, ge}, ^ = {disjoint, codisjoint}, # = ∅), ≤ is reverse inclusion of constraint sets, and Holds is their conjunction (Relation.holds_iff in Logic/Natural/Soundness.lean). Exactly the seven images are nondegenerately realizable among the sixteen subsets (Relation.mem_range_constraints_iff in Logic/Natural/Completeness.lean).

Equations

Instances For

theorem NaturalLogic.Relation.constraints_injective :

Function.Injective constraints

@[instance_reducible]

instance NaturalLogic.Relation.instPartialOrder :

PartialOrder Relation

The implication order ([Ica12]'s ≪): R ≤ R' iff xRy entails xR'y — reverse inclusion of constraint sets, certified semantically by Relation.Holds.of_le. # is the top; there is no bottom: the two diamonds (≡ over ⊑/⊒, ^ over |/⌣) meet only at #, since x = y makes x,y neither disjoint nor exhaustive.

Equations

NaturalLogic.Relation.instPartialOrder = PartialOrder.lift (fun (R : NaturalLogic.Relation) => OrderDual.toDual R.constraints) NaturalLogic.Relation.instPartialOrder._proof_1

theorem NaturalLogic.Relation.le_iff {R R' : Relation} :

R ≤ R' ↔ R'.constraints ⊆ R.constraints

@[instance_reducible]

instance NaturalLogic.Relation.instDecidableLE :

DecidableLE Relation

Equations

x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝.constraints ⊆ x✝¹.constraints) ⋯

@[instance_reducible]

instance NaturalLogic.Relation.instOrderTop :

OrderTop Relation

Equations

NaturalLogic.Relation.instOrderTop = { top := NaturalLogic.Relation.independent, le_top := NaturalLogic.Relation.instOrderTop._proof_1 }

def NaturalLogic.Relation.join :

Relation → Relation → Relation

Join operation ⋈ ([Ica12], Lemma 1.5): given xRy and yR'z, the strongest relation guaranteed between x and z — relation-algebra join, not lattice join. The table is derived from the non-strict Holds reading, certified sound cell-by-cell by Relation.Holds.join in Logic/Natural/Soundness.lean, and tight by Relation.isLeast_join in Logic/Natural/Completeness.lean: each cell is the least relation sound for the chaining ([Ica12]'s Definition 1.4; [MCM09]'s §3 join is instead exact relation composition, valued in union relations outside the seven on 17 of the 49 cells — this table is its best single-relation weakening).

Equations

Instances For

@[instance_reducible]

instance NaturalLogic.Relation.instMul :

Equations

NaturalLogic.Relation.instMul = { mul := NaturalLogic.Relation.join }

@[instance_reducible]

instance NaturalLogic.Relation.instOne :

Equations

NaturalLogic.Relation.instOne = { one := NaturalLogic.Relation.equiv }

@[instance_reducible]

instance NaturalLogic.Relation.instMonoid :

Monoid Relation

The relations form a monoid under ⋈ with identity ≡. The identity and absorption laws are printed in [Ica12] (p. 710); associativity appears in neither [Ica12] nor [MCM09] and is verified here by kernel decide. Not commutative: ^ ⋈ ⌣ = ⊑ but ⌣ ⋈ ^ = ⊒ (chaining is directional).

Equations

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

@[simp]

theorem NaturalLogic.Relation.top_mul (r : Relation) :

⊤ * r = ⊤

# absorbs on the left ([Ica12] p. 710).

@[simp]

theorem NaturalLogic.Relation.mul_top (r : Relation) :

r * ⊤ = ⊤

# absorbs on the right ([Ica12] p. 710).

Entailment signatures #

inductive NaturalLogic.Signature :

The function classes a relation can be projected through, from arbitrary (•) to anti-morphism (◇⊟).

all : Signature
An arbitrary function (•), projecting every relation to #.
mono : Signature
A monotone function (+, upward entailing).
anti : Signature
An antitone function (−, downward entailing).
additive : Signature
An additive function (⊕), preserving joins.
antiAdd : Signature
An anti-additive function (◇), turning joins into meets.
mult : Signature
A multiplicative function (⊞), preserving meets.
antiMult : Signature
An anti-multiplicative function (⊟), turning meets into joins.
addMult : Signature
A morphism (⊕⊞), additive and multiplicative.
antiAddMult : Signature
An anti-morphism (◇⊟), anti-additive and anti-multiplicative.

Instances For

@[instance_reducible]

instance NaturalLogic.instDecidableEqSignature :

DecidableEq Signature

Equations

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

@[instance_reducible]

instance NaturalLogic.instFintypeSignature :

Fintype Signature

Equations

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

@[instance_reducible]

instance NaturalLogic.instReprSignature :

Equations

NaturalLogic.instReprSignature = { reprPrec := NaturalLogic.instReprSignature.repr }

def NaturalLogic.instReprSignature.repr :

Signature → ℕ → Std.Format

Equations

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

Instances For

inductive NaturalLogic.Signature.Property :

The function properties a signature can assert, closed under implication (an additive function is monotone, so ⊕'s set contains monotone).

monotone : Property
Preserves ≤.
antitone : Property
Reverses ≤.
additive : Property
Preserves ⊔.
multiplicative : Property
Preserves ⊓.
antiAdditive : Property
Sends ⊔ to ⊓.
antiMultiplicative : Property
Sends ⊓ to ⊔.

Instances For

@[instance_reducible]

instance NaturalLogic.Signature.instDecidableEqProperty :

DecidableEq Property

Equations

NaturalLogic.Signature.instDecidableEqProperty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance NaturalLogic.Signature.instFintypeProperty :

Fintype Property

Equations

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

@[instance_reducible]

instance NaturalLogic.Signature.instReprProperty :

Equations

NaturalLogic.Signature.instReprProperty = { reprPrec := NaturalLogic.Signature.instReprProperty.repr }

def NaturalLogic.Signature.instReprProperty.repr :

Property → ℕ → Std.Format

Equations

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

Instances For

def NaturalLogic.Signature.properties :

Signature → Finset Property

The property set of a signature: ≤ is reverse inclusion, so addMult/antiAddMult are the most specific elements of their halves and all (•, no property) is the top.

Equations

Instances For

theorem NaturalLogic.Signature.properties_injective :

Function.Injective properties

@[instance_reducible]

instance NaturalLogic.Signature.instPartialOrder :

PartialOrder Signature

The refinement order ([Ica12]'s ≼, §2.2): σ ≤ τ iff every σ-function is a τ-function — reverse inclusion of property sets, certified semantically by Signature.SoundFor.of_le in Logic/Natural/Soundness.lean.

Equations

NaturalLogic.Signature.instPartialOrder = PartialOrder.lift (fun (σ : NaturalLogic.Signature) => OrderDual.toDual σ.properties) NaturalLogic.Signature.instPartialOrder._proof_1

theorem NaturalLogic.Signature.le_iff {σ τ : Signature} :

σ ≤ τ ↔ τ.properties ⊆ σ.properties

@[instance_reducible]

instance NaturalLogic.Signature.instDecidableLE :

DecidableLE Signature

Equations

x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝.properties ⊆ x✝¹.properties) ⋯

@[instance_reducible]

instance NaturalLogic.Signature.instOrderTop :

OrderTop Signature

Equations

NaturalLogic.Signature.instOrderTop = { top := NaturalLogic.Signature.all, le_top := NaturalLogic.Signature.instOrderTop._proof_1 }

def NaturalLogic.Signature.project :

Relation → Signature → Relation

The projection of a relation through a function of the given signature ([Ica12] Definition 2.3, computed by his Lemma 2.4): the strongest relation guaranteed between f x and f y when x R y and f has signature σ. The rows are certified sound against the function classes in Logic/Natural/Soundness.lean (soundFor_*) and tight by Signature.isLeast_project in Logic/Natural/Completeness.lean. One cell deviates from the printed table: [Ica12] prints [R]^• = # for all R (p. 715), but every function preserves equality, so his Definition 2.3 forces [≡]^• = ≡.

Equations

Instances For

theorem NaturalLogic.Signature.project_equiv (φ : Signature) :

project Relation.equiv φ = Relation.equiv

Every signature except • preserves equiv (• is the class of arbitrary functions, which need not respect equivalence).

theorem NaturalLogic.Signature.project_independent (φ : Signature) :

project Relation.independent φ = Relation.independent

Projection preserves independent for all signatures.

def NaturalLogic.Signature.fromProjectionPair :

Relation → Relation → Signature

Recover an entailment signature from its projection of forward and negation. These two probes uniquely identify each signature (up to •'s probe pair being (#, #)).

Equations

Instances For

def NaturalLogic.Signature.compose (ψ φ : Signature) :

Composition of entailment signatures ([Ica12], 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 (• included: its probe pair is (#, #), which makes it absorbing, [Ica12] p. 716).

Equations

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

Instances For

theorem NaturalLogic.Signature.compose_identity_left (s : Signature) :

addMult.compose s = s

addMult (⊕⊞, the morphism class) is the identity for composition ([Ica12] Lemma 2.7).

theorem NaturalLogic.Signature.compose_identity_right (s : Signature) :

s.compose addMult = s

theorem NaturalLogic.Signature.compose_all_left (s : Signature) :

all.compose s = all

• is absorbing: composing with the no-property class yields the no-property class ([Ica12] p. 716: φ ∘ • = • = • ∘ φ).

theorem NaturalLogic.Signature.compose_all_right (s : Signature) :

s.compose all = all

theorem NaturalLogic.Signature.compose_assoc (a b c : Signature) :

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

Composition is associative.

@[instance_reducible]

instance NaturalLogic.Signature.instMul :

Equations

NaturalLogic.Signature.instMul = { mul := NaturalLogic.Signature.compose }

@[instance_reducible]

instance NaturalLogic.Signature.instOne :

Equations

NaturalLogic.Signature.instOne = { one := NaturalLogic.Signature.addMult }

@[instance_reducible]

instance NaturalLogic.Signature.instMonoid :

Monoid Signature

Equations

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

The sign of a signature #

def NaturalLogic.Signature.sign (φ : Signature) :

SignType

The sign of a signature, [Ica12]'s coarse upward/downward quotient: 1 for an upward-entailing context, which preserves forward entailment ([⊑]^φ = ⊑), -1 for a downward-entailing one, which reverses it ([⊑]^φ = ⊒), and 0 when neither is guaranteed, for a non-monotone context such as exactly n or an arbitrary one.

Equations

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

Instances For

theorem NaturalLogic.Signature.sign_mul (φ ψ : Signature) :

(φ * ψ).sign = φ.sign * ψ.sign

Composing signatures then taking the sign gives the product of the signs.

def NaturalLogic.Signature.signHom :

Signature →* SignType

sign as a monoid homomorphism, so that the signature monoid and its coarse quotient can never disagree.

Equations

NaturalLogic.Signature.signHom = { toFun := NaturalLogic.Signature.sign, map_one' := NaturalLogic.Signature.signHom._proof_1, map_mul' := NaturalLogic.Signature.sign_mul }

Instances For

theorem NaturalLogic.Signature.sign_antiAddMult :

antiAddMult.sign = ↑Polarity.negative

The anti-morphism signature of sentential negation has the sign of the negative polarity.

def NaturalLogic.Signature.contextProjectivity (path : List Signature) :

The projectivity signature of a position, as the monoid product of the signatures along its path, listed root-first (outermost context first): [Ica12]'s marking recursion pro(s(u)) = top(s) ∘ pro(u) (Definition 2.9). Under the projection action, mul_smul applies the innermost — last — signature to the relation first. For example, contextProjectivity [.antiAdd, .addMult] = .antiAdd: an intersective modifier inside a no-restrictor leaves the position anti-additive.

Equations

NaturalLogic.Signature.contextProjectivity path = path.prod

Instances For

Projection composition #

theorem NaturalLogic.projection_composition (R : Relation) (φ ψ : Signature) :

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

Projecting through φ and then ψ projects through the composite signature ([Ica12] Definition 2.6 and Lemma 2.7) — the mul_smul law of MulAction Signature Relation. Since compose is derived from project by probing at forward and negation, the content is that the two probes determine the whole table.

@[instance_reducible]

instance NaturalLogic.instSMulSignatureRelation :

SMul Signature Relation

Equations

NaturalLogic.instSMulSignatureRelation = { smul := fun (σ : NaturalLogic.Signature) (R : NaturalLogic.Relation) => NaturalLogic.Signature.project R σ }

@[simp]

theorem NaturalLogic.Signature.smul_def (σ : Signature) (R : Relation) :

σ • R = project R σ

@[instance_reducible]

instance NaturalLogic.instMulActionSignatureRelation :

MulAction Signature Relation

Projection is an action of the signature monoid on the relations: projection_composition is the mul_smul law.

Equations

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

The negation signature #

def NaturalLogic.negationSignature :

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

Equations

NaturalLogic.negationSignature = NaturalLogic.Signature.antiAddMult

Instances For