Documentation

Linglib.Semantics.Exhaustification.Trivalent

Trivalent exhaustification #

This file defines Spector and Sudo's two trivalent exhaustification operators. Both assert the prejacent and deny its innocently excludable alternatives, computed by Fox's algorithm on the classical truth conditions; they differ in the negation applied to a denied alternative. exh1 uses weak negation, under which an undefined alternative counts as denied, so the operator is undefined exactly where the prejacent is (exh1_eq_zero_iff). exh2 uses strong negation, under which an undefined alternative leaves the whole undefined, so the operator inherits the presuppositions of the alternatives it denies (exh2_eq_zero_iff).

Implementation notes #

The innocently excludable alternatives are Exhaustification.innocent.excluded applied to the classical parts of the trivalent propositions, where the classical part sends 1 to true and both -1 and 0 to false.

References #

source
def Exhaustification.Trivalent.classicalPart {W : Type} (p : W → SignType) :
W → Bool

The classical truth conditions of a trivalent proposition hold exactly where it is 1.

Equations
Instances For
    source
    def Exhaustification.Trivalent.excluded {W : Type} [Fintype W] [DecidableEq W] (alts : List (W → SignType)) (p : W → SignType) :
    Finset (Finset W)

    The innocently excludable alternatives of a trivalent prejacent, computed classically.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Exhaustification.Trivalent.exh1 {W : Type} [Fintype W] [DecidableEq W] (alts : List (W → SignType)) (p : W → SignType) :
      W → SignType

      Weak-negation exhaustification is 1 where the prejacent is 1 and no excludable alternative is, -1 where the prejacent is -1 or some excludable alternative is 1, and 0 where the prejacent is 0.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Exhaustification.Trivalent.exh2 {W : Type} [Fintype W] [DecidableEq W] (alts : List (W → SignType)) (p : W → SignType) :
        W → SignType

        Strong-negation exhaustification is 0 where the prejacent or some excludable alternative is 0, 1 where the prejacent is 1 and every excludable alternative is -1, and -1 otherwise.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Exhaustification.Trivalent.exh1_eq_zero_iff {W : Type} [Fintype W] [DecidableEq W] (alts : List (W → SignType)) (p : W → SignType) (w : W) :
          exh1 alts p w = 0 ↔ p w = 0

          exh1 presupposes exactly what its prejacent presupposes.

          source
          theorem Exhaustification.Trivalent.exh2_eq_zero_iff {W : Type} [Fintype W] [DecidableEq W] (alts : List (W → SignType)) (p : W → SignType) (w : W) :
          exh2 alts p w = 0 ↔ p w = 0 ∨ ∃ q ∈ alts, predToFinset (classicalPart q) ∈ excluded alts p ∧ q w = 0

          exh2 presupposes what its prejacent and its excludable alternatives presuppose.

          source
          theorem Exhaustification.Trivalent.exh1_preserves_presup {W : Type} [Fintype W] [DecidableEq W] (alts : List (W → SignType)) (p : W → SignType) (w : W) (h : p w = 0) :
          exh1 alts p w = 0
          source
          theorem Exhaustification.Trivalent.exh2_preserves_presup {W : Type} [Fintype W] [DecidableEq W] (alts : List (W → SignType)) (p : W → SignType) (w : W) (h : p w = 0) :
          exh2 alts p w = 0