@[reducible, inline]

abbrev Semantics.Entailment.Polarity.IsUpwardEntailing (f : Set World → Set World) : Prop

IsUpwardEntailing is an abbreviation for Monotone.

A context function f : Set World → Set World is upward entailing if it preserves the ordering: If p ≤ q, then f(p) ≤ f(q).

Equations

• Semantics.Entailment.Polarity.IsUpwardEntailing f = Monotone f

@[reducible, inline]

abbrev Semantics.Entailment.Polarity.IsDownwardEntailing (f : Set World → Set World) : Prop

IsDownwardEntailing is an abbreviation for Antitone.

A context function f : Set World → Set World is downward entailing if it reverses the ordering: If p ≤ q, then f(q) ≤ f(p).

Equations

• Semantics.Entailment.Polarity.IsDownwardEntailing f = Antitone f

@[reducible, inline]

abbrev Semantics.Entailment.Polarity.IsUE (f : Set World → Set World) : Prop

Equations

• Semantics.Entailment.Polarity.IsUE = Semantics.Entailment.Polarity.IsUpwardEntailing

@[reducible, inline]

abbrev Semantics.Entailment.Polarity.IsDE (f : Set World → Set World) : Prop

Equations

• Semantics.Entailment.Polarity.IsDE = Semantics.Entailment.Polarity.IsDownwardEntailing

theorem Semantics.Entailment.Polarity.id_isUpwardEntailing : IsUpwardEntailing id

Identity is UE.

theorem Semantics.Entailment.Polarity.pnot_isDownwardEntailing : IsDownwardEntailing pnot

Negation is DE.

theorem Semantics.Entailment.Polarity.pnot_pnot_isUpwardEntailing : IsUpwardEntailing (pnot ∘ pnot)

Double negation is UE.

theorem Semantics.Entailment.Polarity.ue_comp_ue {f g : Set World → Set World} (hf : IsUpwardEntailing f) (hg : IsUpwardEntailing g) : IsUpwardEntailing (f ∘ g)

UE ∘ UE = UE

theorem Semantics.Entailment.Polarity.de_comp_de {f g : Set World → Set World} (hf : IsDownwardEntailing f) (hg : IsDownwardEntailing g) : IsUpwardEntailing (f ∘ g)

DE ∘ DE = UE (double negation).

theorem Semantics.Entailment.Polarity.ue_comp_de {f g : Set World → Set World} (hf : IsUpwardEntailing f) (hg : IsDownwardEntailing g) : IsDownwardEntailing (f ∘ g)

UE ∘ DE = DE

theorem Semantics.Entailment.Polarity.de_comp_ue {f g : Set World → Set World} (hf : IsDownwardEntailing f) (hg : IsUpwardEntailing g) : IsDownwardEntailing (f ∘ g)

DE ∘ UE = DE

def Semantics.Entailment.Polarity.isUpwardEntailing (f : Set World → Set World) [(p : Set World) → [DecidablePred p] → DecidablePred (f p)] (tests : List (Set World × Set World)) : Prop

Check if f is upward entailing on given test cases (decidable approximation).

Equations

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

def Semantics.Entailment.Polarity.isDownwardEntailing (f : Set World → Set World) [(p : Set World) → [DecidablePred p] → DecidablePred (f p)] (tests : List (Set World × Set World)) : Prop

Check if f is downward entailing on given test cases (decidable approximation).

Equations

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

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

Negation reverses entailment.

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

DE contexts reverse scalar strength.

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

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

Equations

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

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

Conditional antecedent is DE.

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

Conditional consequent is UE.

structure Semantics.Entailment.Polarity.GroundedUE : Type

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

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

structure Semantics.Entailment.Polarity.GroundedDE : Type

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

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

inductive Semantics.Entailment.Polarity.GroundedPolarity : Type

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

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

def Semantics.Entailment.Polarity.GroundedPolarity.toContextPolarity : GroundedPolarity → ContextPolarity

Extract the ContextPolarity enum from a grounded polarity.

Equations

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

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

Equations

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

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

Equations

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

def Semantics.Entailment.Polarity.identityPolarity : GroundedPolarity

The identity context is grounded UE.

Equations

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

def Semantics.Entailment.Polarity.negationPolarity : GroundedPolarity

Negation is grounded DE.

Equations

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

def Semantics.Entailment.Polarity.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 Semantics.Entailment.Polarity.composePolarity_agrees (outer inner : GroundedPolarity) : (composePolarity outer inner).toContextPolarity = outer.toContextPolarity.compose inner.toContextPolarity

Grounded polarity composition agrees with ContextPolarity.compose.

theorem Semantics.Entailment.Polarity.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 = Core.NaturalLogic.ContextPolarity.upward

Double DE gives UE (grounded version).

def Semantics.Entailment.Polarity.implicatureAllowed (gp : GroundedPolarity) : Prop

Scalar implicatures require UE context.

Equations

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

theorem Semantics.Entailment.Polarity.implicature_allowed_identity : implicatureAllowed identityPolarity

Implicature is allowed in identity context.

theorem Semantics.Entailment.Polarity.implicature_blocked_negation : ¬implicatureAllowed negationPolarity

Implicature is blocked under single negation.

theorem Semantics.Entailment.Polarity.implicature_allowed_double_negation : implicatureAllowed (composePolarity negationPolarity negationPolarity)

Implicature is allowed under double negation.