Documentation

Linglib.Phenomena.Entailment.NegationTests

source
inductive Semantics.Entailment.NegationTests.Animal :
Type

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

Instances For
    source
    @[implicit_reducible]
    instance Semantics.Entailment.NegationTests.instDecidableEqAnimal :
    DecidableEq 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
      @[implicit_reducible]
      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 :
        Set Animal

        Proposition: x is a dog.

        Equations
        Instances For
          source
          def Semantics.Entailment.NegationTests.isAnimal :
          Set 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 → isAnimal x

            dogs subset animals: isDog |= isAnimal.

            source
            theorem Semantics.Entailment.NegationTests.negation_de_test (x : Animal) :
            ¬isAnimal x → ¬isDog x

            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.