Sheffer
Difficulty: moderate — 5 definitions, 0 abbreviations, 1 lemmas, 2 theorems, 0 examples.
definition lemma theorem
legendThe 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 (Propositional.Formula.exists_andOrNot_of_boolFun), the Sheffer stroke alone is functionally complete too.
Note
Propositional.Formula.nand
The Sheffer stroke (“not both”): the single connective from which every other connective can be built.
def Propositional.Formula.nand {α : Type} (φ ψ : Propositional.Formula α) : Propositional.Formula α
Show details
| φ.nand ψ = (φ.and ψ).neg
Complexity: 21 (size of the value term)
Outer dependencies: Propositional.Formula
Used by: Propositional.NandFormula.toFormula
Note
Propositional.NandFormula
A formula built from atoms using only the Sheffer stroke.
inductive Propositional.NandFormula (α : Type) : Type
Show details
| Propositional.NandFormula.atom : {α : Type} → α → Propositional.NandFormula α | Propositional.NandFormula.nand : {α : Type} → Propositional.NandFormula α → Propositional.NandFormula α → Propositional.NandFormula α
Outer dependencies: (none)
Note
Propositional.NandFormula.val
The truth table of a Sheffer-stroke-only formula: the same rule as Propositional.Formula.nand at every step.
def Propositional.NandFormula.val {α : Type} (v : Propositional.Valuation α) : Propositional.NandFormula α → Bool
Show details
| Propositional.NandFormula.val v (Propositional.NandFormula.atom a) = v a | Propositional.NandFormula.val v (φ.nand ψ) = !(Propositional.NandFormula.val v φ && Propositional.NandFormula.val v ψ)
Complexity: 27 (size of the value term)
Outer dependencies: Propositional.NandFormula, Propositional.Valuation
Note
Propositional.NandFormula.toFormula
Translate a Sheffer-stroke-only formula into an ordinary formula, using Propositional.Formula.nand.
def Propositional.NandFormula.toFormula {α : Type} : Propositional.NandFormula α → Propositional.Formula α
Show details
| (Propositional.NandFormula.atom a).toFormula = Propositional.Formula.atom a | (φ.nand ψ).toFormula = φ.toFormula.nand ψ.toFormula
Complexity: 23 (size of the value term)
Outer dependencies: Propositional.Formula, Propositional.NandFormula
Inner dependencies: Propositional.Formula.nand
Important
Propositional.NandFormula.toFormula_val
theorem Propositional.NandFormula.toFormula_val {α : Type} (v : Propositional.Valuation α) (φ : Propositional.NandFormula α) : Propositional.Formula.val v φ.toFormula = Propositional.NandFormula.val v φ
Show details
fun {α} v φ => Propositional.NandFormula.rec (fun a => Eq.refl (Propositional.Formula.val v (Propositional.NandFormula.atom a).toFormula)) (fun φ ψ ihφ ihψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.Formula.val.eq_2 v (φ.toFormula.and ψ.toFormula)) (Eq.trans (congrArg not (congr (congrArg and ihφ) ihψ)) (Bool.not_and (Propositional.NandFormula.val v φ) (Propositional.NandFormula.val v ψ))))) (Bool.not_and (Propositional.NandFormula.val v φ) (Propositional.NandFormula.val v ψ))) (eq_self (!Propositional.NandFormula.val v φ || !Propositional.NandFormula.val v ψ)))) φ
Complexity: 753 (size of the value term)
Dependencies: Propositional.Formula.val, Propositional.NandFormula, Propositional.NandFormula.toFormula, Propositional.NandFormula.val, Propositional.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)
Note
Propositional.NandFormula.ofFormula
Every formula’s truth table is already expressible using only the Sheffer stroke.
def Propositional.NandFormula.ofFormula {α : Type} : Propositional.Formula α → Propositional.NandFormula α
Show details
| Propositional.NandFormula.ofFormula (Propositional.Formula.atom a) = Propositional.NandFormula.atom a | Propositional.NandFormula.ofFormula φ.neg = (Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula φ) | Propositional.NandFormula.ofFormula (φ.and ψ) = ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula ψ)).nand ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula ψ)) | Propositional.NandFormula.ofFormula (φ.or ψ) = ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula φ)).nand ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.NandFormula.ofFormula ψ)) | Propositional.NandFormula.ofFormula (φ.imp ψ) = (Propositional.NandFormula.ofFormula φ).nand ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.NandFormula.ofFormula ψ))
Complexity: 23 (size of the value term)
Outer dependencies: Propositional.Formula, Propositional.NandFormula
Tip
Propositional.NandFormula.ofFormula_val
theorem Propositional.NandFormula.ofFormula_val {α : Type} (v : Propositional.Valuation α) (φ : Propositional.Formula α) : Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula φ) = Propositional.Formula.val v φ
Show details
fun {α} v φ => Propositional.Formula.rec (fun a => Eq.refl (Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (Propositional.Formula.atom a)))) (fun φ ih => of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v (Propositional.NandFormula.ofFormula φ) (Propositional.NandFormula.ofFormula φ)) (congrArg not (Eq.trans (congr (congrArg and ih) ih) (Bool.and_self (Propositional.Formula.val v φ)))))) !Propositional.Formula.val v φ) (eq_self !Propositional.Formula.val v φ))) (fun φ ψ ihφ ihψ => Bool.casesOn (motive := fun t => Propositional.Formula.val v φ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (Propositional.Formula.val v φ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v φ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (fun hφ => Bool.casesOn (motive := fun t => Propositional.Formula.val v ψ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (Propositional.Formula.val v ψ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula ψ)) ((Propositional.NandFormula.ofFormula φ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula ψ)) ((Propositional.NandFormula.ofFormula φ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (Eq.refl (Propositional.Formula.val v ψ))) (Eq.symm h) (Eq.refl (Propositional.Formula.val v φ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v φ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (fun hφ => Bool.casesOn (motive := fun t => Propositional.Formula.val v ψ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (Propositional.Formula.val v ψ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula ψ)) ((Propositional.NandFormula.ofFormula φ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.and ψ)) = Propositional.Formula.val v (φ.and ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula ψ)) ((Propositional.NandFormula.ofFormula φ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (Eq.refl (Propositional.Formula.val v ψ))) (Eq.symm h) (Eq.refl (Propositional.Formula.val v φ))) (Eq.refl (Propositional.Formula.val v φ))) (fun φ ψ ihφ ihψ => Bool.casesOn (motive := fun t => Propositional.Formula.val v φ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (Propositional.Formula.val v φ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v φ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (fun hφ => Bool.casesOn (motive := fun t => Propositional.Formula.val v ψ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (Propositional.Formula.val v ψ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula φ)) ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula φ)) ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (Eq.refl (Propositional.Formula.val v ψ))) (Eq.symm h) (Eq.refl (Propositional.Formula.val v φ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v φ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (fun hφ => Bool.casesOn (motive := fun t => Propositional.Formula.val v ψ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (Propositional.Formula.val v ψ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula φ)) ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.or ψ)) = Propositional.Formula.val v (φ.or ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v ((Propositional.NandFormula.ofFormula φ).nand (Propositional.NandFormula.ofFormula φ)) ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (Eq.refl (Propositional.Formula.val v ψ))) (Eq.symm h) (Eq.refl (Propositional.Formula.val v φ))) (Eq.refl (Propositional.Formula.val v φ))) (fun φ ψ ihφ ihψ => Bool.casesOn (motive := fun t => Propositional.Formula.val v φ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (Propositional.Formula.val v φ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v φ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (fun hφ => Bool.casesOn (motive := fun t => Propositional.Formula.val v ψ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (Propositional.Formula.val v ψ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v (Propositional.NandFormula.ofFormula φ) ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v (Propositional.NandFormula.ofFormula φ) ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (Eq.refl (Propositional.Formula.val v ψ))) (Eq.symm h) (Eq.refl (Propositional.Formula.val v φ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v φ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (fun hφ => Bool.casesOn (motive := fun t => Propositional.Formula.val v ψ = t → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (Propositional.Formula.val v ψ) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v (Propositional.NandFormula.ofFormula φ) ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (fun h => Eq.ndrec (motive := fun x => Propositional.Formula.val v ψ = x → Propositional.NandFormula.val v (Propositional.NandFormula.ofFormula (φ.imp ψ)) = Propositional.Formula.val v (φ.imp ψ)) (fun hψ => of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (Propositional.NandFormula.val.eq_2 v (Propositional.NandFormula.ofFormula φ) ((Propositional.NandFormula.ofFormula ψ).nand (Propositional.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 (Propositional.Formula.val v ψ))) (Eq.refl (Propositional.Formula.val v ψ))) (Eq.symm h) (Eq.refl (Propositional.Formula.val v φ))) (Eq.refl (Propositional.Formula.val v φ))) φ
Complexity: 16391 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.val, Propositional.NandFormula.ofFormula, Propositional.NandFormula.val, Propositional.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
Important
Propositional.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 Propositional.NandFormula.exists_nand_of_boolFun {n : ℕ} (f : Propositional.BoolFun (n + 1)) : ∃ φ, ∀ (w : Propositional.Valuation (Fin (n + 1))), Propositional.NandFormula.val w φ = f w
Show details
fun {n} f => Exists.casesOn (Propositional.Formula.exists_andOrNot_of_boolFun f) fun φ hφ => Exists.intro (Propositional.NandFormula.ofFormula φ) fun w => Eq.trans (Propositional.NandFormula.ofFormula_val w φ) (hφ w)
Complexity: 879 (size of the value term)
Dependencies: Propositional.BoolFun, Propositional.NandFormula, Propositional.NandFormula.val, Propositional.Valuation
Proof dependencies: Propositional.Formula, Propositional.Formula.exists_andOrNot_of_boolFun, Propositional.Formula.val, Propositional.NandFormula.ofFormula, Propositional.NandFormula.ofFormula_val
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