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 Frame + Fintype instance so that the canonical GQ denotations from Semantics.Quantification.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 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 :
Core.Logic.Intensional.Frame

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

Equations
Instances For
    source
    @[implicit_reducible]
    instance Semantics.Entailment.Monotonicity.instFintypeEntityEntailmentModel :
    Fintype entailmentModel.Entity
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[implicit_reducible]
    instance Semantics.Entailment.Monotonicity.instDecidableEvery_semEntailmentModelOfDecidablePredEntity (R S : entailmentModel.Entity → Prop) [DecidablePred R] [DecidablePred S] :
    Decidable (Quantification.Quantifier.every_sem entailmentModel R S)
    Equations
    source
    @[implicit_reducible]
    instance Semantics.Entailment.Monotonicity.instDecidableSome_semEntailmentModelOfDecidablePredEntity (R S : entailmentModel.Entity → Prop) [DecidablePred R] [DecidablePred S] :
    Decidable (Quantification.Quantifier.some_sem entailmentModel R S)
    Equations
    source
    @[implicit_reducible]
    instance Semantics.Entailment.Monotonicity.instDecidableNo_semEntailmentModelOfDecidablePredEntity (R S : entailmentModel.Entity → Prop) [DecidablePred R] [DecidablePred S] :
    Decidable (Quantification.Quantifier.no_sem entailmentModel R S)
    Equations
    source
    def Semantics.Entailment.Monotonicity.every (a b : Set World) :
    Prop

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

    Equations
    Instances For
      source
      def Semantics.Entailment.Monotonicity.some' (a b : Set World) :
      Prop

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

      Equations
      Instances For
        source
        def Semantics.Entailment.Monotonicity.no (a b : Set World) :
        Prop

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

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

            "Every student" as a function of scope.

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

              "Some student" as a function of scope.

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

                "No student" as a function of scope.

                Equations
                Instances For
                  source
                  theorem Semantics.Entailment.Monotonicity.every_scope_UE :
                  Polarity.IsUpwardEntailing every_scope

                  "Every" is UE in scope.

                  source
                  theorem Semantics.Entailment.Monotonicity.some_scope_UE :
                  Polarity.IsUpwardEntailing some_scope

                  "Some" is UE in scope.

                  source
                  theorem Semantics.Entailment.Monotonicity.no_scope_DE :
                  Polarity.IsDownwardEntailing no_scope

                  "No" is DE in scope.

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

                  Fixed scope for testing restrictor monotonicity.

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

                    "Every ___ smokes" as a function of restrictor.

                    Equations
                    Instances For
                      source
                      theorem Semantics.Entailment.Monotonicity.every_restr_DE :
                      Polarity.IsDownwardEntailing every_restr

                      "Every" is DE in restrictor.