Documentation

Linglib.Logic.Natural.Soundness

Soundness of the projectivity calculus #

This file gives the seven relations their lattice content and proves the tables of Logic/Natural/Basic.lean sound for it over bounded lattices: chained relations compose as the join table says, and a signature's projection row holds of a function exactly when the function is monotone or antitone and carries disjoint and codisjoint pairs as the row says. The function classes of [Ica12] fall in their rows, their unit conditions being mathlib's pairing of meets with ⊥ and joins with ⊤, and so do bounded lattice homomorphisms and, into the order dual, complementation.

Main results #

Implementation notes #

References #

Lattice content of the relations #

source
def NaturalLogic.Relation.Holds {α : Type u_1} [Lattice α] [BoundedOrder α] :
Relation → α → α → 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 ≤ (MacCartney's exclusive reading takes it proper, which the projectivity tables do not need).

Equations
Instances For
    source
    def NaturalLogic.Relation.Atom.Holds {α : Type u_1} [Lattice α] [BoundedOrder α] :
    Atom → α → α → Prop

    The lattice content of an atomic constraint ([Ica12] Definition 1.2).

    Equations
    Instances For
      source
      theorem NaturalLogic.Relation.holds_iff {α : Type u_1} [Lattice α] [BoundedOrder α] {R : Relation} {x y : α} :
      R.Holds x y ↔ ∀ a ∈ R.constraints, a.Holds x y

      A relation's content is the conjunction of its constraint atoms: constraints is the single source of truth for Holds.

      source
      @[instance_reducible]
      instance NaturalLogic.Relation.Atom.decidableHolds {α : Type u_1} [Lattice α] [BoundedOrder α] [DecidableEq α] [DecidableLE α] (a : Atom) (x y : α) :
      Decidable (a.Holds x y)
      Equations
      source
      @[instance_reducible]
      instance NaturalLogic.Relation.decidableHolds {α : Type u_1} [Lattice α] [BoundedOrder α] [DecidableEq α] [DecidableLE α] (R : Relation) (x y : α) :
      Decidable (R.Holds x y)
      Equations

      Join soundness #

      source
      theorem NaturalLogic.Relation.Holds.join {β : Type u_1} [DistribLattice β] [BoundedOrder β] {R S : Relation} {x y z : β} (hR : R.Holds x y) (hS : S.Holds y z) :
      (R.join S).Holds x z

      Chained relations compose as the join table says. Distributivity is needed for the cells that reason through a complement (negation ⋈ negation = equiv is uniqueness of complements).

      Soundness of a signature for a function #

      source
      def NaturalLogic.Signature.SoundFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (σ : Signature) (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
      Instances For
        source
        theorem NaturalLogic.soundFor_mono_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
        Signature.mono.SoundFor f ↔ Monotone f

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

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

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

        source
        theorem NaturalLogic.Signature.SoundFor.monotone {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ : Signature} {f : α → β} (h : σ.SoundFor f) (hσ : σ.sign = 1) :
        Monotone f

        A signature of upward polarity is sound only for monotone functions.

        source
        theorem NaturalLogic.Signature.SoundFor.antitone {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ : Signature} {f : α → β} (h : σ.SoundFor f) (hσ : σ.sign = -1) :
        Antitone f

        A signature of downward polarity is sound only for antitone functions.

        source
        theorem NaturalLogic.soundFor_additive_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
        Signature.additive.SoundFor f ↔ Monotone f ∧ ∀ ⦃x y : α⦄, Codisjoint x y → Codisjoint (f x) (f y)

        The .additive row is sound exactly for the monotone functions sending codisjoint pairs to codisjoint pairs.

        source
        theorem NaturalLogic.soundFor_mult_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
        Signature.mult.SoundFor f ↔ Monotone f ∧ ∀ ⦃x y : α⦄, Disjoint x y → Disjoint (f x) (f y)

        The .mult row is sound exactly for the monotone functions sending disjoint pairs to disjoint pairs.

        source
        theorem NaturalLogic.soundFor_antiAdd_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
        Signature.antiAdd.SoundFor f ↔ Antitone f ∧ ∀ ⦃x y : α⦄, Codisjoint x y → Disjoint (f x) (f y)

        The .antiAdd row is sound exactly for the antitone functions sending codisjoint pairs to disjoint pairs.

        source
        theorem NaturalLogic.soundFor_antiMult_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
        Signature.antiMult.SoundFor f ↔ Antitone f ∧ ∀ ⦃x y : α⦄, Disjoint x y → Codisjoint (f x) (f y)

        The .antiMult row is sound exactly for the antitone functions sending disjoint pairs to codisjoint pairs.

        source
        theorem NaturalLogic.soundFor_addMult_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
        Signature.addMult.SoundFor f ↔ Monotone f ∧ (∀ ⦃x y : α⦄, Disjoint x y → Disjoint (f x) (f y)) ∧ ∀ ⦃x y : α⦄, Codisjoint x y → Codisjoint (f x) (f y)

        The .addMult row is sound exactly for the monotone functions preserving disjointness and codisjointness.

        source
        theorem NaturalLogic.soundFor_antiAddMult_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
        Signature.antiAddMult.SoundFor f ↔ Antitone f ∧ (∀ ⦃x y : α⦄, Disjoint x y → Codisjoint (f x) (f y)) ∧ ∀ ⦃x y : α⦄, Codisjoint x y → Disjoint (f x) (f y)

        The .antiAddMult row is sound exactly for the antitone functions exchanging disjointness and codisjointness.

        source
        theorem NaturalLogic.soundFor_additive {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : (∀ (p q : α), f (p ⊔ q) = f p ⊔ f q) ∧ f ⊤ = ⊤) :
        Signature.additive.SoundFor f
        source
        theorem NaturalLogic.soundFor_mult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : (∀ (p q : α), f (p ⊓ q) = f p ⊓ f q) ∧ f ⊥ = ⊥) :
        Signature.mult.SoundFor f
        source
        theorem NaturalLogic.soundFor_antiAdd {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : IsAntiAdditive f ∧ f ⊤ = ⊥) :
        Signature.antiAdd.SoundFor f
        source
        theorem NaturalLogic.soundFor_antiMult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : IsAntiMultiplicative f ∧ f ⊥ = ⊤) :
        Signature.antiMult.SoundFor f
        source
        theorem NaturalLogic.soundFor_addMult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (hadd : (∀ (p q : α), f (p ⊔ q) = f p ⊔ f q) ∧ f ⊤ = ⊤) (hmult : (∀ (p q : α), f (p ⊓ q) = f p ⊓ f q) ∧ f ⊥ = ⊥) :
        Signature.addMult.SoundFor f
        source
        theorem NaturalLogic.soundFor_antiAddMult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (haa : IsAntiAdditive f ∧ f ⊤ = ⊥) (ham : IsAntiMultiplicative f ∧ f ⊥ = ⊤) :
        Signature.antiAddMult.SoundFor f
        source
        theorem NaturalLogic.soundFor_addMult_of_boundedLatticeHomClass {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {F : Type u_4} [FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) :
        Signature.addMult.SoundFor ⇑f

        A bounded lattice homomorphism realizes the morphism row.

        source
        theorem NaturalLogic.soundFor_antiAddMult_of_boundedLatticeHomClass {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {F : Type u_4} [FunLike F α βᵒᵈ] [BoundedLatticeHomClass F α βᵒᵈ] (f : F) :
        Signature.antiAddMult.SoundFor (⇑OrderDual.ofDual ∘ ⇑f)

        A bounded lattice homomorphism into the order dual realizes the anti-morphism row.

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

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

        source
        theorem NaturalLogic.Relation.Holds.of_le {β : Type u_2} [Lattice β] [BoundedOrder β] {R R' : Relation} {u v : β} (h : R.Holds u v) (href : R ≤ R') :
        R'.Holds u v

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

        source
        theorem NaturalLogic.Relation.Holds.apply {β : Type u_2} [Lattice β] [BoundedOrder β] {ι : Type u_4} {R : Relation} {f g : ι → β} (h : R.Holds f g) (i : ι) :
        R.Holds (f i) (g i)

        A relation between functions holds pointwise.

        source
        theorem NaturalLogic.Signature.SoundFor.apply {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {ι : Type u_4} {σ : Signature} {f : α → ι → β} (h : σ.SoundFor f) (i : ι) :
        σ.SoundFor fun (x : α) => f x i

        A signature sound for a two-place function is sound for it at any fixed second argument, the lattice operations on functions being pointwise.

        source
        theorem NaturalLogic.Signature.project_mono (R : Relation) :
        Monotone (project R)

        A more specific signature projects every relation at least as informatively.

        source
        theorem NaturalLogic.Signature.SoundFor.of_le {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ τ : Signature} {f : α → β} (h : σ.SoundFor f) (hστ : σ ≤ τ) :
        τ.SoundFor f

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

        Composition and paths #

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

        Soundness composes along Signature.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.

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

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

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

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

        Worked instance: double negation is a morphism, semantically #

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

        source
        theorem NaturalLogic.compl_soundFor_antiAddMult {α : Type u_1} [BooleanAlgebra α] :
        Signature.antiAddMult.SoundFor compl

        Complementation realizes the anti-morphism row.

        source
        theorem NaturalLogic.not_soundFor_antiAddMult :
        Signature.antiAddMult.SoundFor Not

        Propositional negation realizes the anti-morphism row at the Prop instance.

        Per-position profiles #

        Two-place operators carry one signature per argument position — a determiner is one signature in its restrictor and another in its scope. Signature₂ records the pair, Signature₂.SoundFor says each component is sound for the corresponding section (the other argument held constant), and Signature.SoundFor.comp₂ composes an outer context into both positions at once. Certified instances for generalized quantifiers live in Semantics/Quantification/Signatures.lean.

        source
        structure NaturalLogic.Signature₂ :
        Type

        A per-position signature profile for a two-place operator. For determiners the positions are restrictor and scope; under the restrictor analysis of conditionals, antecedent and consequent.

        Instances For
          source
          def NaturalLogic.instDecidableEqSignature₂.decEq (x✝ x✝¹ : Signature₂) :
          Decidable (x✝ = x✝¹)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance NaturalLogic.instDecidableEqSignature₂ :
            DecidableEq Signature₂
            Equations
            source
            def NaturalLogic.instReprSignature₂.repr :
            Signature₂ → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance NaturalLogic.instReprSignature₂ :
              Repr Signature₂
              Equations
              source
              def NaturalLogic.Signature₂.SoundFor {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] (σ : Signature₂) (f : α → β → γ) :
              Prop

              A profile is sound for a two-place operator when each component signature is sound for the corresponding section (the other argument held constant).

              Equations
              Instances For
                source
                theorem NaturalLogic.Signature.SoundFor.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Lattice γ] [BoundedOrder γ] [Lattice δ] [BoundedOrder δ] {ψ : Signature} {g : γ → δ} {σ : Signature₂} {f : α → β → γ} (hg : ψ.SoundFor g) (hf : σ.SoundFor f) :
                { restrictor := ψ * σ.restrictor, scope := ψ * σ.scope }.SoundFor fun (x : α) (y : β) => g (f x y)

                Composing a sound outer context into a sound two-place operator composes the profile componentwise — the two-place form of Signature.SoundFor.comp.

                The function class of a signature #

                source
                def NaturalLogic.Signature.Property.HoldsFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] :
                Property → (α → β) → Prop

                The function class a property asserts.

                Equations
                Instances For
                  source
                  def NaturalLogic.Signature.HoldsFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] (σ : Signature) (f : α → β) :
                  Prop

                  A function has signature σ — is a "σ-function" — when it has every property σ asserts.

                  Equations
                  Instances For
                    source
                    theorem NaturalLogic.Signature.soundFor_of_holdsFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ : Signature} {f : α → β} (h : σ.HoldsFor f) :
                    σ.SoundFor f

                    σ's projection row is sound for every σ-function ([Ica12] Lemma 2.5), aggregating the per-row theorems.

                    source
                    theorem NaturalLogic.Signature.HoldsFor.of_le {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {σ τ : Signature} {f : α → β} (h : σ.HoldsFor f) (hστ : σ ≤ τ) :
                    τ.HoldsFor f

                    The class of a more specific signature is included in the class of a less specific one — the sound direction of the refinement order, with the converse in Logic/Natural/Completeness.lean (le_iff_holdsFor).

                    source
                    theorem NaturalLogic.Signature.holdsFor_anti_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
                    anti.HoldsFor f ↔ Antitone f
                    source
                    theorem NaturalLogic.Signature.holdsFor_antiAdd_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
                    antiAdd.HoldsFor f ↔ IsAntiAdditive f ∧ f ⊤ = ⊥
                    source
                    theorem NaturalLogic.Signature.holdsFor_antiAddMult_iff {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} :
                    antiAddMult.HoldsFor f ↔ (IsAntiAdditive f ∧ f ⊤ = ⊥) ∧ IsAntiMultiplicative f ∧ f ⊥ = ⊤
                    source
                    theorem NaturalLogic.Signature.holdsFor_addMult_of_galoisConnection {α : Type u_1} [Lattice α] [BoundedOrder α] {f u l : α → α} (gc₁ : GaloisConnection f u) (gc₂ : GaloisConnection l f) :
                    addMult.HoldsFor f

                    A map with adjoints on both sides is in the morphism class ⊕⊞ — the Lawvere reading of the signature: bi-adjoints preserve everything.

                    source
                    theorem NaturalLogic.Signature.holdsFor_antiAddMult_compl {γ : Type u_3} [BooleanAlgebra γ] :
                    antiAddMult.HoldsFor compl

                    Complementation, the self-dual adjoint pair, is in the anti-morphism class ◇⊟.

                    source
                    @[instance_reducible]
                    instance NaturalLogic.Signature.Property.decidableHoldsFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Fintype α] [DecidableLE α] [DecidableEq β] [DecidableLE β] (p : Property) (f : α → β) :
                    Decidable (p.HoldsFor f)
                    Equations
                    source
                    @[instance_reducible]
                    instance NaturalLogic.Signature.decidableHoldsFor {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] [Fintype α] [DecidableLE α] [DecidableEq β] [DecidableLE β] (σ : Signature) (f : α → β) :
                    Decidable (σ.HoldsFor f)
                    Equations