Sheffer

Difficulty: moderate — 5 definitions, 0 abbreviations, 1 lemmas, 2 theorems, 0 examples.

definition lemma theorem
legend

The Sheffer stroke (“not both”) is a single connective from which every other connective can be built: negation, conjunction, and disjunction each reduce to a couple of Sheffer strokes (De Morgan for disjunction), and implication reduces via \(\varphi \to \psi = \lnot\varphi \lor \psi\).

Since it alone can express negation, conjunction, and disjunction, and those three are already functionally complete (PropositionalLogic.Formula.exists_andOrNot_of_boolFun), the Sheffer stroke alone is functionally complete too.

The Sheffer stroke (“not both”): the single connective from which every other connective can be built.

def Logic.PropositionalLogic.Formula.nand {α : Type} (φ ψ : Logic.PropositionalLogic.Formula α) :
  Logic.PropositionalLogic.Formula α
Show details 
| φ.nand ψ = (φ.and ψ).neg

Complexity: 21 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula

Used by: Logic.PropositionalLogic.NandFormula.toFormula

A formula built from atoms using only the Sheffer stroke.

inductive Logic.PropositionalLogic.NandFormula (α : Type) : Type
  • atom : α → Logic.PropositionalLogic.NandFormula α
  • nand : Logic.PropositionalLogic.NandFormula α →
Logic.PropositionalLogic.NandFormula α → Logic.PropositionalLogic.NandFormula α
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, HEq, Nat, Nat.ble, PProd, PULift, PUnit, SizeOf, cond, eq_of_heq

Used by: Logic.PropositionalLogic.NandFormula.exists_nand_of_boolFun, Logic.PropositionalLogic.NandFormula.ofFormula, Logic.PropositionalLogic.NandFormula.toFormula, Logic.PropositionalLogic.NandFormula.toFormula_val, Logic.PropositionalLogic.NandFormula.val

The truth table of a Sheffer-stroke-only formula: the same rule as PropositionalLogic.Formula.nand at every step.

def Logic.PropositionalLogic.NandFormula.val {α : Type} (v : Logic.PropositionalLogic.Valuation α) :
  Logic.PropositionalLogic.NandFormula α → Bool
Show details 
| Logic.PropositionalLogic.NandFormula.val v (Logic.PropositionalLogic.NandFormula.atom a) = v a
| Logic.PropositionalLogic.NandFormula.val v (φ.nand ψ) =
  !(Logic.PropositionalLogic.NandFormula.val v φ && Logic.PropositionalLogic.NandFormula.val v ψ)

Complexity: 27 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.NandFormula, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Bool.and, Bool.not, Eq, Eq.mpr, Eq.symm, PProd, PUnit, congrArg, id

Used by: Logic.PropositionalLogic.NandFormula.exists_nand_of_boolFun, Logic.PropositionalLogic.NandFormula.ofFormula_val, Logic.PropositionalLogic.NandFormula.toFormula_val

Translate a Sheffer-stroke-only formula into an ordinary formula, using PropositionalLogic.Formula.nand.

def Logic.PropositionalLogic.NandFormula.toFormula {α : Type} :
  Logic.PropositionalLogic.NandFormula α → Logic.PropositionalLogic.Formula α
Show details 
| (Logic.PropositionalLogic.NandFormula.atom a).toFormula = Logic.PropositionalLogic.Formula.atom a
| (φ.nand ψ).toFormula = φ.toFormula.nand ψ.toFormula

Complexity: 23 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.NandFormula

Inner dependencies: Logic.PropositionalLogic.Formula.nand

Lean core dependencies: Eq, Eq.mpr, Eq.symm, PProd, PUnit, congrArg, id

Used by: Logic.PropositionalLogic.NandFormula.toFormula_val

theorem Logic.PropositionalLogic.NandFormula.toFormula_val {α : Type}
  (v : Logic.PropositionalLogic.Valuation α) (φ : Logic.PropositionalLogic.NandFormula α) :
  Logic.PropositionalLogic.Formula.val v φ.toFormula = Logic.PropositionalLogic.NandFormula.val v φ
