Implication signatures

A complement-taking operator such as manage, force or refuse implies something about its complement in a positive context, in a negative context, or in both. Nairn, Condoravdi and Karttunen classify these operators by their implication signature, the polarity of the complement each context implies, if any: manage is +/−, since managed to leave implies left and didn't manage to leave implies didn't leave; force is +/◦, refuse −/◦, hesitate ◦/+, and a propositional attitude such as want is ◦/◦. MacCartney and Manning count nine signatures, covering the two-way and one-way implicatives, the factives and the attitudes.

Each slot of a signature is a flat value, ◦ being ⊥, so signatures are ordered by how much they imply: force's +/◦ lies below manage's +/−, and the attitudes' ◦/◦ is ⊥.

Main definitions

• NaturalLogic.ImplicationSignature: the complement's implied polarity in a positive and in a negative context
• NaturalLogic.ImplicationSignature.implied: the polarity implied in a context of a given polarity

References

• [NCK06]
• [MCM09]

structure NaturalLogic.ImplicationSignature : Type

The implication signature of a complement-taking operator gives the polarity of the complement it implies in a positive context and in a negative context, ⊥ where it implies nothing.

• positive : Flat Polarity

  The complement's implied polarity in a positive context.

• negative : Flat Polarity

  The complement's implied polarity in a negative context.

theorem NaturalLogic.ImplicationSignature.ext {x y : ImplicationSignature} (positive : x.positive = y.positive) (negative : x.negative = y.negative) : x = y

theorem NaturalLogic.ImplicationSignature.ext_iff {x y : ImplicationSignature} : x = y ↔ x.positive = y.positive ∧ x.negative = y.negative

@[instance_reducible]

instance NaturalLogic.instDecidableEqImplicationSignature : DecidableEq ImplicationSignature

Equations

• NaturalLogic.instDecidableEqImplicationSignature = NaturalLogic.instDecidableEqImplicationSignature.decEq

def NaturalLogic.instDecidableEqImplicationSignature.decEq (x✝ x✝¹ : ImplicationSignature) : Decidable (x✝ = x✝¹)

Equations

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

def NaturalLogic.instReprImplicationSignature.repr : ImplicationSignature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance NaturalLogic.instReprImplicationSignature : Repr ImplicationSignature

Equations

• NaturalLogic.instReprImplicationSignature = { reprPrec := NaturalLogic.instReprImplicationSignature.repr }

def NaturalLogic.ImplicationSignature.implied (s : ImplicationSignature) : Polarity → Flat Polarity

The polarity of the complement implied in a context of polarity m.

Equations

• s.implied Polarity.positive = s.positive
• s.implied Polarity.negative = s.negative

@[simp]

theorem NaturalLogic.ImplicationSignature.implied_positive (s : ImplicationSignature) : s.implied Polarity.positive = s.positive

@[simp]

theorem NaturalLogic.ImplicationSignature.implied_negative (s : ImplicationSignature) : s.implied Polarity.negative = s.negative

theorem NaturalLogic.ImplicationSignature.implied_injective : Function.Injective implied

@[instance_reducible]

instance NaturalLogic.ImplicationSignature.instPartialOrder : PartialOrder ImplicationSignature

One signature is below another when every context implies less under it.

Equations

• NaturalLogic.ImplicationSignature.instPartialOrder = PartialOrder.lift NaturalLogic.ImplicationSignature.implied NaturalLogic.ImplicationSignature.implied_injective

theorem NaturalLogic.ImplicationSignature.le_iff {s t : ImplicationSignature} : s ≤ t ↔ s.positive ≤ t.positive ∧ s.negative ≤ t.negative

@[instance_reducible]

instance NaturalLogic.ImplicationSignature.instOrderBot : OrderBot ImplicationSignature

The signature ◦/◦ implies nothing in either context.

Equations

• NaturalLogic.ImplicationSignature.instOrderBot = { bot := { positive := ⊥, negative := ⊥ }, bot_le := NaturalLogic.ImplicationSignature.instOrderBot._proof_1 }

@[simp]

theorem NaturalLogic.ImplicationSignature.bot_positive : ⊥.positive = ⊥

@[simp]

theorem NaturalLogic.ImplicationSignature.bot_negative : ⊥.negative = ⊥