Completeness
Difficulty: hard — 1 definitions, 0 abbreviations, 3 lemmas, 2 theorems, 0 examples.
Completeness. Every tautology is provable in our Hilbert system, the converse of soundness (Propositional.Formula.soundness). The classical argument, due to Kalmár: first show that for any formula and any valuation, the literals matching that valuation prove the formula outright if it is true there, and prove its negation if it is false there (Propositional.Formula.kalmar below); then, given that this holds for every valuation of a tautology, eliminate the literals one at a time by case-splitting on each variable (Propositional.Formula.eliminate below), leaving the tautology itself provable from no hypotheses at all.
Propositional.Formula.starred
The formula \(\varphi\) itself if \(v\) makes it true, its negation otherwise.
Propositional.Formula.starred {n : ℕ} (v : Propositional.Valuation (Fin (n + 1))) (φ : Propositional.Formula (Fin (n + 1))) : Propositional.Formula (Fin (n + 1))
Show details
fun {n} v φ => if Propositional.Formula.val v φ = true then φ else φ.neg
Complexity: 205 (size of the value term)
Outer dependencies: Propositional.Formula, Propositional.Valuation
Inner dependencies: Propositional.Formula.val
Propositional.Formula.kalmar
Kalmár’s Lemma. Under a valuation, the literals for every atom together derive a formula if that valuation makes it true, and derive its negation otherwise.
Propositional.Formula.kalmar {n : ℕ} (v : Propositional.Valuation (Fin (n + 1))) (φ : Propositional.Formula (Fin (n + 1))) : Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1))) (Propositional.Formula.starred v φ)
Show details
fun {n} v φ => Propositional.Formula.rec (fun a => id (id (Bool.casesOn (motive := fun x => v a = x → Propositional.Formula.Derivable (List.map (fun i => if v i = true then Propositional.Formula.atom i else (Propositional.Formula.atom i).neg) (List.finRange (n + 1))) (if Propositional.Formula.val v (Propositional.Formula.atom a) = true then Propositional.Formula.atom a else (Propositional.Formula.atom a).neg)) (v a) (fun hv => Propositional.Formula.Derivable.assumption (List.mem_map.mpr (Exists.intro a ⟨List.mem_finRange a, of_eq_true (Eq.trans (congr (congrArg Eq (ite_cond_eq_false (Propositional.Formula.atom a) (Propositional.Formula.atom a).neg (Eq.trans (congrFun' (congrArg Eq hv) true) Bool.false_eq_true))) (ite_cond_eq_false (Propositional.Formula.atom a) (Propositional.Formula.atom a).neg (Eq.trans (congrFun' (congrArg Eq hv) true) Bool.false_eq_true))) (eq_self (Propositional.Formula.atom a).neg))⟩))) (fun hv => Propositional.Formula.Derivable.assumption (List.mem_map.mpr (Exists.intro a ⟨List.mem_finRange a, of_eq_true (Eq.trans (congr (congrArg Eq (ite_cond_eq_true (Propositional.Formula.atom a) (Propositional.Formula.atom a).neg (Eq.trans (congrFun' (congrArg Eq hv) true) (eq_self true)))) (ite_cond_eq_true (Propositional.Formula.atom a) (Propositional.Formula.atom a).neg (Eq.trans (congrFun' (congrArg Eq hv) true) (eq_self true)))) (eq_self (Propositional.Formula.atom a)))⟩))) (Eq.refl (v a))))) (fun φ ihφ => id (if hφ : Propositional.Formula.val v φ = true then Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Eq.trans (congrArg not hφ) Bool.not_true)) true) (fun a => Eq.refl φ.neg) fun a => Eq.refl φ.neg.neg))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_dni φ)) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true)) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg) (if_true φ φ.neg))) ihφ)) else Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congrArg not (Bool.of_not_eq_true hφ)) Bool.not_false)) true) (eq_self true)) (fun a => Eq.refl φ.neg) fun a => Eq.refl φ.neg.neg) (if_true φ.neg φ.neg.neg)))) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)) ihφ))) (fun φ ψ ihφ ihψ => id (if hφ : Propositional.Formula.val v φ = true then if hψ : Propositional.Formula.val v ψ = true then Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg and hφ) hψ) (Bool.true_and true))) true) (eq_self true)) (fun a => Eq.refl (φ.and ψ)) fun a => Eq.refl (φ.and ψ).neg) (if_true (φ.and ψ) (φ.and ψ).neg)))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.andIntro) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true)) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg) (if_true φ φ.neg))) ihφ)) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq hψ) true) (eq_self true)) (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg) (if_true ψ ψ.neg))) ihψ)) else Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Eq.trans (congr (congrArg and hφ) (Bool.of_not_eq_true hψ)) (Bool.and_false true))) true) (fun a => Eq.refl (φ.and ψ)) fun a => Eq.refl (φ.and ψ).neg))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_contrapose Propositional.Formula.Provable.andElim2)) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hψ)) true) (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg)) ihψ)) else if hψ : Propositional.Formula.val v ψ = true then Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Eq.trans (congr (congrArg and (Bool.of_not_eq_true hφ)) hψ) (Bool.false_and true))) true) (fun a => Eq.refl (φ.and ψ)) fun a => Eq.refl (φ.and ψ).neg))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_contrapose Propositional.Formula.Provable.andElim1)) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)) ihφ)) else Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Eq.trans (congr (congrArg and (Bool.of_not_eq_true hφ)) (Bool.of_not_eq_true hψ)) (Bool.false_and false))) true) (fun a => Eq.refl (φ.and ψ)) fun a => Eq.refl (φ.and ψ).neg))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_contrapose Propositional.Formula.Provable.andElim1)) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)) ihφ)))) (fun φ ψ ihφ ihψ => id (if hφ : Propositional.Formula.val v φ = true then if hψ : Propositional.Formula.val v ψ = true then Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or hφ) hψ) (Bool.true_or true))) true) (eq_self true)) (fun a => Eq.refl (φ.or ψ)) fun a => Eq.refl (φ.or ψ).neg) (if_true (φ.or ψ) (φ.or ψ).neg)))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.orIntro1) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true)) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg) (if_true φ φ.neg))) ihφ)) else Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or hφ) (Bool.of_not_eq_true hψ)) (Bool.true_or false))) true) (eq_self true)) (fun a => Eq.refl (φ.or ψ)) fun a => Eq.refl (φ.or ψ).neg) (if_true (φ.or ψ) (φ.or ψ).neg)))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.orIntro1) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true)) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg) (if_true φ φ.neg))) ihφ)) else if hψ : Propositional.Formula.val v ψ = true then Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or (Bool.of_not_eq_true hφ)) hψ) (Bool.or_true false))) true) (eq_self true)) (fun a => Eq.refl (φ.or ψ)) fun a => Eq.refl (φ.or ψ).neg) (if_true (φ.or ψ) (φ.or ψ).neg)))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.orIntro2) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq hψ) true) (eq_self true)) (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg) (if_true ψ ψ.neg))) ihψ)) else Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or (Bool.of_not_eq_true hφ)) (Bool.of_not_eq_true hψ)) (Bool.or_false false))) true) (fun a => Eq.refl (φ.or ψ)) fun a => Eq.refl (φ.or ψ).neg))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_deMorgan_or φ ψ)) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)) ihφ)) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hψ)) true) (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg)) ihψ)))) (fun φ ψ ihφ ihψ => id (if hφ : Propositional.Formula.val v φ = true then if hψ : Propositional.Formula.val v ψ = true then Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or (Eq.trans (congrArg not hφ) Bool.not_true)) hψ) (Bool.false_or true))) true) (eq_self true)) (fun a => Eq.refl (φ.imp ψ)) fun a => Eq.refl (φ.imp ψ).neg) (if_true (φ.imp ψ) (φ.imp ψ).neg)))) (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.k) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq hψ) true) (eq_self true)) (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg) (if_true ψ ψ.neg))) ihψ)) else Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or (Eq.trans (congrArg not hφ) Bool.not_true)) (Bool.of_not_eq_true hψ)) (Bool.false_or false))) true) (fun a => Eq.refl (φ.imp ψ)) fun a => Eq.refl (φ.imp ψ).neg))) (have h1 := Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.assumption (of_eq_true (Eq.trans List.mem_cons._simp_1 (Eq.trans (congr (congrArg Or (eq_self (φ.imp ψ))) (Eq.trans List.mem_map._simp_1 (congrArg Exists (funext fun a => Eq.trans (congrFun' (congrArg And (List.mem_finRange._simp_1 a)) (Propositional.Formula.literal v a = φ.imp ψ)) (true_and (Propositional.Formula.literal v a = φ.imp ψ)))))) (true_or (∃ a, Propositional.Formula.literal v a = φ.imp ψ)))))) (Propositional.Formula.Derivable.weaken (List.subset_cons_self (φ.imp ψ) (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq hφ) true) (eq_self true)) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg) (if_true φ φ.neg))) ihφ)); have h1d := Propositional.Formula.Derivable.deduction h1; have h2d := Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.k) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hψ)) true) (fun a => Eq.refl ψ) fun a => Eq.refl ψ.neg)) ihψ); Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax Propositional.Formula.Provable.negIntro) h1d) h2d) else if hψ : Propositional.Formula.val v ψ = true then Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or (Eq.trans (congrArg not (Bool.of_not_eq_true hφ)) Bool.not_false)) hψ) (Bool.true_or true))) true) (eq_self true)) (fun a => Eq.refl (φ.imp ψ)) fun a => Eq.refl (φ.imp ψ).neg) (if_true (φ.imp ψ) (φ.imp ψ).neg)))) (have h := Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_explosion φ ψ)) (Propositional.Formula.Derivable.assumption (of_eq_true (Eq.trans List.mem_cons._simp_1 (Eq.trans (congr (congrArg Or (eq_self φ)) (Eq.trans List.mem_map._simp_1 (congrArg Exists (funext fun a => Eq.trans (congrFun' (congrArg And (List.mem_finRange._simp_1 a)) (Propositional.Formula.literal v a = φ)) (true_and (Propositional.Formula.literal v a = φ)))))) (true_or (∃ a, Propositional.Formula.literal v a = φ))))))) (Propositional.Formula.Derivable.weaken (List.subset_cons_self φ (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)) ihφ)); Propositional.Formula.Derivable.deduction h) else Eq.mpr (id (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.trans (ite_congr (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or (Eq.trans (congrArg not (Bool.of_not_eq_true hφ)) Bool.not_false)) (Bool.of_not_eq_true hψ)) (Bool.true_or false))) true) (eq_self true)) (fun a => Eq.refl (φ.imp ψ)) fun a => Eq.refl (φ.imp ψ).neg) (if_true (φ.imp ψ) (φ.imp ψ).neg)))) (have h := Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.mp (Propositional.Formula.Derivable.ax (Propositional.Formula.provable_explosion φ ψ)) (Propositional.Formula.Derivable.assumption (of_eq_true (Eq.trans List.mem_cons._simp_1 (Eq.trans (congr (congrArg Or (eq_self φ)) (Eq.trans List.mem_map._simp_1 (congrArg Exists (funext fun a => Eq.trans (congrFun' (congrArg And (List.mem_finRange._simp_1 a)) (Propositional.Formula.literal v a = φ)) (true_and (Propositional.Formula.literal v a = φ)))))) (true_or (∃ a, Propositional.Formula.literal v a = φ))))))) (Propositional.Formula.Derivable.weaken (List.subset_cons_self φ (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (Eq.mp (congrArg (Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1)))) (ite_congr (congrFun' (congrArg Eq (Bool.of_not_eq_true hφ)) true) (fun a => Eq.refl φ) fun a => Eq.refl φ.neg)) ihφ)); Propositional.Formula.Derivable.deduction h))) φ
Complexity: 112678 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.Derivable, Propositional.Formula.literal, Propositional.Formula.starred, Propositional.Valuation
Proof dependencies: Propositional.Formula.Derivable.deduction, Propositional.Formula.Derivable.weaken, Propositional.Formula.provable_contrapose, Propositional.Formula.provable_deMorgan_or, Propositional.Formula.provable_dni, Propositional.Formula.provable_explosion, Propositional.Formula.val
Lean core dependencies: And, Bool, Bool.and, Bool.and_false, Bool.false_and, Bool.false_eq_true, Bool.false_or, Bool.not, Bool.not_false, Bool.not_true, Bool.of_not_eq_true, Bool.or, Bool.or_false, Bool.or_true, Bool.true_and, Bool.true_or, Eq, Eq.mp, Eq.mpr, Eq.trans, Exists, False, Fin, List, List.finRange, List.map, List.mem_finRange, List.mem_map, List.subset_cons_self, Nat, Not, Or, True, congr, congrArg, congrFun', dite, eq_self, funext, id, if_true, ite, ite_cond_eq_false, ite_cond_eq_true, ite_congr, of_eq_true, true_and, true_or
Used by: Propositional.Formula.completeness
Propositional.Formula.eliminate
Variable elimination. If some formula is derivable from the literals of every valuation restricted to a list of atoms, then it is provable outright, no hypotheses needed — by peeling one atom off the list at a time, case-splitting between the two valuations that agree except at that atom.
Propositional.Formula.eliminate {n : ℕ} {χ : Propositional.Formula (Fin (n + 1))} (L : List (Fin (n + 1))) : L.Nodup → (∀ (v : Propositional.Valuation (Fin (n + 1))), Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) L) χ) → Propositional.Formula.Derivable [] χ
Show details
fun {n} {χ} x x_1 x_2 => List.brecOn (motive := fun x => x.Nodup → (∀ (v : Propositional.Valuation (Fin (n + 1))), Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) x) χ) → Propositional.Formula.Derivable [] χ) x Propositional.Formula.eliminate._f x_1 x_2
Complexity: 521 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.Derivable, Propositional.Formula.literal, Propositional.Valuation
Proof dependencies: Propositional.Formula.Derivable.case_split, Propositional.Formula.Derivable.deduction
Mathlib dependencies: Function.update, Function.update_congr, Function.update_of_ne, Function.update_self
Lean core dependencies: And, Bool, Bool.false_eq_true, Bool.not, Bool.not_false, Bool.not_true, Eq, Eq.mp, Eq.trans, False, Fin, List, List.Nodup, List.map, List.map_congr_left, List.nodup_cons, Nat, Ne, Not, True, congrArg, congrFun', eq_self, ite, ite_cond_eq_false, ite_cond_eq_true, ite_congr, of_eq_true
Used by: Propositional.Formula.completeness
Propositional.Formula.completeness
Completeness. Every tautology is provable — the converse of Propositional.Formula.soundness.
Propositional.Formula.completeness {n : ℕ} {φ : Propositional.Formula (Fin (n + 1))} (h : φ.Tautology) : φ.Provable
Show details
fun {n} {φ} h => Propositional.Formula.Derivable.provable_of_nil (Propositional.Formula.eliminate (List.finRange (n + 1)) (List.nodup_finRange (n + 1)) fun v => have this := Propositional.Formula.kalmar v φ; Eq.mp (congrArg (fun _a => Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1))) _a) (if_pos rfl)) (Eq.mp (congrArg (fun _a => Propositional.Formula.Derivable (List.map (Propositional.Formula.literal v) (List.finRange (n + 1))) (if _a = true then φ else φ.neg)) (h v)) this))
Complexity: 1744 (size of the value term)
Dependencies: Propositional.Formula, Propositional.Formula.Provable, Propositional.Formula.Tautology
Proof dependencies: Propositional.Formula.Derivable, Propositional.Formula.Derivable.provable_of_nil, Propositional.Formula.eliminate, Propositional.Formula.kalmar, Propositional.Formula.literal, Propositional.Formula.starred, Propositional.Formula.val, Propositional.Valuation
Propositional.Formula.provable_imp_iff_semanticDerive
Provability relates to the semantic Basis III instance — the interesting direction. It proves an implication exactly when the corresponding pair of formulas stand in Propositional.semanticBasis3’s demonstrability relation: soundness and completeness together turn the semantic fact Propositional.Formula.SemanticEntails into a purely proof-theoretic one, expressed through Basis III’s own Popper.Basis1.Derive. Compare Propositional.Formula.provable_imp_iff_syntacticDerive below, where the same kind of statement for the syntactic instance holds for free, by definition.
Propositional.Formula.provable_imp_iff_semanticDerive {n : ℕ} {φ ψ : Propositional.Formula (Fin (n + 1))} : (φ.imp ψ).Provable ↔ (Propositional.semanticBasis3 (Fin (n + 1))).toBasis1.Derive [φ] [ψ]
Show details
fun {n} {φ ψ} => Eq.mpr (id (congrArg (fun _a => (φ.imp ψ).Provable ↔ _a) (propext (Popper.Basis1.derive_singleton (Propositional.semanticBasis3 (Fin (n + 1))).toBasis1)))) (id (Eq.mpr (id (congrArg (fun _a => (φ.imp ψ).Provable ↔ _a) (Eq.symm (propext (Popper.Basis3.deduce_iff_ndeduce_singleton (Propositional.semanticBasis3 (Fin (n + 1))) ψ φ))))) { mp := fun h v hv => have this := Propositional.Formula.soundness h v; Eq.mp (congrFun' (congrArg Eq (Eq.trans (congrFun' (congrArg or (Eq.trans (congrArg not hv) Bool.not_true)) (Propositional.Formula.val v ψ)) (Bool.false_or (Propositional.Formula.val v ψ)))) true) this, mpr := fun h => Propositional.Formula.completeness fun v => if hv : Propositional.Formula.val v φ = true then of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congr (congrArg or (Eq.trans (congrArg not hv) Bool.not_true)) (h v hv)) (Bool.or_true false))) true) (eq_self true)) else of_eq_true (Eq.trans (congrFun' (congrArg Eq (Eq.trans (congrFun' (congrArg or (Eq.trans (congrArg not (Bool.of_not_eq_true hv)) Bool.not_false)) (Propositional.Formula.val v ψ)) (Bool.true_or (Propositional.Formula.val v ψ)))) true) (eq_self true)) }))
Complexity: 5742 (size of the value term)
Dependencies: Popper.Basis1.Derive, Popper.Basis3.toBasis1, Propositional.Formula, Propositional.Formula.Provable, Propositional.semanticBasis3
Proof dependencies: Popper.Basis1.derive_singleton, Popper.Basis3.NDeduce, Popper.Basis3.deduce_iff_ndeduce_singleton, Propositional.Formula.completeness, Propositional.Formula.soundness, Propositional.Formula.val, Propositional.Valuation
Lean core dependencies: Bool, Bool.false_or, Bool.not, Bool.not_false, Bool.not_true, Bool.of_not_eq_true, Bool.or, Bool.or_true, Bool.true_or, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Fin, Iff, Nat, Not, True, congr, congrArg, congrFun', dite, eq_self, id, of_eq_true
Used by: (none)
Propositional.Formula.provable_imp_iff_syntacticDerive
Provability relates to the syntactic Basis III instance — for free. Unlike Propositional.Formula.provable_imp_iff_semanticDerive above, this needs neither soundness nor completeness: Propositional.syntacticBasis3’s deducibility is provability of the implication, by definition, so the two sides of the demonstrability relation collapse to the same thing immediately.
Propositional.Formula.provable_imp_iff_syntacticDerive {n : ℕ} {φ ψ : Propositional.Formula (Fin (n + 1))} : (φ.imp ψ).Provable ↔ (Propositional.syntacticBasis3 (Fin (n + 1))).toBasis1.Derive [φ] [ψ]
Show details
fun {n} {φ ψ} => Eq.mpr (id (congrArg (fun _a => (φ.imp ψ).Provable ↔ _a) (propext (Popper.Basis1.derive_singleton (Propositional.syntacticBasis3 (Fin (n + 1))).toBasis1)))) (id (Eq.mpr (id (congrArg (fun _a => (φ.imp ψ).Provable ↔ _a) (Eq.symm (propext (Popper.Basis3.deduce_iff_ndeduce_singleton (Propositional.syntacticBasis3 (Fin (n + 1))) ψ φ))))) Iff.rfl))
Complexity: 2951 (size of the value term)
Dependencies: Popper.Basis1.Derive, Popper.Basis3.toBasis1, Propositional.Formula, Propositional.Formula.Provable, Propositional.syntacticBasis3
Proof dependencies: Popper.Basis1.derive_singleton, Popper.Basis3.NDeduce, Popper.Basis3.deduce_iff_ndeduce_singleton
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.