Completeness of the projectivity calculus

This file proves the converses to Logic/Natural/Soundness.lean: the join and projection tables are tight, the seven relations are exactly the nondegenerately realizable conjunctions of constraint atoms, and the refinement order on signatures coincides with inclusion of function classes.

Tightness ([Ica12]'s Lemma 1.5, as an equality) has countermodels already on the three-atom Boolean algebra Finset (Fin 3). The classification is [MCM09] §2's sixteen-class partition, following Sánchez Valencia: the nine subsets outside the range of Relation.constraints force an argument to ⊥ or ⊤ in every bounded lattice.

Main declarations

• Relation.isLeast_join, Relation.join_le_iff: each join cell is the least sound chaining ([Ica12] Definition 1.4).
• Relation.mem_range_constraints_of_holds: a constraint set realized by a nondegenerate pair is one of the seven.
• Relation.mem_range_constraints_iff: the classification, as an iff against realizability on Finset (Fin 3).
• Relation.exists_isLeast_holds: [Ica12]'s Lemma 1.3 — any nondegenerate pair stands in a strongest relation — on any bounded lattice.
• Signature.isLeast_project: each projection cell is the least relation sound for the signature's function class ([Ica12] Definition 2.3), with countermodels on the two-element Boolean algebra.
• Signature.le_iff_holdsFor: the refinement order is inclusion of function classes — [Ica12]'s semantic definition of ≼, recovered.
• Signature.isLeast_compose, Signature.holdsFor_comp: composition is the least signature covering composites ([Ica12] Definition 2.6).

Implementation notes

The nine signatures are not an exhaustive classification of realizable property profiles: the constant-⊤ function is simultaneously monotone, antitone, completely additive, and completely anti-multiplicative, and {+, −, ⊕, ⊟} is no signature's property set. The signatures are the downward-closed profiles [Ica12] names, each tight for its own row.

References

• [Ica12] — Definitions 1.4, 2.3, and 2.6, Lemmas 1.3, 1.5, and 2.4.
• [MCM09] — §2's sixteen-class partition, following Sánchez Valencia.

Tightness of the join table

theorem NaturalLogic.Relation.isLeast_join (R S : Relation) : IsLeast {T : Relation | ∀ (x y z : Finset (Fin 3)), R.Holds x y → S.Holds y z → T.Holds x z} (R.join S)

Tightness of the join table ([Ica12] Lemma 1.5 is an equality): R.join S is the least — strongest — relation sound for chaining R then S, already over the three-atom Boolean algebra. Soundness over any bounded distributive lattice is Relation.Holds.join; conversely any T sound on Finset (Fin 3) alone weakens the table entry.

Why seven relations

theorem NaturalLogic.Relation.mem_range_constraints_of_holds {α : Type u_1} [Lattice α] [BoundedOrder α] {s : Finset Atom} {x y : α} (h : ∀ a ∈ s, a.Holds x y) (hx : x ≠ ⊥) (hx' : x ≠ ⊤) (hy : y ≠ ⊥) (hy' : y ≠ ⊤) : s ∈ Set.range constraints

Completeness half of the classification: a conjunction of atomic constraints satisfied by a nondegenerate pair, in any bounded lattice, is the constraint set of one of the seven relations.

theorem NaturalLogic.Relation.mem_range_constraints_iff {s : Finset Atom} : s ∈ Set.range constraints ↔ ∃ (x : Finset (Fin 3)) (y : Finset (Fin 3)), x ≠ ⊥ ∧ x ≠ ⊤ ∧ y ≠ ⊥ ∧ y ≠ ⊤ ∧ ∀ a ∈ s, a.Holds x y

Why seven: of the sixteen conjunctions of atomic constraints, exactly the seven in the range of constraints are nondegenerately realizable — here already on the three-atom Boolean algebra; the other nine force an argument to ⊥ or ⊤ on every bounded lattice ([MCM09]'s nontrivial-denotation proviso, [Ica12] §1).

The join characterization and the strongest relation

theorem NaturalLogic.Relation.join_le_iff {R S T : Relation} : R.join S ≤ T ↔ ∀ (x y z : Finset (Fin 3)), R.Holds x y → S.Holds y z → T.Holds x z

[Ica12]'s Definition 1.4 as a characterization: R.join S ≤ T exactly when chaining R's content with S's lands inside T's — soundness and tightness in one iff, the sup_le_iff idiom.

theorem NaturalLogic.Relation.exists_isLeast_holds {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (hx : x ≠ ⊥) (hx' : x ≠ ⊤) (hy : y ≠ ⊥) (hy' : y ≠ ⊤) : ∃ (R : Relation), IsLeast {S : Relation | S.Holds x y} R

[Ica12]'s Lemma 1.3: any two elements distinct from ⊥ and ⊤ stand in a strongest natural-logic relation — stated there for Boolean lattices, proved here for any bounded lattice. It fails at ⊥/⊤: x ⌣ ⊤ and x ⊑ ⊤ hold with no common strengthening.

Tightness of the projection tables

theorem NaturalLogic.Signature.isLeast_project (R : Relation) (σ : Signature) : IsLeast {T : Relation | ∀ (f : Finset (Fin 1) → Finset (Fin 1)), σ.HoldsFor f → ∀ (x y : Finset (Fin 1)), R.Holds x y → T.Holds (f x) (f y)} (project R σ)

Tightness of the projection tables ([Ica12] Definition 2.3; his Lemma 2.4 as an equality): project R σ is the least relation T such that every σ-function sends R-pairs to T-pairs, already over the two-element Boolean algebra.

theorem NaturalLogic.Signature.le_iff_holdsFor {σ τ : Signature} : σ ≤ τ ↔ ∀ (f : Finset (Fin 1) → Finset (Fin 1)), σ.HoldsFor f → τ.HoldsFor f

The refinement order on signatures is inclusion of function classes — [Ica12]'s semantic definition of ≼ (§2.2) recovered as a characterization of the property-set order, with countermodels on the two-element Boolean algebra.

Tightness of signature composition

theorem NaturalLogic.Signature.holdsFor_comp (ψ φ : Signature) (f g : Finset (Fin 1) → Finset (Fin 1)) : ψ.HoldsFor f → φ.HoldsFor g → (ψ * φ).HoldsFor (f ∘ g)

Function classes compose along Signature.compose: a ψ-function after a φ-function is a ψ * φ-function, on the two-element Boolean algebra.

theorem NaturalLogic.Signature.isLeast_compose (ψ φ : Signature) : IsLeast {χ : Signature | ∀ (f g : Finset (Fin 1) → Finset (Fin 1)), ψ.HoldsFor f → φ.HoldsFor g → χ.HoldsFor (f ∘ g)} (ψ * φ)

Tightness of signature composition ([Ica12] Definition 2.6): ψ * φ is the least signature whose class contains every composite of a ψ-function after a φ-function.