The Zwarts hierarchy of negative strength

The strengths of negation a context can carry, ordered as the chain weak < antiAdditive < antiMorphic ([Zwa98]; [vdW97]'s minimal, regular and classical negation): a context is weakly negative when it is downward entailing, anti-additive when it also turns disjunctions into conjunctions, and anti-morphic when it also turns conjunctions into disjunctions, as clausal negation does. Each strength is the function class of a natural-logic signature (DEStrength.toSignature), so its semantic content is Signature.HoldsFor, with the unit conditions that keep a constant map from holding every strength, and a signature realizes a strength through its projection behavior (Signature.toDEStrength).

Main declarations

• PolarityItem.DEStrength: the three strengths, a linear order.
• PolarityItem.DEStrength.toSignature: the signature whose function class a strength is.
• NaturalLogic.Signature.toDEStrength: the strength a signature realizes, ⊥ for a signature that is not downward entailing.
• NaturalLogic.Signature.toDEStrength_ne_bot_iff: a signature realizes a strength exactly when it is downward entailing.

References

• [Zwa98]
• [vdW97]
• [Ica12]
• [Lad79]

The hierarchy

inductive PolarityItem.DEStrength : Type

The three strengths of negation ([Zwa98]): weak is plain downward entailment, antiAdditive adds the ∨→∧ distributivity of nobody, and antiMorphic the ∧→∨ distributivity of clausal negation.

• weak : DEStrength
• antiAdditive : DEStrength
• antiMorphic : DEStrength

@[instance_reducible]

instance PolarityItem.instDecidableEqDEStrength : DecidableEq DEStrength

Equations

• PolarityItem.instDecidableEqDEStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def PolarityItem.instReprDEStrength.repr : DEStrength → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PolarityItem.instReprDEStrength : Repr DEStrength

Equations

• PolarityItem.instReprDEStrength = { reprPrec := PolarityItem.instReprDEStrength.repr }

@[instance_reducible]

instance PolarityItem.instFintypeDEStrength : Fintype DEStrength

Equations

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

def PolarityItem.DEStrength.toNat : DEStrength → ℕ

Rank in the chain weak < antiAdditive < antiMorphic.

Equations

• PolarityItem.DEStrength.weak.toNat = 0
• PolarityItem.DEStrength.antiAdditive.toNat = 1
• PolarityItem.DEStrength.antiMorphic.toNat = 2

theorem PolarityItem.DEStrength.toNat_injective : Function.Injective toNat

@[instance_reducible]

instance PolarityItem.instLinearOrderDEStrength : LinearOrder DEStrength

The Zwarts hierarchy as the linear order weak < antiAdditive < antiMorphic.

Equations

• PolarityItem.instLinearOrderDEStrength = LinearOrder.lift' PolarityItem.DEStrength.toNat PolarityItem.DEStrength.toNat_injective

def PolarityItem.DEStrength.toSignature : DEStrength → NaturalLogic.Signature

The natural-logic signature whose function class a strength of negation is: an antitone, an anti-additive or an anti-morphic map, with the unit conditions of [Ica12].

Equations

• PolarityItem.DEStrength.weak.toSignature = NaturalLogic.Signature.anti
• PolarityItem.DEStrength.antiAdditive.toSignature = NaturalLogic.Signature.antiAdd
• PolarityItem.DEStrength.antiMorphic.toSignature = NaturalLogic.Signature.antiAddMult

theorem PolarityItem.DEStrength.toSignature_antitone : Antitone toSignature

A stronger strength is a more specific signature.

Signatures and strength

def NaturalLogic.Signature.toDEStrength (φ : Signature) : WithBot PolarityItem.DEStrength

toDEStrength φ is the strength of negation the signature φ realizes, ⊥ when φ is not downward entailing. It is read off project: a signature is downward entailing when it reverses forward entailment, anti-additive when it also turns cover into alternation, and anti-morphic when it also turns alternation into cover.

Equations

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

theorem NaturalLogic.Signature.toDEStrength_ne_bot_iff (σ : Signature) : σ.toDEStrength ≠ ⊥ ↔ σ.sign = -1

A signature realizes a strength of negation exactly when it is downward entailing ([Lad79]).

theorem NaturalLogic.Signature.toDEStrength_toSignature (s : PolarityItem.DEStrength) : s.toSignature.toDEStrength = ↑s

A strength is the one its signature realizes.