FunctionalCompleteness
Difficulty: optional — 9 definitions, 1 abbreviations, 7 lemmas, 2 theorems, 0 examples.
definition abbreviation lemma theorem
legendA set of connectives is functionally complete when every truth table is the truth table of some formula built only from that set. Negation, conjunction, and disjunction together are functionally complete: the canonical disjunctive normal form witnesses this for any truth table. A row of the truth table where the function is true becomes a conjunction of literals (an atom, or its negation, matching that row); the function itself becomes the disjunction of those rows.
The Sheffer stroke alone is already functionally complete, since it can express each of the other three: 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\).
Note
Propositional.BoolFun
A Boolean function taking \(n\) Boolean arguments.
Propositional.BoolFun (n : ℕ) : Type
Show details
fun n => (Fin n → Bool) → Bool
Complexity: 9 (size of the value term)
Outer dependencies: (none)
Note
Propositional.Formula.bigAnd
The conjunction of a list of formulas: true exactly when every formula in the list is. Unfolds via the already-simp List.foldr equations, so it needs no separate step lemmas.
Propositional.Formula.bigAnd {n : ℕ} (l : List (Propositional.Formula (Fin (n + 1)))) : Propositional.Formula (Fin (n + 1))
Show details
fun {n} l => List.foldr Propositional.Formula.and Propositional.Formula.verum'✝ l
Complexity: 131 (size of the value term)
Outer dependencies: Propositional.Formula
Lean core dependencies: Fin, List, List.foldr, Nat
Tip
Propositional.Formula.bigAnd_val
Propositional.Formula.bigAnd_val {n : ℕ} (l : List (Propositional.Formula (Fin (n + 1)))) (w : Propositional.Valuation (Fin (n + 1))) : Propositional.Formula.val w (Propositional.Formula.bigAnd l) = true ↔ ∀ φ ∈ l, Propositional.Formula.val w φ = true
Show details
fun {n} l w => id (List.rec (of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Propositional.Formula.val_verum'✝ w)) true) (eq_self true))) (Eq.trans (forall_congr fun φ => Eq.trans (implies_congr List.not_mem_nil._simp_1 (Eq.refl (Propositional.Formula.val w φ = true))) IsEmpty.forall_iff._simp_1) (implies_true (Propositional.Formula (Fin (n + 1)))))) (iff_self True))) (fun φ l ih => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (Eq.trans (congrFun' (congrArg Eq (Propositional.Formula.val.eq_3 w φ (List.foldr Propositional.Formula.and Propositional.Formula.verum'✝ l))) true) (Bool.and_eq_true (Propositional.Formula.val w φ) (Propositional.Formula.val w (List.foldr Propositional.Formula.and Propositional.Formula.verum'✝ l)))) (congrArg (And (Propositional.Formula.val w φ = true)) (propext ih)))) (Eq.trans (forall_congr fun φ_1 => implies_congr List.mem_cons._simp_1 (Eq.refl (Propositional.Formula.val w φ_1 = true))) forall_eq_or_imp._simp_1)) (iff_self (Propositional.Formula.val w φ = true ∧ ∀ φ ∈ l, Propositional.Formula.val w φ = true)))) l)
Complexity: 11081 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.bigAnd, Propositional.Formula.val, Propositional.Valuation
Lean core dependencies: And, Bool, Bool.and, Bool.and_eq_true, Eq, Eq.trans, False, Fin, Iff, List, List.foldr, Nat, Or, True, congr, congrArg, congrFun', eq_self, forall_congr, id, iff_self, implies_congr, implies_true, of_eq_true
Used by: Propositional.Formula.minterm_val
Note
Propositional.Formula.bigOr
The disjunction of a list of formulas: true exactly when some formula in the list is.
Propositional.Formula.bigOr {n : ℕ} (l : List (Propositional.Formula (Fin (n + 1)))) : Propositional.Formula (Fin (n + 1))
Show details
fun {n} l => List.foldr Propositional.Formula.or Propositional.Formula.falsum'✝ l
Complexity: 131 (size of the value term)
Outer dependencies: Propositional.Formula
Lean core dependencies: Fin, List, List.foldr, Nat
Tip
Propositional.Formula.bigOr_val
Propositional.Formula.bigOr_val {n : ℕ} (l : List (Propositional.Formula (Fin (n + 1)))) (w : Propositional.Valuation (Fin (n + 1))) : Propositional.Formula.val w (Propositional.Formula.bigOr l) = true ↔ ∃ φ ∈ l, Propositional.Formula.val w φ = true
Show details
fun {n} l w => id (List.rec (of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Propositional.Formula.val_falsum'✝ w)) true) Bool.false_eq_true)) (Eq.trans (congrArg Exists (funext fun φ => Eq.trans (congrFun' (congrArg And List.not_mem_nil._simp_1) (Propositional.Formula.val w φ = true)) (false_and (Propositional.Formula.val w φ = true)))) exists_false._simp_1)) (iff_self False))) (fun φ l ih => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (Eq.trans (congrFun' (congrArg Eq (Propositional.Formula.val.eq_4 w φ (List.foldr Propositional.Formula.or Propositional.Formula.falsum'✝ l))) true) (Bool.or_eq_true (Propositional.Formula.val w φ) (Propositional.Formula.val w (List.foldr Propositional.Formula.or Propositional.Formula.falsum'✝ l)))) (congrArg (Or (Propositional.Formula.val w φ = true)) (propext ih)))) (Eq.trans (congrArg Exists (funext fun φ_1 => congrFun' (congrArg And List.mem_cons._simp_1) (Propositional.Formula.val w φ_1 = true))) exists_eq_or_imp._simp_1)) (iff_self (Propositional.Formula.val w φ = true ∨ ∃ φ ∈ l, Propositional.Formula.val w φ = true)))) l)
Complexity: 12983 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.bigOr, Propositional.Formula.val, Propositional.Valuation
Lean core dependencies: And, Bool, Bool.false_eq_true, Bool.or, Bool.or_eq_true, Eq, Eq.trans, Exists, False, Fin, Iff, List, List.foldr, Nat, Or, True, congr, congrArg, congrFun', false_and, funext, id, iff_self, of_eq_true
Used by: Propositional.Formula.dnf_val
Note
Propositional.Formula.literal
The literal for atom \(i\) under valuation \(v\): the atom itself if \(v\) makes it true, its negation otherwise.
Propositional.Formula.literal {n : ℕ} (v : Propositional.Valuation (Fin (n + 1))) (i : Fin (n + 1)) : Propositional.Formula (Fin (n + 1))
Show details
fun {n} v i => if v i = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg
Complexity: 203 (size of the value term)
Outer dependencies: Propositional.Formula, Propositional.Valuation
Tip
Propositional.Formula.literal_val
Propositional.Formula.literal_val {n : ℕ} (v w : Propositional.Valuation (Fin (n + 1))) (i : Fin (n + 1)) : Propositional.Formula.val w (Propositional.Formula.literal v i) = true ↔ w i = v i
Show details
fun {n} v w i => id (Bool.casesOn (motive := fun t => v i = t → (Propositional.Formula.val w (if v i = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ w i = v i)) (v i) (fun h => Eq.ndrec (motive := fun x => v i = x → (Propositional.Formula.val w (if x = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ w i = x)) (fun hv => Bool.casesOn (motive := fun t => w i = t → (Propositional.Formula.val w (if false = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ w i = false)) (w i) (fun h => Eq.ndrec (motive := fun x => w i = x → (Propositional.Formula.val w (if false = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ x = false)) (fun hw => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrArg (Propositional.Formula.val w) (ite_cond_eq_false (Propositional.Formula.atom i) (Propositional.Formula.atom i).neg Bool.false_eq_true)) (Propositional.Formula.val.eq_2 w (Propositional.Formula.atom i))) (Eq.trans (congrArg not hw) Bool.not_false))) true) (eq_self true))) (eq_self false)) (iff_self True))) (Eq.symm h) (Eq.refl (w i))) (fun h => Eq.ndrec (motive := fun x => w i = x → (Propositional.Formula.val w (if false = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ x = false)) (fun hw => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrArg (Propositional.Formula.val w) (ite_cond_eq_false (Propositional.Formula.atom i) (Propositional.Formula.atom i).neg Bool.false_eq_true)) (Propositional.Formula.val.eq_2 w (Propositional.Formula.atom i))) (Eq.trans (congrArg not hw) Bool.not_true))) true) Bool.false_eq_true)) Bool.true_eq_false) (iff_self False))) (Eq.symm h) (Eq.refl (w i))) (Eq.refl (w i))) (Eq.symm h) (Eq.refl (v i))) (fun h => Eq.ndrec (motive := fun x => v i = x → (Propositional.Formula.val w (if x = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ w i = x)) (fun hv => Bool.casesOn (motive := fun t => w i = t → (Propositional.Formula.val w (if true = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ w i = true)) (w i) (fun h => Eq.ndrec (motive := fun x => w i = x → (Propositional.Formula.val w (if true = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ x = true)) (fun hw => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrArg (Propositional.Formula.val w) (ite_cond_eq_true (Propositional.Formula.atom i) (Propositional.Formula.atom i).neg (eq_self true))) (Propositional.Formula.val.eq_1 w i)) hw)) true) Bool.false_eq_true)) Bool.false_eq_true) (iff_self False))) (Eq.symm h) (Eq.refl (w i))) (fun h => Eq.ndrec (motive := fun x => w i = x → (Propositional.Formula.val w (if true = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) = true ↔ x = true)) (fun hw => of_eq_true (Eq.trans (congr (congrArg Iff (Eq.trans (congrFun' (congrArg Eq (Eq.trans (Eq.trans (congrArg (Propositional.Formula.val w) (ite_cond_eq_true (Propositional.Formula.atom i) (Propositional.Formula.atom i).neg (eq_self true))) (Propositional.Formula.val.eq_1 w i)) hw)) true) (eq_self true))) (eq_self true)) (iff_self True))) (Eq.symm h) (Eq.refl (w i))) (Eq.refl (w i))) (Eq.symm h) (Eq.refl (v i))) (Eq.refl (v i)))
Complexity: 11857 (size of the value term)
Proof dependencies: Propositional.Formula
Lean core dependencies: Bool, Bool.false_eq_true, Bool.not, Bool.not_false, Bool.not_true, Bool.true_eq_false, Eq, Eq.symm, Eq.trans, False, Fin, Iff, Nat, True, congr, congrArg, congrFun', eq_self, id, iff_self, ite, ite_cond_eq_false, ite_cond_eq_true, of_eq_true
Used by: Propositional.Formula.minterm_val
Note
Propositional.Formula.minterm
The minterm for \(v\): the conjunction of every atom’s literal under \(v\), true exactly at \(v\) itself.
Propositional.Formula.minterm {n : ℕ} (v : Propositional.Valuation (Fin (n + 1))) : Propositional.Formula (Fin (n + 1))
Show details
fun {n} v => Propositional.Formula.bigAnd (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))
Complexity: 129 (size of the value term)
Outer dependencies: Propositional.Formula, Propositional.Valuation
Inner dependencies: Propositional.Formula.bigAnd, Propositional.Formula.literal
Lean core dependencies: Fin, List.finRange, List.map, Nat
Tip
Propositional.Formula.minterm_val
Propositional.Formula.minterm_val {n : ℕ} (v w : Propositional.Valuation (Fin (n + 1))) : Propositional.Formula.val w (Propositional.Formula.minterm v) = true ↔ w = v
Show details
fun {n} v w => Eq.mpr (id (congrFun' (congrArg Iff (Eq.trans (Propositional.Formula.minterm_val._simp_1_2 (List.map (Propositional.Formula.literal v) (List.finRange (n + 1))) w) Propositional.Formula.minterm_val._simp_1_3)) (w = v))) { mp := fun h => funext fun i => (Propositional.Formula.literal_val v w i).mp (h i (List.mem_finRange i)), mpr := fun heq i x => Eq.mpr (id (congrArg (fun _a => Propositional.Formula.val _a (Propositional.Formula.literal v i) = true) heq)) ((Propositional.Formula.literal_val v v i).mpr rfl) }
Complexity: 3281 (size of the value term)
Proof dependencies: Propositional.Formula, Propositional.Formula.bigAnd, Propositional.Formula.bigAnd_val, Propositional.Formula.literal, Propositional.Formula.literal_val
Lean core dependencies: Bool, Eq, Eq.mpr, Eq.trans, Fin, Iff, List, List.finRange, List.forall_mem_map, List.map, List.mem_finRange, Nat, congrArg, congrFun', funext, id, rfl
Used by: Propositional.Formula.dnf_val
Note
Propositional.Formula.dnf
Completeness of \(\{\lnot, \land, \lor\}\). The canonical disjunctive normal form for a Boolean function: the disjunction, over every row where the function is true, of that row’s minterm.
Propositional.Formula.dnf {n : ℕ} (f : Propositional.BoolFun (n + 1)) : Propositional.Formula (Fin (n + 1))
Show details
fun {n} f => Propositional.Formula.bigOr (List.map Propositional.Formula.minterm (List.filter f Finset.univ.toList))
Complexity: 343 (size of the value term)
Outer dependencies: Propositional.BoolFun, Propositional.Formula
Inner dependencies: Propositional.Formula.bigOr, Propositional.Formula.minterm, Propositional.Valuation
Mathlib dependencies: Finset.toList, Finset.univ
Lean core dependencies: Bool, Fin, List.filter, List.map, Nat
Tip
Propositional.Formula.dnf_val
Propositional.Formula.dnf_val {n : ℕ} (f : Propositional.BoolFun (n + 1)) (w : Propositional.Valuation (Fin (n + 1))) : Propositional.Formula.val w (Propositional.Formula.dnf f) = true ↔ f w = true
Show details
fun {n} f w => id (Eq.mpr (id (congrArg (fun _a => _a ↔ f w = true) (propext (Propositional.Formula.bigOr_val (List.map Propositional.Formula.minterm (List.filter f Finset.univ.toList)) w)))) { mp := fun a => Exists.casesOn a fun φ h => And.casesOn h fun hφmem hφval => Exists.casesOn (List.mem_map.mp hφmem) fun v h => And.casesOn h fun hvmem right => Eq.ndrec (motive := fun φ => φ ∈ List.map Propositional.Formula.minterm (List.filter f Finset.univ.toList) → Propositional.Formula.val w φ = true → f w = true) (fun hφmem hφval => And.casesOn (List.mem_filter.mp hvmem) fun left hv2 => Eq.mpr (id (congrArg (fun _a => f _a = true) ((Propositional.Formula.minterm_val v w).mp hφval))) hv2) right hφmem hφval, mpr := fun hf => Exists.intro (Propositional.Formula.minterm w) ⟨List.mem_map.mpr (Exists.intro w ⟨List.mem_filter.mpr ⟨Finset.mem_toList.mpr (Finset.mem_univ w), hf⟩, rfl⟩), (Propositional.Formula.minterm_val w w).mpr rfl⟩ })
Complexity: 20061 (size of the value term)
Dependencies: Propositional.BoolFun, Propositional.Formula.dnf, Propositional.Formula.val, Propositional.Valuation
Proof dependencies: Propositional.Formula, Propositional.Formula.bigOr, Propositional.Formula.bigOr_val, Propositional.Formula.minterm, Propositional.Formula.minterm_val
Mathlib dependencies: Finset, Finset.mem_toList, Finset.mem_univ, Finset.toList, Finset.univ
Tip
Propositional.Formula.exists_andOrNot_of_boolFun
Every Boolean function of \(n + 1\) arguments is the truth table of some formula using only negation, conjunction, and disjunction.
Propositional.Formula.exists_andOrNot_of_boolFun {n : ℕ} (f : Propositional.BoolFun (n + 1)) : ∃ φ, ∀ (w : Propositional.Valuation (Fin (n + 1))), Propositional.Formula.val w φ = f w
Show details
fun {n} f => Exists.intro (Propositional.Formula.dnf f) fun w => Bool.eq_iff_iff.mpr (Propositional.Formula.dnf_val f w)
Complexity: 355 (size of the value term)
Dependencies: Propositional.BoolFun, Propositional.Formula, Propositional.Formula.val, Propositional.Valuation
Proof dependencies: Propositional.Formula.dnf, Propositional.Formula.dnf_val
Note
Propositional.NandFormula
A formula built from atoms using only the Sheffer stroke.
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.
Propositional.NandFormula.val {α : Type} (v : Propositional.Valuation α) : Propositional.NandFormula α → Bool
Show details
fun {α} v x => Propositional.NandFormula.brecOn x (Propositional.NandFormula.val._f 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.
Propositional.NandFormula.toFormula {α : Type} : Propositional.NandFormula α → Propositional.Formula α
Show details
fun {α} x => Propositional.NandFormula.brecOn x Propositional.NandFormula.toFormula._f
Complexity: 23 (size of the value term)
Outer dependencies: Propositional.Formula, Propositional.NandFormula
Inner dependencies: Propositional.Formula.nand
Important
Propositional.NandFormula.toFormula_val
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.
Propositional.NandFormula.ofFormula {α : Type} : Propositional.Formula α → Propositional.NandFormula α
Show details
fun {α} x => Propositional.Formula.brecOn x Propositional.NandFormula.ofFormula._f
Complexity: 23 (size of the value term)
Outer dependencies: Propositional.Formula, Propositional.NandFormula
Tip
Propositional.NandFormula.ofFormula_val
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.
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.
definitionabbreviationlemmatheoremdeclared elsewheredependencyproof dependency
legend