Documentation

Linglib.Theories.Semantics.Entailment.Polarity

source
@[reducible, inline]
abbrev Semantics.Entailment.Polarity.IsUpwardEntailing (f : BProp World → BProp World) :
Prop

IsUpwardEntailing is an abbreviation for Monotone.

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

Examples: "some", "or", scope of "every"

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Semantics.Entailment.Polarity.IsDownwardEntailing (f : BProp World → BProp World) :
    Prop

    IsDownwardEntailing is an abbreviation for Antitone.

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

    Examples: "no", "not", restrictor of "every"

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Semantics.Entailment.Polarity.IsUE (f : BProp World → BProp World) :
      Prop
      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Semantics.Entailment.Polarity.IsDE (f : BProp World → BProp World) :
        Prop
        Equations
        Instances For
          source
          theorem Semantics.Entailment.Polarity.id_isUpwardEntailing :
          IsUpwardEntailing id

          Identity is UE: The trivial context preserves entailment.

          source
          theorem Semantics.Entailment.Polarity.pnot_isDownwardEntailing :
          IsDownwardEntailing pnot

          Negation is DE: If P ⊆ Q, then ¬Q ⊆ ¬P.

          Uses Core.Proposition.Decidable.pnot_antitone for the proof.

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

          Double negation is UE: negating twice preserves entailment.

          This follows from Mathlib's Antitone.comp (DE ∘ DE = UE).

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

          UE ∘ UE = UE (from Mathlib)

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

          DE ∘ DE = UE (double negation).

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

          UE ∘ DE = DE (from Mathlib)

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

          DE ∘ UE = DE (from Mathlib)

          source
          def Semantics.Entailment.Polarity.isUpwardEntailing (f : BProp World → BProp World) (tests : List (BProp World × BProp World)) :
          Bool

          Check if f is upward entailing on given test cases.

          This is a decidable approximation: it checks the property on a finite set of test cases rather than proving it universally.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Semantics.Entailment.Polarity.isDownwardEntailing (f : BProp World → BProp World) (tests : List (BProp World × BProp World)) :
            Bool

            Check if f is downward entailing on given test cases.

            This is a decidable approximation: it checks the property on a finite set of test cases rather than proving it universally.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Semantics.Entailment.Polarity.negation_is_DE :
              isDownwardEntailing pnot testCases = true

              Negation is Downward Entailing.

              If P ⊨ Q, then ¬Q ⊨ ¬P

              Test: p0 ⊨ p01, so ¬p01 ⊨ ¬p0

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

              Negation reverses entailment.

              p0 ⊨ p01 (true in {w0} entails true in {w0,w1}) ¬p01 ⊨ ¬p0 (false in {w0,w1} entails false in {w0})

              source
              theorem Semantics.Entailment.Polarity.conjunction_second_UE :
              isUpwardEntailing (pand p01) testCases = true

              Conjunction (second arg) is Upward Entailing.

              If P ⊨ Q, then (R ∧ P) ⊨ (R ∧ Q)

              source
              theorem Semantics.Entailment.Polarity.disjunction_second_UE :
              isUpwardEntailing (por p01) testCases = true

              Disjunction (second arg) is Upward Entailing.

              If P ⊨ Q, then (R ∨ P) ⊨ (R ∨ Q)

              source
              theorem Semantics.Entailment.Polarity.double_negation_is_ue :
              isUpwardEntailing (pnot ∘ pnot) testCases = true

              Double negation is UE (decidable verification).

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

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

              Equations
              Instances For
                source
                theorem Semantics.Entailment.Polarity.conditional_antecedent_DE :
                isDownwardEntailing (materialCond p012) testCases = true

                Conditional antecedent is Downward Entailing.

                If P ⊨ Q, then "If Q, C" ⊨ "If P, C"

                This is the core DE property of conditional antecedents: strengthening the antecedent weakens the conditional (via contraposition).

                Example: "dogs" ⊨ "animals", so "If it's an animal, it barks" ⊨ "If it's a dog, it barks"

                source
                theorem Semantics.Entailment.Polarity.implication_consequent_UE :
                isUpwardEntailing (fun (c : BProp World) => materialCond c p01) testCases = true

                Implication second argument is UE.

                If P ⊨ Q, then (A → P) ⊨ (A → Q)

                The consequent position of a conditional is upward entailing.

                source
                theorem Semantics.Entailment.Polarity.conditional_monotonicity_summary :
                isDownwardEntailing (materialCond p012) testCases = true ∧ isUpwardEntailing (fun (c : BProp World) => materialCond c p01) testCases = true

                Conditional positions and monotonicity.

                • Antecedent position: DE (strengthening weakens the conditional)
                • Consequent position: UE (strengthening strengthens the conditional)

                This explains scalar implicature patterns:

                • "If some passed, happy" - antecedent is DE, so SI blocked (global preferred)
                • "If passed, happy about some" - consequent is UE, so SI computed (local available)
                source
                theorem Semantics.Entailment.Polarity.de_reverses_strength :
                entails p0 p01 = true ∧ entails (pnot p01) (pnot p0) = true

                DE contexts reverse scalar strength.

                In UE: all ⊢ some (all is stronger, "some" implicates "not all") In DE: some ⊢ all (some is stronger, no "not all" implicature)

                source
                structure Semantics.Entailment.Polarity.GroundedUE :
                Type

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

                Instances For
                  source
                  structure Semantics.Entailment.Polarity.GroundedDE :
                  Type

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

                  Instances For
                    source
                    inductive Semantics.Entailment.Polarity.GroundedPolarity :
                    Type

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

                    Instances For
                      source
                      def Semantics.Entailment.Polarity.GroundedPolarity.toContextPolarity :
                      GroundedPolarity → ContextPolarity

                      Extract the ContextPolarity enum from a grounded polarity.

                      Equations
                      Instances For
                        source
                        def Semantics.Entailment.Polarity.mkUpward (ctx : BProp World → BProp World) (h : Monotone ctx) :
                        GroundedPolarity

                        Create a grounded UE polarity from a proof.

                        Equations
                        Instances For
                          source
                          def Semantics.Entailment.Polarity.mkDownward (ctx : BProp World → BProp World) (h : Antitone ctx) :
                          GroundedPolarity

                          Create a grounded DE polarity from a proof.

                          Equations
                          Instances For
                            source
                            def Semantics.Entailment.Polarity.identityPolarity :
                            GroundedPolarity

                            The identity context is grounded UE.

                            Equations
                            Instances For
                              source
                              def Semantics.Entailment.Polarity.negationPolarity :
                              GroundedPolarity

                              Negation is grounded DE.

                              Equations
                              Instances For
                                source
                                def Semantics.Entailment.Polarity.composePolarity (outer inner : GroundedPolarity) :
                                GroundedPolarity

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

                                The case analysis mirrors ContextPolarity.compose (which is derived from the EntailmentSig monoid), but additionally carries Mathlib proof witnesses:

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  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.

                                  This connects the proof-carrying system to the algebraic system: the Mathlib composition lemmas produce the same polarity classification as the monoid-derived ContextPolarity.compose.

                                  source
                                  theorem Semantics.Entailment.Polarity.double_de_is_ue_grounded (f g : BProp World → BProp 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).

                                  "It's not the case that no one..." creates a UE context.

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

                                  Scalar implicatures require UE context.

                                  In a DE context, the alternatives reverse, so "not all" doesn't follow from "some". This function captures that constraint.

                                  Equations
                                  Instances For
                                    source
                                    theorem Semantics.Entailment.Polarity.implicature_allowed_identity :
                                    implicatureAllowed identityPolarity

                                    Implicature is allowed in identity context.

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

                                    Implicature is blocked under single negation.

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

                                    Implicature is allowed under double negation.

                                    "It's not the case that John didn't eat some of the cookies" → Can derive "not all" implicature because double DE = UE!