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 each signature's projection row holds of every function in the signature's class.

Main declarations #

Implementation notes #

The algebraic rows hold in the sound direction only — projection rows are class-maximal, not function-characterizing; tightness is proved in Logic/Natural/Completeness.lean for the join table. The additive-family rows need the IsCompletely* unit conditions, exactly as [Ica12]'s tables assume, and the proofs go through over bounded lattices rather than his Boolean lattices. soundFor_all holds unconditionally: every function realizes the no-property row.

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

      The join table is sound: chained relations compose as join 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.soundFor_additive {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (h : IsCompletelyAdditive f) :
        Signature.additive.SoundFor f

        The .additive row is sound for completely additive functions.

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

        The .mult row is sound for completely multiplicative functions.

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

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

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

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

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

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

        source
        theorem NaturalLogic.soundFor_antiAddMult {α : Type u_1} {β : Type u_2} [Lattice α] [BoundedOrder α] [Lattice β] [BoundedOrder β] {f : α → β} (haa : IsCompletelyAntiAdditive f) (ham : IsCompletelyAntiMultiplicative f) :
        Signature.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".

        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: .all is 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.Signature.project_mono (R : Relation) :
        Monotone (project R)

        Projection is monotone in the signature order: 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))

        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 #

        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_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