Icard (2012): Inclusion and Exclusion in Natural Language

This file formalizes Icard's projectivity calculus, which extends the Monotonicity Calculus from inclusion to the exclusion relations of MacCartney and Manning. The relations, their join and projection tables and the composition of signatures are the library's NaturalLogic substrate, whose implementations this file checks against the printed cells; on top of them it builds the typed language of Section 2, with the projectivity markings of a lexicon's constants, the projectivity of a context (Definition 2.9, Ctx.pro), and the soundness of projectivity marking (Proposition 2.10, Model.soundFor_ctxFun). The calculus 𝒞 of Section 3 is Derives, with the Substitution rule over contexts, and Theorem 3.1 is Derives.sound. The worked example of Section 3.2, that Every job that involves a giant squid is dangerous entails Not every job that involves a cephalopod is safe, is derived from the paper's assumption set by three substitutions and two compositions (derives_squid), and Section 4's correspondence between the signatures and Zwarts's three classes of negative polarity items is Licenses, read off the substrate's strength map Signature.toDEStrength.

Implementation notes

• Types are unmarked and the markings live on the lexicon's constants, one signature per arrow, outermost first; the topmost projectivity of a term is its first remaining marking, • when none is left. A model's constants are functions of their signatures over the whole unmarked domains, Boolean algebras, which is stronger than the paper's marked domains and leaves Definition 2.8's subtyping of marked types aside.
• The paper's remark that terms of additive and anti-additive types always alternate, the witness of incompleteness, is not formalized: in the unmarked function lattice the constant ⊤ function and complementation are additive and anti-additive without being disjoint.
• One cell of the printed projection table deviates from Definition 2.3 (project_equiv).

References

• [Ica12]
• [MCM09]
• [Zwa98]

The printed tables

The join table (Lemma 1.5), the projection table (Lemma 2.4) and the composition table (Lemma 2.7) are the substrate's join, project and compose; the cells are certified sound and least in Logic/Natural/Soundness.lean and Logic/Natural/Completeness.lean.

The typed language (Sections 2.1 and 2.3)

inductive Icard2012.Base : Type

The basic types: predicates, intransitive verbs and truth values.

• p : Base
• v : Base
• t : Base

@[instance_reducible]

instance Icard2012.instDecidableEqBase : DecidableEq Base

Equations

• Icard2012.instDecidableEqBase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Icard2012.Ty : Type

Unmarked types.

• base : Base → Ty
• arrow : Ty → Ty → Ty

