Soundness of the projectivity calculus

Semantic grounding for [Ica12]'s projectivity machinery: NLRelation gets its lattice content (Holds, his Definition 1.2 — non-exclusive equations, so ⊑ is plain ≤), and a signature is sound for a function (EntailmentSig.SoundFor) when the function projects every relation as the signature's project row says (his Lemma 2.5). The characterization theorems discharge each row from the property family in Entailment — the additive-family rows need the IsCompletely* unit conditions, exactly as Icard's tables assume; the soundness proofs go through over bounded lattices, not just his Boolean lattices.

SoundFor.comp and soundFor_contextProjectivity certify EntailmentSig.compose and path projection against function composition (his Lemma 2.7 and Proposition 2.10): study-file locality computations over the enum become corollaries of facts about actual context functions.

Main declarations

• NLRelation.Holds: lattice content of the seven relations;
• EntailmentSig.SoundFor: σ's projection row is sound for f;
• soundFor_mono_iff, soundFor_anti_iff: the monotone rows, as iffs;
• soundFor_additive … soundFor_antiAddMult: the algebraic rows, from IsCompletely* hypotheses (sound direction; the converses fail — projection rows are class-maximal, not function-characterizing);
• SoundFor.comp: soundness composes along EntailmentSig.compose;
• soundFor_contextProjectivity: soundness folds along a signature path.

Order soundness

With the Refines orders carrying their [Ica12] readings (.all = •, the no-property top; ≡ not below the exclusion relations), both orders are certified here: NLRelation.Holds.of_refines (relation-level implication) and EntailmentSig.SoundFor.of_refines (a more specific signature's soundness implies a less specific one's), via the projection monotonicity EntailmentSig.project_refines. soundFor_all holds unconditionally — every function realizes the no-property row.

Lattice content of the relations

def NaturalLogic.NLRelation.Holds {α : Type u_1} [Lattice α] [BoundedOrder α] : NLRelation → α → α → Prop

The lattice content of a natural-logic relation ([Ica12] Definition 1.2), in mathlib's complementation vocabulary: negation is IsCompl, alternation is Disjoint, cover is Codisjoint; forward is non-strict ≤ (the enum comments' ⊂ follows MacCartney's exclusive reading, which the projectivity tables do not need).

Equations

• NaturalLogic.NLRelation.equiv.Holds = fun (x1 x2 : α) => x1 = x2
• NaturalLogic.NLRelation.forward.Holds = fun (x1 x2 : α) => x1 ≤ x2
• NaturalLogic.NLRelation.reverse.Holds = fun (x1 x2 : α) => x1 ≥ x2
• NaturalLogic.NLRelation.negation.Holds = IsCompl
• NaturalLogic.NLRelation.alternation.Holds = Disjoint
• NaturalLogic.NLRelation.cover.Holds = Codisjoint
• NaturalLogic.NLRelation.independent.Holds = fun (x x_1 : α) => True

Soundness of a signature for a function

def NaturalLogic.EntailmentSig.SoundFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (σ : EntailmentSig) (f : α → β) : Prop

A signature σ is sound for f when f projects every relation as σ's row of the projection table says ([Ica12] Lemma 2.5: every φ-function projects R to [R]^φ).

Equations

• σ.SoundFor f = ∀ (R : NaturalLogic.NLRelation) (x y : α), R.Holds x y → (NaturalLogic.EntailmentSig.project R σ).Holds (f x) (f y)

theorem NaturalLogic.soundFor_mono_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} : EntailmentSig.mono.SoundFor f ↔ Monotone f

The .mono row is sound for exactly the monotone functions.

theorem NaturalLogic.soundFor_anti_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} : EntailmentSig.anti.SoundFor f ↔ Antitone f

The .anti row is sound for exactly the antitone functions.

theorem NaturalLogic.soundFor_additive {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : Entailment.IsCompletelyAdditive f) : EntailmentSig.additive.SoundFor f

The .additive row is sound for completely additive functions.

theorem NaturalLogic.soundFor_mult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : Entailment.IsCompletelyMultiplicative f) : EntailmentSig.mult.SoundFor f

The .mult row is sound for completely multiplicative functions.

theorem NaturalLogic.soundFor_antiAdd {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : Entailment.IsCompletelyAntiAdditive f) : EntailmentSig.antiAdd.SoundFor f

The .antiAdd row is sound for completely anti-additive functions.