Show details 
fun {α} v φ =>
  Logic.PropositionalLogic.NandFormula.rec
    (fun a =>
      Eq.refl
        (Logic.PropositionalLogic.Formula.val v
          (Logic.PropositionalLogic.NandFormula.atom a).toFormula))
    (fun φ ψ ihφ ihψ =>
      of_eq_true
        (Eq.trans
          (congr
            (congrArg Eq
              (Eq.trans (Logic.PropositionalLogic.Formula.val.eq_2 v (φ.toFormula.and ψ.toFormula))
                (Eq.trans (congrArg not (congr (congrArg and ihφ) ihψ))
                  (Bool.not_and (Logic.PropositionalLogic.NandFormula.val v φ)
                    (Logic.PropositionalLogic.NandFormula.val v ψ)))))
            (Bool.not_and (Logic.PropositionalLogic.NandFormula.val v φ)
              (Logic.PropositionalLogic.NandFormula.val v ψ)))
          (eq_self
            (!Logic.PropositionalLogic.NandFormula.val v φ ||
              !Logic.PropositionalLogic.NandFormula.val v ψ))))
    φ

Complexity: 753 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.NandFormula, Logic.PropositionalLogic.NandFormula.toFormula, Logic.PropositionalLogic.NandFormula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Bool.and, Bool.not, Bool.not_and, Bool.or, Eq, Eq.trans, True, congr, congrArg, eq_self, of_eq_true

Used by: (none)

Every formula’s truth table is already expressible using only the Sheffer stroke.

def Logic.PropositionalLogic.NandFormula.ofFormula {α : Type} :
  Logic.PropositionalLogic.Formula α → Logic.PropositionalLogic.NandFormula α
Show details 
| Logic.PropositionalLogic.NandFormula.ofFormula (Logic.PropositionalLogic.Formula.atom a) =
  Logic.PropositionalLogic.NandFormula.atom a
| Logic.PropositionalLogic.NandFormula.ofFormula φ.neg =
  (Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
    (Logic.PropositionalLogic.NandFormula.ofFormula φ)
| Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ) =
  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
        (Logic.PropositionalLogic.NandFormula.ofFormula ψ)).nand
    ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
      (Logic.PropositionalLogic.NandFormula.ofFormula ψ))
| Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ) =
  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
        (Logic.PropositionalLogic.NandFormula.ofFormula φ)).nand
    ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
      (Logic.PropositionalLogic.NandFormula.ofFormula ψ))
| Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ) =
  (Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
    ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
      (Logic.PropositionalLogic.NandFormula.ofFormula ψ))

Complexity: 23 (size of the value term)

Outer dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.NandFormula

Lean core dependencies: Eq, Eq.mpr, Eq.symm, PProd, PUnit, congrArg, id

Used by: Logic.PropositionalLogic.NandFormula.exists_nand_of_boolFun, Logic.PropositionalLogic.NandFormula.ofFormula_val

theorem Logic.PropositionalLogic.NandFormula.ofFormula_val {α : Type}
  (v : Logic.PropositionalLogic.Valuation α) (φ : Logic.PropositionalLogic.Formula α) :
  Logic.PropositionalLogic.NandFormula.val v (Logic.PropositionalLogic.NandFormula.ofFormula φ) =
    Logic.PropositionalLogic.Formula.val v φ
