Documentation

Linglib.Studies.Icard2012

[Ica12]: Inclusion and Exclusion in Natural Language #

Table verifications for [Ica12]'s relation algebra against the substrate implementations in Logic/Natural/Basic.lean: the join table (Lemma 1.5, p. 710 — the printed cells, independently certified against the non-strict Holds reading by Relation.Holds.join and tight by Relation.isLeast_join), the projectivity tables (Lemma 2.4, p. 715), the composition table (Lemma 2.7, p. 716) with its signature order (§2.2), the polarity coarsening, the classification of not as the anti-morphism (p. 713), and path computations illustrating the §2.4 context-projectivity mechanism. The tables' semantic soundness is certified once and for all in Logic/Natural/Soundness.lean; this file checks the implementations cell-by-cell against the paper's printed entries.

The final sections formalize the ground fragment of the paper's projectivity calculus 𝒞 (§3.1) with its soundness theorem (Theorem 3.1), and the §3.2 worked fragment: the assumption set Γ, the derivation that no ⊑ not every is not an extra postulate, and a concrete model witnessing Γ's satisfiability.

The join table (Lemma 1.5, p. 710) #

The refinement order (§2.2) #

The projectivity tables (Lemma 2.4, p. 715) #

Forward entailment (dog ⊑ animal), negation, alternation (cat | dog), and cover (animal ⌣ nondog) pushed through each signature class.

The composition table (Lemma 2.7, p. 716) #

The polarity coarsening #

Path computations (§2.4) #

A position's signature is the monoid product along the path from root to target (his pro(s(u)) = top(s) ∘ pro(u)); the sentences are illustrations of the mechanism, not the paper's own examples.

The negation signature #

Not is anti-additive and anti-multiplicative (p. 713); ⊖ is its own inverse — the only non-identity signature with one (p. 716).

The calculus 𝒞 of relations (§3.1) #

The ground fragment of the projectivity calculus: Reflexivity, the four Symmetry rules, Absurdity, and Composition, over an assumption set of relational statements. The Substitution rule needs the signature-typed term language and is not yet formalized; neither is the paper's closing observation that 𝒞 is incomplete (terms of additive and anti-additive type always alternate, underivably from ∅) — completeness is left open there.

source
inductive Icard2012.Derives {ι : Type u_1} (Γ : ι → NaturalLogic.Relation → ι → Prop) :
ι → NaturalLogic.Relation → ι → Prop

The ground fragment of the projectivity calculus 𝒞 ([Ica12] §3.1, p. 719), deriving relational statements between terms ι from an assumption set Γ.

Instances For
    source
    theorem Icard2012.Derives.sound {ι : Type u_1} {β : Type u_2} [DistribLattice β] [BoundedOrder β] {Γ : ι → NaturalLogic.Relation → ι → Prop} {v : ι → β} (hΓ : ∀ {t : ι} {R : NaturalLogic.Relation} {t' : ι}, Γ t R t' → R.Holds (v t) (v t')) (hv : ∀ (i : ι), v i ≠ ⊥) {t : ι} {R : NaturalLogic.Relation} {t' : ι} (h : Derives Γ t R t') :
    R.Holds (v t) (v t')

    [Ica12]'s Theorem 3.1 for the ground fragment: a derivable statement holds in every ⊥-free model of the assumptions. Composition is sound by Relation.Holds.join; Absurdity is the one rule needing nonvacuity, since t | t forces ⟦t⟧ = ⊥.

    The worked fragment (§3.2) #

    The paper's mini-lexicon and its assumption set Γ; the derivation that no ⊑ not every needs no extra postulate; and a concrete model over the three-atom Boolean algebra witnessing that Γ is satisfiable.

    source
    inductive Icard2012.Item :
    Type

    The constants of the §3.2 fragment that Γ relates.

    Instances For
      source
      @[instance_reducible]
      instance Icard2012.instDecidableEqItem :
      DecidableEq Item
      Equations
      source
      @[instance_reducible]
      instance Icard2012.instFintypeItem :
      Fintype Item
      Equations
      source
      def Icard2012.instReprItem.repr :
      Item → ℕ → Std.Format
      Equations
      Instances For
        source
        @[instance_reducible]
        instance Icard2012.instReprItem :
        Repr Item
        Equations
        source
        inductive Icard2012.Assumption :
        Item → NaturalLogic.Relation → Item → Prop

        The §3.2 assumption set Γ: every ^ not every, some ^ no, no | every, safe | dangerous, giant squid ⊑ cephalopod.

        Instances For
          source
          theorem Icard2012.derives_no_forward_notEvery :
          Derives Assumption Item.no NaturalLogic.Relation.forward Item.notEvery

          §3.2: no ⊑ not every is derivable, not postulated — Composition on no | every and every ^ not every, with | ⋈ ^ = ⊑.

          source
          def Icard2012.squidModel :
          Item → Finset (Fin 3)

          A model of the §3.2 assumptions over the three-atom Boolean algebra.

          Equations
          Instances For
            source
            theorem Icard2012.squidModel_models {t : Item} {R : NaturalLogic.Relation} {t' : Item} (h : Assumption t R t') :
            R.Holds (squidModel t) (squidModel t')
            source
            theorem Icard2012.squidModel_ne_bot (i : Item) :
            squidModel i ≠ ⊥