def Icard2012.instDecidableEqTy.decEq (x✝ x✝¹ : Ty) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Icard2012.instDecidableEqTy.decEq (Icard2012.Ty.base a) (Icard2012.Ty.base b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Icard2012.instDecidableEqTy.decEq (Icard2012.Ty.base a) (a_1.arrow a_2) = isFalse ⋯
• Icard2012.instDecidableEqTy.decEq (a.arrow a_1) (Icard2012.Ty.base a_2) = isFalse ⋯

@[instance_reducible]

instance Icard2012.instDecidableEqTy : DecidableEq Ty

Equations

• Icard2012.instDecidableEqTy = Icard2012.instDecidableEqTy.decEq

structure Icard2012.Lexicon (κ : Type u_1) : Type u_1

A lexicon: the constants' types and the projectivity markings of their arrows, outermost first (Definition 2.1).

• ty : κ → Ty
• marks : κ → List NaturalLogic.Signature

inductive Icard2012.Term {κ : Type u_1} (L : Lexicon κ) : Ty → Type u_1

Terms of the language (Definition 2.8): constants and applications.

• const {κ : Type u_1} {L : Lexicon κ} (c : κ) : Term L (L.ty c)
• app {κ : Type u_1} {L : Lexicon κ} {σ τ : Ty} : Term L (σ.arrow τ) → Term L σ → Term L τ

def Icard2012.Term.marks {κ : Type u_1} {L : Lexicon κ} {τ : Ty} : Term L τ → List NaturalLogic.Signature

The markings a term still carries: applying a term consumes its outermost marking.

Equations

• (Icard2012.Term.const c).marks = L.marks c
• (s.app a).marks = s.marks.tail

def Icard2012.Term.top {κ : Type u_1} {L : Lexicon κ} {τ : Ty} (t : Term L τ) : NaturalLogic.Signature

The topmost projectivity of a term (Section 2.4): its outermost marking, • when it has none.

Equations

• t.top = t.marks.headD NaturalLogic.Signature.all

inductive Icard2012.Ctx {κ : Type u_1} (L : Lexicon κ) (σ : Ty) : Ty → Type u_1

A context (Section 2.4): a term with one hole of type σ, in function or argument position.

• hole {κ : Type u_1} {L : Lexicon κ} {σ : Ty} : Ctx L σ σ
• appL {κ : Type u_1} {L : Lexicon κ} {σ ρ τ : Ty} : Ctx L σ (ρ.arrow τ) → Term L ρ → Ctx L σ τ
• appR {κ : Type u_1} {L : Lexicon κ} {σ ρ τ : Ty} : Term L (ρ.arrow τ) → Ctx L σ ρ → Ctx L σ τ

def Icard2012.Ctx.fill {κ : Type u_1} {L : Lexicon κ} {σ τ : Ty} : Ctx L σ τ → Term L σ → Term L τ

Filling the hole of a context.

Equations

• Icard2012.Ctx.hole.fill x✝ = x✝
• (c.appL u).fill x✝ = (c.fill x✝).app u
• (Icard2012.Ctx.appR f c).fill x✝ = f.app (c.fill x✝)

def Icard2012.Ctx.pro {κ : Type u_1} {L : Lexicon κ} {σ τ : Ty} : Ctx L σ τ → NaturalLogic.Signature

The projectivity of a context (Definition 2.9): the identity marking at the hole, the context's own projectivity into the function position, and the function's topmost projectivity composed with the argument's into the argument position.

Equations

• Icard2012.Ctx.hole.pro = NaturalLogic.Signature.addMult
• (c.appL a).pro = c.pro
• (Icard2012.Ctx.appR f c).pro = f.top * c.pro

Models (Definition 2.8)

The domain of a basic type is a Boolean algebra and that of an arrow all functions, the Boolean lattice of Proposition 1.1; a constant denotes a function of its signature whose values again are (Definition 2.2).

def Icard2012.Dom (B : Base → Type u) : Ty → Type u

The domains of the unmarked types.

Equations

• Icard2012.Dom B (Icard2012.Ty.base b) = B b
• Icard2012.Dom B (σ.arrow τ) = (Icard2012.Dom B σ → Icard2012.Dom B τ)

@[reducible]

def Icard2012.Dom.booleanAlgebra {B : Base → Type u} [(b : Base) → BooleanAlgebra (B b)] (τ : Ty) : BooleanAlgebra (Dom B τ)

The Boolean algebra of a domain: that of the basic type, or the pointwise one on functions.

Equations

• One or more equations did not get rendered due to their size.
• Icard2012.Dom.booleanAlgebra (σ.arrow τ) = Pi.instBooleanAlgebra

@[reducible]

instance Icard2012.Dom.instBooleanAlgebra {B : Base → Type u} [(b : Base) → BooleanAlgebra (B b)] (τ : Ty) : BooleanAlgebra (Dom B τ)

Equations

• Icard2012.Dom.instBooleanAlgebra τ = Icard2012.Dom.booleanAlgebra τ

def Icard2012.Mem {B : Base → Type u} [(b : Base) → BooleanAlgebra (B b)] : List NaturalLogic.Signature → (τ : Ty) → Dom B τ → Prop

A value of a type is of the given markings when it is a function of the first marking whose values are of the remaining ones (Definition 2.2).

Equations

• Icard2012.Mem (φ :: ms) (σ.arrow τ) f = (φ.SoundFor f ∧ ∀ (x : Icard2012.Dom B σ), Icard2012.Mem ms τ (f x))
• Icard2012.Mem x✝² x✝¹ x✝ = True

structure Icard2012.Model {κ : Type u_1} (L : Lexicon κ) : Type (max (u + 1) u_1)

A model of the language: domains for the basic types and a denotation for each constant of its markings.

• B : Base → Type u
• ba (b : Base) : BooleanAlgebra (self.B b)
• val (c : κ) : Dom self.B (L.ty c)
• mem (c : κ) : Mem (L.marks c) (L.ty c) (self.val c)

def Icard2012.Model.eval {κ : Type u_1} {L : Lexicon κ} (M : Model L) {τ : Ty} : Term L τ → Dom M.B τ

The denotation of a term.

Equations

• M.eval (Icard2012.Term.const c) = M.val c
• M.eval (s.app a) = M.eval s (M.eval a)

def Icard2012.Model.ctxFun {κ : Type u_1} {L : Lexicon κ} {σ : Ty} (M : Model L) {τ : Ty} : Ctx L σ τ → Dom M.B σ → Dom M.B τ

The function a context denotes (Section 2.4).

Equations

• M.ctxFun Icard2012.Ctx.hole = id
• M.ctxFun (c.appL a) = fun (a_1 : Icard2012.Dom M.B σ) => M.ctxFun c a_1 (M.eval a)
• M.ctxFun (Icard2012.Ctx.appR f c) = M.eval f ∘ M.ctxFun c

theorem Icard2012.Model.eval_fill {κ : Type u_1} {L : Lexicon κ} {σ : Ty} (M : Model L) {τ : Ty} (c : Ctx L σ τ) (s : Term L σ) : M.eval (c.fill s) = M.ctxFun c (M.eval s)

theorem Icard2012.Model.mem_eval {κ : Type u_1} {L : Lexicon κ} (M : Model L) {τ : Ty} (t : Term L τ) : Mem t.marks τ (M.eval t)

Every term denotes a value of its markings.

theorem Icard2012.Model.soundFor_ctxFun {κ : Type u_1} {L : Lexicon κ} {σ : Ty} (M : Model L) {τ : Ty} (c : Ctx L σ τ) : c.pro.SoundFor (M.ctxFun c)

Soundness of projectivity marking (Proposition 2.10): a context denotes a function of its projectivity.

The calculus 𝒞 (Section 3.1)

inductive Icard2012.Derives {κ : Type u_1} {L : Lexicon κ} (Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop) {τ : Ty} : Term L τ → NaturalLogic.Relation → Term L τ → Prop

The projectivity calculus 𝒞: Reflexivity, the four Symmetry rules, Absurdity, Composition along the join, and Substitution through a context with the projection of the relation, deriving relational statements between terms of a type from an assumption set.

• ax {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {τ : Ty} {t t' : Term L τ} {R : NaturalLogic.Relation} : Γ t R t' → Derives Γ t R t'
• refl {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {τ : Ty} (t : Term L τ) : Derives Γ t NaturalLogic.Relation.forward t
• symm_forward {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {τ : Ty} {t t' : Term L τ} : Derives Γ t NaturalLogic.Relation.forward t' → Derives Γ t' NaturalLogic.Relation.reverse t
• symm_reverse {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {τ : Ty} {t t' : Term L τ} : Derives Γ t NaturalLogic.Relation.reverse t' → Derives Γ t' NaturalLogic.Relation.forward t
• symm_alternation {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {τ : Ty} {t t' : Term L τ} : Derives Γ t NaturalLogic.Relation.alternation t' → Derives Γ t' NaturalLogic.Relation.alternation t
• symm_cover {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {τ : Ty} {t t' : Term L τ} : Derives Γ t NaturalLogic.Relation.cover t' → Derives Γ t' NaturalLogic.Relation.cover t
• absurd {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {τ ρ : Ty} {t : Term L τ} {s s' : Term L ρ} (R : NaturalLogic.Relation) : Derives Γ t NaturalLogic.Relation.alternation t → Derives Γ s R s'
• comp {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {τ : Ty} {t u v : Term L τ} {R S : NaturalLogic.Relation} : Derives Γ t R u → Derives Γ u S v → Derives Γ t (R * S) v
• subst {κ : Type u_1} {L : Lexicon κ} {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} {σ τ : Ty} {s s' : Term L σ} {R : NaturalLogic.Relation} (c : Ctx L σ τ) : Derives Γ s R s' → Derives Γ (c.fill s) (NaturalLogic.Signature.project R c.pro) (c.fill s')

theorem Icard2012.Derives.sound {κ : Type u_1} {L : Lexicon κ} (M : Model L) {Γ : {τ : Ty} → Term L τ → NaturalLogic.Relation → Term L τ → Prop} (hΓ : ∀ {τ : Ty} {t t' : Term L τ} {R : NaturalLogic.Relation}, Γ t R t' → R.Holds (M.eval t) (M.eval t')) (hv : ∀ {τ : Ty} (t : Term L τ), M.eval t ≠ ⊥) {τ : Ty} {t t' : Term L τ} {R : NaturalLogic.Relation} (h : Derives (fun {τ : Ty} => Γ) t R t') : R.Holds (M.eval t) (M.eval t')

Soundness of 𝒞 (Theorem 3.1): a derivable statement holds in every model of the assumptions in which no term denotes ⊥; Composition is Lemma 1.6, Substitution Corollary 2.12, and Absurdity needs the nonvacuity.

The worked example (Section 3.2)

inductive Icard2012.Const : Type

The constants of the fragment.

• every : Const
• some : Const
• no : Const
• notEvery : Const
• job : Const
• giantSquid : Const
• cephalopod : Const
• safe : Const
• dangerous : Const
• is : Const
• involves : Const
• that : Const

@[instance_reducible]

instance Icard2012.instDecidableEqConst : DecidableEq Const

Equations

• Icard2012.instDecidableEqConst x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Icard2012.lexicon : Lexicon Const

The fragment's lexicon: every is anti-additive then multiplicative, some additive twice, no anti-additive twice, not every additive then anti-multiplicative, and the adjectives, copula, verb and relativizer morphisms.

Equations

• One or more equations did not get rendered due to their size.

def Icard2012.k (c : Const) : Term lexicon (lexicon.ty c)

A constant as a term.

Equations

• Icard2012.k c = Icard2012.Term.const c

inductive Icard2012.Assumption {τ : Ty} : Term lexicon τ → NaturalLogic.Relation → Term lexicon τ → Prop

The assumption set Γ of Section 3.2.

• everyNegNotEvery : Assumption (k Const.every) NaturalLogic.Relation.negation (k Const.notEvery)
• someNegNo : Assumption (k Const.some) NaturalLogic.Relation.negation (k Const.no)
• noAltEvery : Assumption (k Const.no) NaturalLogic.Relation.alternation (k Const.every)
• safeAltDangerous : Assumption (k Const.safe) NaturalLogic.Relation.alternation (k Const.dangerous)
• squidLeCephalopod : Assumption (k Const.giantSquid) NaturalLogic.Relation.forward (k Const.cephalopod)

theorem Icard2012.derives_no_forward_notEvery : Derives (fun {τ : Ty} => Assumption) (k Const.no) NaturalLogic.Relation.forward (k Const.notEvery)

no ⊑ not every needs no extra postulate: Composition on no | every and every ^ not every, with | ⋈ ^ = ⊑.

def Icard2012.sentence (q : Term lexicon (lexicon.ty Const.every)) (n : Term lexicon (Ty.base Base.p)) (a : Term lexicon (lexicon.ty Const.safe)) : Term lexicon (Ty.base Base.t)

Q job that involves a N is A, for a determiner q, a noun n and an adjective a.

Equations

• One or more equations did not get rendered due to their size.

def Icard2012.t₀ : Term lexicon (Ty.base Base.t)

Every job that involves a giant squid is dangerous.

Equations

• Icard2012.t₀ = Icard2012.sentence (Icard2012.k Icard2012.Const.every) (Icard2012.k Icard2012.Const.giantSquid) (Icard2012.k Icard2012.Const.dangerous)

def Icard2012.u₀ : Term lexicon (Ty.base Base.t)

Every job that involves a giant squid is safe.

Equations

• Icard2012.u₀ = Icard2012.sentence (Icard2012.k Icard2012.Const.every) (Icard2012.k Icard2012.Const.giantSquid) (Icard2012.k Icard2012.Const.safe)

def Icard2012.v₀ : Term lexicon (Ty.base Base.t)

Every job that involves a cephalopod is safe.

Equations

• Icard2012.v₀ = Icard2012.sentence (Icard2012.k Icard2012.Const.every) (Icard2012.k Icard2012.Const.cephalopod) (Icard2012.k Icard2012.Const.safe)

def Icard2012.t₀' : Term lexicon (Ty.base Base.t)

Not every job that involves a cephalopod is safe.

Equations

• Icard2012.t₀' = Icard2012.sentence (Icard2012.k Icard2012.Const.notEvery) (Icard2012.k Icard2012.Const.cephalopod) (Icard2012.k Icard2012.Const.safe)

def Icard2012.adjectiveCtx : Ctx lexicon ((Ty.base Base.p).arrow (Ty.base Base.p)) (Ty.base Base.t)

The context of the adjective: its projectivity is top(every(job…)) ∘ top(is) = ⊞.

Equations

• One or more equations did not get rendered due to their size.

def Icard2012.nounCtx : Ctx lexicon (Ty.base Base.p) (Ty.base Base.t)

The context of the noun under a, with the adjective already safe: its projectivity is top(every) ∘ top(that) ∘ top(involves) ∘ top(a) = ◇.

Equations

• One or more equations did not get rendered due to their size.

def Icard2012.determinerCtx : Ctx lexicon (lexicon.ty Const.every) (Ty.base Base.t)

The context of the determiner, under no function: projectivity ⊕⊞.

Equations

• One or more equations did not get rendered due to their size.

theorem Icard2012.derives_squid : Derives (fun {τ : Ty} => Assumption) t₀ NaturalLogic.Relation.forward t₀'

The main example: Every job that involves a giant squid is dangerous ⊑ Not every job that involves a cephalopod is safe (the paper misprints giant squid in the conclusion). Substituting safe for dangerous under ⊞ keeps |, cephalopod for giant squid under ◇ turns ⊑ into ⊒, and not every for every under ⊕⊞ keeps ^; Composition then gives | ⋈ ⊒ = | and | ⋈ ^ = ⊑.

Negative polarity items (Section 4)

The three classes of [Zwa98] are the signatures' downward half: weak items need an antitone context, strong ones an anti-additive context and superstrong ones an anti-morphic one.

def Icard2012.Licenses (level : PolarityItem.DEStrength) (σ : NaturalLogic.Signature) : Prop

A signature licenses an item of a Zwarts class when the strength of negation it realizes, Signature.toDEStrength, is at least as strong.

Equations

• Icard2012.Licenses level σ = (↑level ≤ σ.toDEStrength)

@[instance_reducible]

instance Icard2012.instDecidableLicenses (level : PolarityItem.DEStrength) (σ : NaturalLogic.Signature) : Decidable (Licenses level σ)

Equations

• Icard2012.instDecidableLicenses level σ = Icard2012.instDecidableLicenses._aux_1 level σ

theorem Icard2012.licenses_weak {σ : NaturalLogic.Signature} (h : σ.sign = -1) : Licenses PolarityItem.DEStrength.weak σ

A downward signature licenses the weak items.