theorem NaturalLogic.soundFor_antiMult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : Entailment.IsCompletelyAntiMultiplicative f) : EntailmentSig.antiMult.SoundFor f

The .antiMult row is sound for completely anti-multiplicative functions.

theorem NaturalLogic.soundFor_addMult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (hadd : Entailment.IsCompletelyAdditive f) (hmult : Entailment.IsCompletelyMultiplicative f) : EntailmentSig.addMult.SoundFor f

The .addMult row (preserve everything) is sound for morphisms: completely additive and completely multiplicative functions.

theorem NaturalLogic.soundFor_antiAddMult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (haa : Entailment.IsCompletelyAntiAdditive f) (ham : Entailment.IsCompletelyAntiMultiplicative f) : EntailmentSig.antiAddMult.SoundFor f

The .antiAddMult row is sound for anti-morphisms: completely anti-additive and completely anti-multiplicative functions. This is the sentential-negation row — the semantic content of "double negation is a morphism".

theorem NaturalLogic.soundFor_all {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (f : α → β) : EntailmentSig.all.SoundFor f

Every function realizes the • row: .all is the no-property signature, projecting every relation to #.

theorem NaturalLogic.NLRelation.Holds.of_refines {β : Type u_2} [Lattice β] [BoundedOrder β] {R R' : NLRelation} {u v : β} (h : R.Holds u v) (href : R.Refines R') : R'.Holds u v

Relation-level order soundness: Refines is the implication order on the lattice content ([Ica12] §1).

theorem NaturalLogic.EntailmentSig.project_refines {σ τ : EntailmentSig} (h : σ.Refines τ) (R : NLRelation) : (project R σ).Refines (project R τ)

Projection is monotone in the signature order: a more specific signature projects every relation at least as informatively.

theorem NaturalLogic.EntailmentSig.SoundFor.of_refines {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ τ : EntailmentSig} {f : α → β} (h : σ.SoundFor f) (hστ : σ.Refines τ) : τ.SoundFor f

Signature-order soundness: if σ refines τ (every σ-function is a τ-function), σ-soundness implies τ-soundness. This is the theorem that makes the Refines order mean class inclusion.

Composition and paths

theorem NaturalLogic.EntailmentSig.SoundFor.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] {ψ φ : EntailmentSig} {f : β → γ} {g : α → β} (hf : ψ.SoundFor f) (hg : φ.SoundFor g) : (ψ * φ).SoundFor (f ∘ g)

Soundness composes along EntailmentSig.compose ([Ica12] Lemma 2.7 + Proposition 2.10): if ψ is sound for the outer function and φ for the inner one, ψ * φ is sound for the composite. This is the theorem that certifies the enum-level compose table against actual context functions.

theorem NaturalLogic.soundFor_addMult_id {α : Type u_1} [Lattice α] [BoundedOrder α] : EntailmentSig.addMult.SoundFor id

The identity context is sound for the identity signature .addMult.

theorem NaturalLogic.soundFor_contextProjectivity {α : Type u_1} [Lattice α] [BoundedOrder α] (l : List (EntailmentSig × (α → α))) : (∀ p ∈ l, p.1.SoundFor p.2) → (EntailmentSig.contextProjectivity (List.map Prod.fst l)).SoundFor (List.foldr (fun (x1 x2 : α → α) => x1 ∘ x2) id (List.map Prod.snd l))

Path soundness: a path of (signature, context) pairs, each sound, yields a context sound for contextProjectivity of the signature path — the semantic counterpart of [Ica12] Definition 2.9's marking algorithm. Signatures are listed outermost-first, matching contextProjectivity.

Worked instance: double negation is a morphism, semantically

pnot is completely anti-additive and completely anti-multiplicative, so the .antiAddMult row is sound for it; composing it with itself certifies the enum fact ◇⊟ ∘ ◇⊟ = ⊕⊞ against the actual function pnot ∘ pnot.

theorem NaturalLogic.pnot_isCompletelyAntiAdditive : Entailment.IsCompletelyAntiAdditive Entailment.pnot

theorem NaturalLogic.pnot_isCompletelyAntiMultiplicative : Entailment.IsCompletelyAntiMultiplicative Entailment.pnot

theorem NaturalLogic.pnot_soundFor_antiAddMult : EntailmentSig.antiAddMult.SoundFor Entailment.pnot

Negation realizes the anti-morphism row.