Grounded context polarity

Semantic grounding for ContextPolarity (defined in NaturalLogic) via mathlib's Monotone/Antitone infrastructure: IsUpwardEntailing/ IsDownwardEntailing abbreviate Monotone/Antitone on Set α → Set β, so the composition rules (UE ∘ UE = UE, DE ∘ DE = UE, mixed = DE) are Monotone.comp/Antitone.comp and friends. The polarity composition rules are a homomorphic image of the EntailmentSig monoid — see EntailmentSig.toContextPolarity_compose. GroundedPolarity bundles a context function with its monotonicity proof on the toy World model.

@[reducible, inline]

abbrev Entailment.IsUpwardEntailing {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

A context function is upward entailing if it preserves entailment: Monotone on sets of worlds.

Equations

• Entailment.IsUpwardEntailing f = Monotone f

@[reducible, inline]

abbrev Entailment.IsDownwardEntailing {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

A context function is downward entailing if it reverses entailment: Antitone on sets of worlds.

Equations

• Entailment.IsDownwardEntailing f = Antitone f

@[reducible, inline]

abbrev Entailment.IsUE {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

Equations

• Entailment.IsUE f = Entailment.IsUpwardEntailing f

@[reducible, inline]

abbrev Entailment.IsDE {α : Type u_1} {β : Type u_2} (f : Set α → Set β) : Prop

Equations

• Entailment.IsDE f = Entailment.IsDownwardEntailing f

theorem Entailment.id_isUpwardEntailing : IsUpwardEntailing id

Identity is UE.

theorem Entailment.pnot_isDownwardEntailing : IsDownwardEntailing pnot

Negation is DE.

theorem Entailment.pnot_pnot_isUpwardEntailing : IsUpwardEntailing (pnot ∘ pnot)

Double negation is UE.

theorem Entailment.ue_comp_ue {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Set β → Set γ} {g : Set α → Set β} (hf : IsUpwardEntailing f) (hg : IsUpwardEntailing g) : IsUpwardEntailing (f ∘ g)

UE ∘ UE = UE

theorem Entailment.de_comp_de {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Set β → Set γ} {g : Set α → Set β} (hf : IsDownwardEntailing f) (hg : IsDownwardEntailing g) : IsUpwardEntailing (f ∘ g)

DE ∘ DE = UE (double negation).

theorem Entailment.ue_comp_de {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Set β → Set γ} {g : Set α → Set β} (hf : IsUpwardEntailing f) (hg : IsDownwardEntailing g) : IsDownwardEntailing (f ∘ g)

UE ∘ DE = DE

theorem Entailment.de_comp_ue {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Set β → Set γ} {g : Set α → Set β} (hf : IsDownwardEntailing f) (hg : IsUpwardEntailing g) : IsDownwardEntailing (f ∘ g)

DE ∘ UE = DE

theorem Entailment.negation_reverses_example : entails p0 p01 ∧ entails (pnot p01) (pnot p0)

Negation reverses entailment.

theorem Entailment.de_reverses_strength : entails p0 p01 ∧ entails (pnot p01) (pnot p0)

DE contexts reverse scalar strength.

def Entailment.materialCond (c : Set World) : Set World → Set World

Material conditional with fixed consequent: "If _, then c"

Equations

• Entailment.materialCond c p w = (p w → c w)

theorem Entailment.materialCond_antecedent_DE (c : Set World) : IsDownwardEntailing (materialCond c)

Conditional antecedent is DE.

theorem Entailment.materialCond_consequent_UE (a : Set World) : IsUpwardEntailing fun (c : Set World) => materialCond c a

Conditional consequent is UE.

structure Entailment.GroundedUE : Type

A grounded UE polarity carries proof that a context function is monotone.

• context : Set World → Set World
• witness : Monotone self.context

structure Entailment.GroundedDE : Type

A grounded DE polarity carries proof that a context function is antitone.

• context : Set World → Set World
• witness : Antitone self.context

inductive Entailment.GroundedPolarity : Type

A grounded polarity is either UE or DE, with proof.

• ue : GroundedUE → GroundedPolarity
• de : GroundedDE → GroundedPolarity

def Entailment.GroundedPolarity.toContextPolarity : GroundedPolarity → ContextPolarity

Extract the ContextPolarity enum from a grounded polarity.

Equations

• (Entailment.GroundedPolarity.ue a).toContextPolarity = NaturalLogic.ContextPolarity.upward
• (Entailment.GroundedPolarity.de a).toContextPolarity = NaturalLogic.ContextPolarity.downward

def Entailment.mkUpward (ctx : Set World → Set World) (h : Monotone ctx) : GroundedPolarity

Equations

• Entailment.mkUpward ctx h = Entailment.GroundedPolarity.ue { context := ctx, witness := h }

def Entailment.mkDownward (ctx : Set World → Set World) (h : Antitone ctx) : GroundedPolarity

Equations

• Entailment.mkDownward ctx h = Entailment.GroundedPolarity.de { context := ctx, witness := h }

def Entailment.identityPolarity : GroundedPolarity

The identity context is grounded UE.

Equations

• Entailment.identityPolarity = Entailment.mkUpward id Entailment.id_isUpwardEntailing

def Entailment.negationPolarity : GroundedPolarity

Negation is grounded DE.

Equations

• Entailment.negationPolarity = Entailment.mkDownward Entailment.pnot Entailment.pnot_isDownwardEntailing

def Entailment.composePolarity (outer inner : GroundedPolarity) : GroundedPolarity

Compose two grounded polarities, with proof that the composition has the right property.

Equations

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

theorem Entailment.composePolarity_agrees (outer inner : GroundedPolarity) : (composePolarity outer inner).toContextPolarity = outer.toContextPolarity.compose inner.toContextPolarity

Grounded polarity composition agrees with ContextPolarity.compose.

theorem Entailment.double_de_is_ue_grounded (f g : Set World → Set World) (hf : Antitone f) (hg : Antitone g) : (composePolarity (mkDownward f hf) (mkDownward g hg)).toContextPolarity = NaturalLogic.ContextPolarity.upward

Double DE gives UE (grounded version).

def Entailment.implicatureAllowed (gp : GroundedPolarity) : Prop

Scalar implicatures require UE context.

Equations

• Entailment.implicatureAllowed gp = (gp.toContextPolarity = NaturalLogic.ContextPolarity.upward)

theorem Entailment.implicature_allowed_identity : implicatureAllowed identityPolarity

Implicature is allowed in identity context.

theorem Entailment.implicature_blocked_negation : ¬implicatureAllowed negationPolarity

Implicature is blocked under single negation.

theorem Entailment.implicature_allowed_double_negation : implicatureAllowed (composePolarity negationPolarity negationPolarity)

Implicature is allowed under double negation.