Documentation

Linglib.Theories.Semantics.Entailment.Monotonicity

Bridge to Canonical GQ Denotations #

The 4-element World type used in the entailment domain doubles as an entity domain. We create a Model + Fintype instance so that the canonical GQ denotations from Semantics.Lexical.Determiner.Quantifier (every_sem, some_sem, no_sem) can be instantiated here.

This bridges the entailment-testing infrastructure (finite, decidable) with the model-theoretic GQ definitions (proved conservative and monotone for arbitrary finite models).

Relation to general monotonicity theorems. The native_decide proofs below verify monotonicity over the 4-element World model. The general theorems — every_scope_up, no_scope_down, every_restrictor_down, some_scope_up — are proved for arbitrary Fintype in Quantifier.lean and Core.Logic.Quantification. The results here are consistent instances of those general proofs.

source
def Semantics.Entailment.Monotonicity.entailmentModel :
Montague.Model

The entailment World type, viewed as a Model entity domain.

Equations
Instances For
    source
    instance Semantics.Entailment.Monotonicity.instFintypeEntityEntailmentModel :
    Fintype entailmentModel.Entity
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[reducible, inline]
    abbrev Semantics.Entailment.Monotonicity.every (a b : World → Bool) :
    Bool

    "Every A is B" — delegates to canonical every_sem.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Semantics.Entailment.Monotonicity.some' (a b : World → Bool) :
      Bool

      "Some A is B" — delegates to canonical some_sem.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Semantics.Entailment.Monotonicity.no (a b : World → Bool) :
        Bool

        "No A is B" — delegates to canonical no_sem.

        Equations
        Instances For
          source
          def Semantics.Entailment.Monotonicity.fixedRestr :
          BProp World
          Equations
          Instances For
            source
            def Semantics.Entailment.Monotonicity.every_scope :
            BProp World → BProp World

            "Every student" as a function of scope.

            Equations
            Instances For
              source
              def Semantics.Entailment.Monotonicity.some_scope :
              BProp World → BProp World

              "Some student" as a function of scope.

              Equations
              Instances For
                source
                def Semantics.Entailment.Monotonicity.no_scope :
                BProp World → BProp World

                "No student" as a function of scope.

                Equations
                Instances For
                  source
                  theorem Semantics.Entailment.Monotonicity.every_scope_UE :
                  Polarity.isUpwardEntailing every_scope testCases = true

                  "Every" is UE in scope.

                  source
                  theorem Semantics.Entailment.Monotonicity.some_scope_UE :
                  Polarity.isUpwardEntailing some_scope testCases = true

                  "Some" is UE in scope.

                  source
                  theorem Semantics.Entailment.Monotonicity.no_scope_DE :
                  Polarity.isDownwardEntailing no_scope testCases = true

                  "No" is DE in scope.

                  source
                  def Semantics.Entailment.Monotonicity.fixedScope :
                  BProp World

                  Fixed scope for testing restrictor monotonicity.

                  Equations
                  Instances For
                    source
                    def Semantics.Entailment.Monotonicity.every_restr :
                    BProp World → BProp World

                    "Every ___ smokes" as a function of restrictor.

                    Equations
                    Instances For
                      source
                      theorem Semantics.Entailment.Monotonicity.every_restr_DE :
                      Polarity.isDownwardEntailing every_restr testCases = true

                      "Every" is DE in restrictor.