Documentation

Linglib.Logic.Trivalent.Propositional

Trivalent propositional logic #

Propositional formulas built from atoms by negation, conjunction, disjunction and the conditional are evaluated into SignType by an interpretation of the binary connectives, the Strong, Weak or Middle Kleene tables or Cooper's or de Finetti's, with Kleene's negation throughout. A formula is realized at a designation standard when its value is designated: K3 designates only 1 and LP also 0, so one evaluation yields both logics, and mixed consequence takes premises at one standard and conclusions at another, as Cobreros, Égré, Ripley and van Rooij do.

Main definitions #

Main results #

Implementation notes #

The API mirrors Mathlib.ModelTheory (Realize, per-constructor @[simp] lemmas, ⊨ notation), and consequence is the multiple-conclusion, list-based MixedConsequence rather than theories as sets. The language has no constants, so ⊤ and ⊥ are p ∨ ¬p and p ∧ ¬p for an atom p, and the model sending every atom to 0 voids every formula under the Strong Kleene tables.

References #

source
inductive Trivalent.Formula (Atom : Type u_1) :
Type u_1

Propositional formulas over an atom type, built by negation, conjunction, disjunction and the conditional.

Instances For
    source
    def Trivalent.instDecidableEqFormula.decEq {Atom✝ : Type u_1} [DecidableEq Atom✝] (x✝ x✝¹ : Formula Atom✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Trivalent.instDecidableEqFormula {Atom✝ : Type u_1} [DecidableEq Atom✝] :
      DecidableEq (Formula Atom✝)
      Equations
      source
      @[reducible, inline]
      abbrev Trivalent.Model (Atom : Type u_1) :
      Type u_1

      A trivalent model assigns a value to each atom.

      Equations
      Instances For
        source
        def Trivalent.Model.ofBool {Atom : Type u_1} (v : Atom → Bool) :
        Model Atom

        The Boolean model of a classical valuation of the atoms, which leaves no atom void.

        Equations
        Instances For
          source
          @[simp]
          theorem Trivalent.Model.ofBool_apply {Atom : Type u_1} (v : Atom → Bool) (a : Atom) :
          ofBool v a = SignType.ofProp (v a = true)
          source
          def Trivalent.Formula.eval {Atom : Type u_1} (C : Connectives) (M : Model Atom) :
          Formula Atom → SignType

          The value of a formula under the connectives C in the model M.

          Equations
          Instances For
            source
            @[simp]
            theorem Trivalent.Formula.eval_atom {Atom : Type u_1} (C : Connectives) (M : Model Atom) (a : Atom) :
            eval C M (atom a) = M a
            source
            @[simp]
            theorem Trivalent.Formula.eval_neg {Atom : Type u_1} (C : Connectives) (M : Model Atom) (φ : Formula Atom) :
            eval C M φ.neg = -eval C M φ
            source
            @[simp]
            theorem Trivalent.Formula.eval_conj {Atom : Type u_1} (C : Connectives) (M : Model Atom) (φ ψ : Formula Atom) :
            eval C M (φ.conj ψ) = C.conj (eval C M φ) (eval C M ψ)
            source
            @[simp]
            theorem Trivalent.Formula.eval_disj {Atom : Type u_1} (C : Connectives) (M : Model Atom) (φ ψ : Formula Atom) :
            eval C M (φ.disj ψ) = C.disj (eval C M φ) (eval C M ψ)
            source
            @[simp]
            theorem Trivalent.Formula.eval_cond {Atom : Type u_1} (C : Connectives) (M : Model Atom) (φ ψ : Formula Atom) :
            eval C M (φ.cond ψ) = C.cond (eval C M φ) (eval C M ψ)
            source
            def Trivalent.Formula.evalBool {Atom : Type u_1} (v : Atom → Bool) :
            Formula Atom → Bool

            Classical evaluation on a Boolean valuation.

            Equations
            Instances For
              source
              @[simp]
              theorem Trivalent.Formula.evalBool_atom {Atom : Type u_1} (v : Atom → Bool) (a : Atom) :
              evalBool v (atom a) = v a
              source
              @[simp]
              theorem Trivalent.Formula.evalBool_neg {Atom : Type u_1} (v : Atom → Bool) (φ : Formula Atom) :
              evalBool v φ.neg = !evalBool v φ
              source
              @[simp]
              theorem Trivalent.Formula.evalBool_conj {Atom : Type u_1} (v : Atom → Bool) (φ ψ : Formula Atom) :
              evalBool v (φ.conj ψ) = (evalBool v φ && evalBool v ψ)
              source
              @[simp]
              theorem Trivalent.Formula.evalBool_disj {Atom : Type u_1} (v : Atom → Bool) (φ ψ : Formula Atom) :
              evalBool v (φ.disj ψ) = (evalBool v φ || evalBool v ψ)
              source
              @[simp]
              theorem Trivalent.Formula.evalBool_cond {Atom : Type u_1} (v : Atom → Bool) (φ ψ : Formula Atom) :
              evalBool v (φ.cond ψ) = (!evalBool v φ || evalBool v ψ)
              source
              theorem Trivalent.Formula.eval_ofBool {Atom : Type u_1} (v : Atom → Bool) (φ : Formula Atom) :
              eval Connectives.strongKleene (Model.ofBool v) φ = SignType.ofProp (evalBool v φ = true)

              On a Boolean model the strong Kleene tables are the classical ones.

              source
              def Trivalent.Formula.Realize {Atom : Type u_1} (C : Connectives) (M : Model Atom) (d : Designation) (φ : Formula Atom) :
              Prop

              A formula is realized at a designation standard when its value under the connectives clears the threshold, so with the strong Kleene connectives Realize .strongKleene M .k3 is strong Kleene satisfaction and Realize .strongKleene M .lp is Priest's LP.

              Equations
              Instances For
                source
                def Trivalent.Formula.«term_⊨[_,_]_» :
                Lean.TrailingParserDescr

                A formula is realized at a designation standard when its value under the connectives clears the threshold, so with the strong Kleene connectives Realize .strongKleene M .k3 is strong Kleene satisfaction and Realize .strongKleene M .lp is Priest's LP.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem Trivalent.Formula.realize_atom {Atom : Type u_1} (C : Connectives) (M : Model Atom) (d : Designation) (a : Atom) :
                  Realize C M d (atom a) ↔ d.threshold ≤ M a
                  source
                  @[simp]
                  theorem Trivalent.Formula.realize_neg {Atom : Type u_1} (C : Connectives) (M : Model Atom) (d : Designation) (φ : Formula Atom) :
                  Realize C M d φ.neg ↔ ¬Realize C M d.dual φ

                  Negation swaps the designation standards at the level of formulas, under any connectives.

                  source
                  theorem Trivalent.Formula.isDual {Atom : Type u_1} (C : Connectives) (d : Designation) :
                  Consequence.IsDual neg (fun (M : Model Atom) => Realize C M d.dual) fun (x : Model Atom) => Realize C x d

                  Each standard is dual to the other along negation ([CERvR12], Definition 20).

                  source
                  theorem Trivalent.Formula.realize_ofBool {Atom : Type u_1} (d : Designation) (v : Atom → Bool) (φ : Formula Atom) :
                  Realize Connectives.strongKleene (Model.ofBool v) d φ ↔ evalBool v φ = true

                  On a Boolean model every standard is classical truth, under the strong Kleene connectives.

                  source
                  @[simp]
                  theorem Trivalent.Formula.realize_conj {Atom : Type u_1} (M : Model Atom) (d : Designation) (φ ψ : Formula Atom) :
                  Realize Connectives.strongKleene M d (φ.conj ψ) ↔ Realize Connectives.strongKleene M d φ ∧ Realize Connectives.strongKleene M d ψ

                  Strong Kleene realization distributes over conjunction at either standard.

                  source
                  @[simp]
                  theorem Trivalent.Formula.realize_disj {Atom : Type u_1} (M : Model Atom) (d : Designation) (φ ψ : Formula Atom) :
                  Realize Connectives.strongKleene M d (φ.disj ψ) ↔ Realize Connectives.strongKleene M d φ ∨ Realize Connectives.strongKleene M d ψ
                  source
                  @[simp]
                  theorem Trivalent.Formula.realize_cond {Atom : Type u_1} (M : Model Atom) (d : Designation) (φ ψ : Formula Atom) :
                  Realize Connectives.strongKleene M d (φ.cond ψ) ↔ Realize Connectives.strongKleene M d.dual φ → Realize Connectives.strongKleene M d ψ

                  A strong Kleene conditional is realized at d iff its consequent is whenever its antecedent is realized at the dual standard.

                  source
                  @[reducible, inline]
                  abbrev Trivalent.Consequence {Atom : Type u_1} (C : Connectives) (m n : Designation) (Γ Δ : List (Formula Atom)) :
                  Prop

                  Mixed consequence under the connectives C takes premises at standard m and conclusions at standard n.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Meta-theorems #

                    source
                    theorem Trivalent.consequence_iff_dual {Atom : Type u_1} {C : Connectives} {m n : Designation} {Γ Δ : List (Formula Atom)} :
                    Consequence C m n Γ Δ ↔ Consequence C n.dual m.dual (List.map Formula.neg Δ) (List.map Formula.neg Γ)

                    Negation dualizes consequence, so Γ ⊨ Δ at m, n iff ¬Δ ⊨ ¬Γ at the dual standards, and K3 and LP are each other's duals ([CERvR12], Lemma 6).

                    source
                    theorem Trivalent.eval_const_zero {Atom : Type u_1} (φ : Formula Atom) :
                    Formula.eval Connectives.strongKleene (fun (x : Atom) => 0) φ = 0

                    In the strong Kleene model sending every atom to 0 every formula evaluates to 0.

                    source
                    theorem Trivalent.k3_no_tautologies {Atom : Type u_1} [Nonempty Atom] (φ : Formula Atom) :
                    ¬∀ (M : Model Atom), Formula.Realize Connectives.strongKleene M Designation.k3 φ

                    K3 has no tautologies, since nothing is designated in the model sending every atom to 0 ([CERvR12], Theorem 2).

                    source
                    theorem Trivalent.lp_all_satisfiable {Atom : Type u_1} (φ : Formula Atom) :
                    Formula.Realize Connectives.strongKleene (fun (x : Atom) => 0) Designation.lp φ

                    Every formula is LP-satisfiable, since the model sending every atom to 0 designates everything ([CERvR12], Theorem 2).

                    source
                    theorem Trivalent.lp_no_explosion :
                    ∃ (φ : Formula Bool) (ψ : Formula Bool), ¬Consequence Connectives.strongKleene Designation.lp Designation.lp [φ.conj φ.neg] [ψ]

                    Explosion fails in LP, since {a ∧ ¬a} ⊭ b with countermodel M a = 0 and M b = -1.