Show details 
fun {α} v φ =>
  Logic.PropositionalLogic.Formula.rec
    (fun a =>
      Eq.refl
        (Logic.PropositionalLogic.NandFormula.val v
          (Logic.PropositionalLogic.NandFormula.ofFormula
            (Logic.PropositionalLogic.Formula.atom a))))
    (fun φ ih =>
      of_eq_true
        (Eq.trans
          (congrFun'
            (congrArg Eq
              (Eq.trans
                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                  (Logic.PropositionalLogic.NandFormula.ofFormula φ)
                  (Logic.PropositionalLogic.NandFormula.ofFormula φ))
                (congrArg not
                  (Eq.trans (congr (congrArg and ih) ih)
                    (Bool.and_self (Logic.PropositionalLogic.Formula.val v φ))))))
            !Logic.PropositionalLogic.Formula.val v φ)
          (eq_self !Logic.PropositionalLogic.Formula.val v φ)))
    (fun φ ψ ihφ ihψ =>
      Bool.casesOn (motive := fun t =>
        Logic.PropositionalLogic.Formula.val v φ = t →
          Logic.PropositionalLogic.NandFormula.val v
              (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
            Logic.PropositionalLogic.Formula.val v (φ.and ψ))
        (Logic.PropositionalLogic.Formula.val v φ)
        (fun h =>
          Eq.ndrec (motive := fun x =>
            Logic.PropositionalLogic.Formula.val v φ = x →
              Logic.PropositionalLogic.NandFormula.val v
                  (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
                Logic.PropositionalLogic.Formula.val v (φ.and ψ))
            (fun hφ =>
              Bool.casesOn (motive := fun t =>
                Logic.PropositionalLogic.Formula.val v ψ = t →
                  Logic.PropositionalLogic.NandFormula.val v
                      (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
                    Logic.PropositionalLogic.Formula.val v (φ.and ψ))
                (Logic.PropositionalLogic.Formula.val v ψ)
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.and ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ))
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr
                                        (congrArg and
                                          (Eq.trans
                                            (congrArg not
                                              (Eq.trans
                                                (congr (congrArg and (Eq.trans ihφ hφ))
                                                  (Eq.trans ihψ hψ))
                                                (Bool.and_self false)))
                                            Bool.not_false))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihφ hφ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self false)))
                                          Bool.not_false))
                                      (Bool.and_self true)))
                                  Bool.not_true)))
                            (Eq.trans (congr (congrArg and hφ) hψ) (Bool.and_self false)))
                          (eq_self false)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.and ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ))
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr
                                        (congrArg and
                                          (Eq.trans
                                            (congrArg not
                                              (Eq.trans
                                                (congr (congrArg and (Eq.trans ihφ hφ))
                                                  (Eq.trans ihψ hψ))
                                                (Bool.and_true false)))
                                            Bool.not_false))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihφ hφ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_true false)))
                                          Bool.not_false))
                                      (Bool.and_self true)))
                                  Bool.not_true)))
                            (Eq.trans (congr (congrArg and hφ) hψ) (Bool.and_true false)))
                          (eq_self false)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
            (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
        (fun h =>
          Eq.ndrec (motive := fun x =>
            Logic.PropositionalLogic.Formula.val v φ = x →
              Logic.PropositionalLogic.NandFormula.val v
                  (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
                Logic.PropositionalLogic.Formula.val v (φ.and ψ))
            (fun hφ =>
              Bool.casesOn (motive := fun t =>
                Logic.PropositionalLogic.Formula.val v ψ = t →
                  Logic.PropositionalLogic.NandFormula.val v
                      (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
                    Logic.PropositionalLogic.Formula.val v (φ.and ψ))
                (Logic.PropositionalLogic.Formula.val v ψ)
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.and ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ))
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr
                                        (congrArg and
                                          (Eq.trans
                                            (congrArg not
                                              (Eq.trans
                                                (congr (congrArg and (Eq.trans ihφ hφ))
                                                  (Eq.trans ihψ hψ))
                                                (Bool.and_false true)))
                                            Bool.not_false))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihφ hφ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_false true)))
                                          Bool.not_false))
                                      (Bool.and_self true)))
                                  Bool.not_true)))
                            (Eq.trans (congr (congrArg and hφ) hψ) (Bool.and_false true)))
                          (eq_self false)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.and ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.and ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ))
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr
                                        (congrArg and
                                          (Eq.trans
                                            (congrArg not
                                              (Eq.trans
                                                (congr (congrArg and (Eq.trans ihφ hφ))
                                                  (Eq.trans ihψ hψ))
                                                (Bool.and_self true)))
                                            Bool.not_true))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihφ hφ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self true)))
                                          Bool.not_true))
                                      (Bool.and_self false)))
                                  Bool.not_false)))
                            (Eq.trans (congr (congrArg and hφ) hψ) (Bool.and_self true)))
                          (eq_self true)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
            (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
        (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
    (fun φ ψ ihφ ihψ =>
      Bool.casesOn (motive := fun t =>
        Logic.PropositionalLogic.Formula.val v φ = t →
          Logic.PropositionalLogic.NandFormula.val v
              (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
            Logic.PropositionalLogic.Formula.val v (φ.or ψ))
        (Logic.PropositionalLogic.Formula.val v φ)
        (fun h =>
          Eq.ndrec (motive := fun x =>
            Logic.PropositionalLogic.Formula.val v φ = x →
              Logic.PropositionalLogic.NandFormula.val v
                  (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
                Logic.PropositionalLogic.Formula.val v (φ.or ψ))
            (fun hφ =>
              Bool.casesOn (motive := fun t =>
                Logic.PropositionalLogic.Formula.val v ψ = t →
                  Logic.PropositionalLogic.NandFormula.val v
                      (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
                    Logic.PropositionalLogic.Formula.val v (φ.or ψ))
                (Logic.PropositionalLogic.Formula.val v ψ)
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.or ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula φ))
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr
                                        (congrArg and
                                          (Eq.trans
                                            (congrArg not
                                              (Eq.trans
                                                (congr (congrArg and (Eq.trans ihφ hφ))
                                                  (Eq.trans ihφ hφ))
                                                (Bool.and_self false)))
                                            Bool.not_false))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihψ hψ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self false)))
                                          Bool.not_false))
                                      (Bool.and_self true)))
                                  Bool.not_true)))
                            (Eq.trans (congr (congrArg or hφ) hψ) (Bool.or_self false)))
                          (eq_self false)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.or ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula φ))
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr
                                        (congrArg and
                                          (Eq.trans
                                            (congrArg not
                                              (Eq.trans
                                                (congr (congrArg and (Eq.trans ihφ hφ))
                                                  (Eq.trans ihφ hφ))
                                                (Bool.and_self false)))
                                            Bool.not_false))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihψ hψ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self true)))
                                          Bool.not_true))
                                      (Bool.and_false true)))
                                  Bool.not_false)))
                            (Eq.trans (congr (congrArg or hφ) hψ) (Bool.or_true false)))
                          (eq_self true)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
            (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
        (fun h =>
          Eq.ndrec (motive := fun x =>
            Logic.PropositionalLogic.Formula.val v φ = x →
              Logic.PropositionalLogic.NandFormula.val v
                  (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
                Logic.PropositionalLogic.Formula.val v (φ.or ψ))
            (fun hφ =>
              Bool.casesOn (motive := fun t =>
                Logic.PropositionalLogic.Formula.val v ψ = t →
                  Logic.PropositionalLogic.NandFormula.val v
                      (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
                    Logic.PropositionalLogic.Formula.val v (φ.or ψ))
                (Logic.PropositionalLogic.Formula.val v ψ)
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.or ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula φ))
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr
                                        (congrArg and
                                          (Eq.trans
                                            (congrArg not
                                              (Eq.trans
                                                (congr (congrArg and (Eq.trans ihφ hφ))
                                                  (Eq.trans ihφ hφ))
                                                (Bool.and_self true)))
                                            Bool.not_true))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihψ hψ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self false)))
                                          Bool.not_false))
                                      (Bool.and_true false)))
                                  Bool.not_false)))
                            (Eq.trans (congr (congrArg or hφ) hψ) (Bool.or_false true)))
                          (eq_self true)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.or ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.or ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula φ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula φ))
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr
                                        (congrArg and
                                          (Eq.trans
                                            (congrArg not
                                              (Eq.trans
                                                (congr (congrArg and (Eq.trans ihφ hφ))
                                                  (Eq.trans ihφ hφ))
                                                (Bool.and_self true)))
                                            Bool.not_true))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihψ hψ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self true)))
                                          Bool.not_true))
                                      (Bool.and_self false)))
                                  Bool.not_false)))
                            (Eq.trans (congr (congrArg or hφ) hψ) (Bool.or_self true)))
                          (eq_self true)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
            (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
        (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
    (fun φ ψ ihφ ihψ =>
      Bool.casesOn (motive := fun t =>
        Logic.PropositionalLogic.Formula.val v φ = t →
          Logic.PropositionalLogic.NandFormula.val v
              (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
            Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
        (Logic.PropositionalLogic.Formula.val v φ)
        (fun h =>
          Eq.ndrec (motive := fun x =>
            Logic.PropositionalLogic.Formula.val v φ = x →
              Logic.PropositionalLogic.NandFormula.val v
                  (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
                Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
            (fun hφ =>
              Bool.casesOn (motive := fun t =>
                Logic.PropositionalLogic.Formula.val v ψ = t →
                  Logic.PropositionalLogic.NandFormula.val v
                      (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
                    Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
                (Logic.PropositionalLogic.Formula.val v ψ)
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  (Logic.PropositionalLogic.NandFormula.ofFormula φ)
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr (congrArg and (Eq.trans ihφ hφ))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihψ hψ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self false)))
                                          Bool.not_false))
                                      (Bool.and_true false)))
                                  Bool.not_false)))
                            (Eq.trans
                              (congr (congrArg or (Eq.trans (congrArg not hφ) Bool.not_false)) hψ)
                              (Bool.or_false true)))
                          (eq_self true)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  (Logic.PropositionalLogic.NandFormula.ofFormula φ)
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr (congrArg and (Eq.trans ihφ hφ))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihψ hψ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self true)))
                                          Bool.not_true))
                                      (Bool.and_self false)))
                                  Bool.not_false)))
                            (Eq.trans
                              (congr (congrArg or (Eq.trans (congrArg not hφ) Bool.not_false)) hψ)
                              (Bool.or_self true)))
                          (eq_self true)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
            (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
        (fun h =>
          Eq.ndrec (motive := fun x =>
            Logic.PropositionalLogic.Formula.val v φ = x →
              Logic.PropositionalLogic.NandFormula.val v
                  (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
                Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
            (fun hφ =>
              Bool.casesOn (motive := fun t =>
                Logic.PropositionalLogic.Formula.val v ψ = t →
                  Logic.PropositionalLogic.NandFormula.val v
                      (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
                    Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
                (Logic.PropositionalLogic.Formula.val v ψ)
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  (Logic.PropositionalLogic.NandFormula.ofFormula φ)
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr (congrArg and (Eq.trans ihφ hφ))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihψ hψ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self false)))
                                          Bool.not_false))
                                      (Bool.and_self true)))
                                  Bool.not_true)))
                            (Eq.trans
                              (congr (congrArg or (Eq.trans (congrArg not hφ) Bool.not_true)) hψ)
                              (Bool.or_self false)))
                          (eq_self false)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (fun h =>
                  Eq.ndrec (motive := fun x =>
                    Logic.PropositionalLogic.Formula.val v ψ = x →
                      Logic.PropositionalLogic.NandFormula.val v
                          (Logic.PropositionalLogic.NandFormula.ofFormula (φ.imp ψ)) =
                        Logic.PropositionalLogic.Formula.val v (φ.imp ψ))
                    (fun hψ =>
                      of_eq_true
                        (Eq.trans
                          (congr
                            (congrArg Eq
                              (Eq.trans
                                (Logic.PropositionalLogic.NandFormula.val.eq_2 v
                                  (Logic.PropositionalLogic.NandFormula.ofFormula φ)
                                  ((Logic.PropositionalLogic.NandFormula.ofFormula ψ).nand
                                    (Logic.PropositionalLogic.NandFormula.ofFormula ψ)))
                                (Eq.trans
                                  (congrArg not
                                    (Eq.trans
                                      (congr (congrArg and (Eq.trans ihφ hφ))
                                        (Eq.trans
                                          (congrArg not
                                            (Eq.trans
                                              (congr (congrArg and (Eq.trans ihψ hψ))
                                                (Eq.trans ihψ hψ))
                                              (Bool.and_self true)))
                                          Bool.not_true))
                                      (Bool.and_false true)))
                                  Bool.not_false)))
                            (Eq.trans
                              (congr (congrArg or (Eq.trans (congrArg not hφ) Bool.not_true)) hψ)
                              (Bool.or_true false)))
                          (eq_self true)))
                    (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
                (Eq.refl (Logic.PropositionalLogic.Formula.val v ψ)))
            (Eq.symm h) (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
        (Eq.refl (Logic.PropositionalLogic.Formula.val v φ)))
    φ

Complexity: 16391 (size of the value term)

Dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.NandFormula.ofFormula, Logic.PropositionalLogic.NandFormula.val, Logic.PropositionalLogic.Valuation

Lean core dependencies: Bool, Bool.and, Bool.and_false, Bool.and_self, Bool.and_true, Bool.not, Bool.not_false, Bool.not_true, Bool.or, Bool.or_false, Bool.or_self, Bool.or_true, Eq, Eq.symm, Eq.trans, True, congr, congrArg, congrFun', eq_self, of_eq_true

Used by: Logic.PropositionalLogic.NandFormula.exists_nand_of_boolFun

Sheffer’s theorem. Every Boolean function of \(n + 1\) arguments is the truth table of some formula using only the Sheffer stroke.

theorem Logic.PropositionalLogic.NandFormula.exists_nand_of_boolFun {n : ℕ}
  (f : Logic.PropositionalLogic.BoolFun (n + 1)) :
  ∃ φ,
    ∀ (w : Logic.PropositionalLogic.Valuation (Fin (n + 1))),
      Logic.PropositionalLogic.NandFormula.val w φ = f w
Show details 
fun {n} f =>
  Exists.casesOn (Logic.PropositionalLogic.Formula.exists_andOrNot_of_boolFun f) fun φ hφ =>
    Exists.intro (Logic.PropositionalLogic.NandFormula.ofFormula φ) fun w =>
      Eq.trans (Logic.PropositionalLogic.NandFormula.ofFormula_val w φ) (hφ w)

Complexity: 879 (size of the value term)

Dependencies: Logic.PropositionalLogic.BoolFun, Logic.PropositionalLogic.NandFormula, Logic.PropositionalLogic.NandFormula.val, Logic.PropositionalLogic.Valuation

Proof dependencies: Logic.PropositionalLogic.Formula, Logic.PropositionalLogic.Formula.exists_andOrNot_of_boolFun, Logic.PropositionalLogic.Formula.val, Logic.PropositionalLogic.NandFormula.ofFormula, Logic.PropositionalLogic.NandFormula.ofFormula_val

Lean core dependencies: Bool, Eq, Eq.trans, Exists, Fin, Nat

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend