Documentation

Linglib.Phenomena.Entailment.NegationTests

source
inductive Semantics.Entailment.NegationTests.Animal :
Type

A simple domain with dogs and cats (both animals).

Instances For
    source
    instance Semantics.Entailment.NegationTests.instDecidableEqAnimal :
    DecidableEq Animal
    Equations
    source
    def Semantics.Entailment.NegationTests.instBEqAnimal.beq :
    Animal → Animal → Bool
    Equations
    Instances For
      source
      instance Semantics.Entailment.NegationTests.instBEqAnimal :
      BEq Animal
      Equations
      source
      def Semantics.Entailment.NegationTests.instReprAnimal.repr :
      Animal → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Semantics.Entailment.NegationTests.instReprAnimal :
        Repr Animal
        Equations
        source
        def Semantics.Entailment.NegationTests.allAnimals :
        List Animal
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Semantics.Entailment.NegationTests.isDog :
          BProp Animal

          Proposition: x is a dog.

          Equations
          Instances For
            source
            def Semantics.Entailment.NegationTests.isAnimal :
            BProp Animal

            Proposition: x is an animal (tautology in this domain).

            Equations
            Instances For
              source
              theorem Semantics.Entailment.NegationTests.dogs_subset_animals (x : Animal) :
              isDog x = true → isAnimal x = true

              dogs subset animals: isDog |= isAnimal.

              source
              theorem Semantics.Entailment.NegationTests.negation_de_test (x : Animal) :
              Core.Proposition.Decidable.pnot Animal isAnimal x = true → Core.Proposition.Decidable.pnot Animal isDog x = true

              Negation is DE: dogs <= animals implies not-animal <= not-dog.

              source
              theorem Semantics.Entailment.NegationTests.de_prediction_matches_data :
              Phenomena.Negation.negation_de_valid.judgedValid = true

              DE prediction matches negation_de_valid.

              source
              theorem Semantics.Entailment.NegationTests.not_ue_prediction_matches_data :
              Phenomena.Negation.negation_not_ue.judgedValid = false

              Not-UE prediction matches negation_not_ue.

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

              Double negation is UE (DE comp DE = UE).

              source
              theorem Semantics.Entailment.NegationTests.double_neg_prediction_matches_data :
              Phenomena.Negation.double_negation_ue.judgedValid = true

              Double negation prediction matches double_negation_ue.

              source
              theorem Semantics.Entailment.NegationTests.all_predictions_match :
              Phenomena.Negation.negation_de_valid.judgedValid = true ∧ Phenomena.Negation.negation_not_ue.judgedValid = false ∧ Phenomena.Negation.double_negation_ue.judgedValid = true

              All negation predictions from formal semantics match empirical judgments.