Completeness of classical propositional logical is a mathematical theorem asserting that classical provability relation is the same as the relation of truth preservation given by $True, $False. Today there plenty of known methods to prove the theorem, we will be interested in the one proved by Kalmar in 1935, which is a lesser known proof, however with an interesting twist that the proof is in fact constructive, i.e. there is a construction that transforms between the two deductive relations mentioned above (for more details on constructive logic/mathematics see) . Lets see how we managed to verify it proof assistant Lean (joint work with Jáchym Šimon, my bachelor student)
First of all, Lean is implemented in C++, and as many proof assistants it is heavily based on mathematical foundations given by Type Theory, which seems to be the right fit to be used in this way, hence before you start i would recommend some read on the topic (see e.g. a short introductory text) and closely related proof system of Natural Deduction invented by Gentzen . To understand the relation between type theory and logic also recommend checking the Curry-Howard isomorphism.
Finally, lets talk about writing the verification. A good thing is that there is a lot of documentation and nice tutorials are written about Lean (to be found on the web page). We read those and than started formalizing right away. I must say I was rather shocked how intuitive it was to work with Lean. Of course, manage to write the code is one thing, learn to do it right is the other (too many times did we rewrite the thing completely, after discovering new tricks). In the after spending few months with the proof assistant (unfortunately barely scratching the surface of its capabilities) I got the impression that verified mathematics will play an important role in the future: The code in Lean is readable (e.g. LaTeX symbols and its shortcuts are implemented) and intuitive, would not be so bad writing papers using it.
Maybe some time in future I will share more Lean stories but for know you can download the resulting source code here.
import knihovny.data.list.basicimport knihovny.data.list.defsimport knihovny.data.boolimport knihovny.data.nat.basicimport init.meta.tactic
-- lean definice (mostly tactics for Hilbert style proofs) variables {α β γ : Type}
meta def tac1 : tactic unit := `[ repeat { assumption <|> {left, {repeat {assumption <|> {left, assumption} <|> right}} } <|> right } ]
--assump pro hledání mezi předpoklady meta def assump : tactic unit := `[ { repeat {{left, { repeat{{left, exact rfl} <|> right <|> exact rfl }} } <|> right <|> exact rfl}} <|> {tac1}]
-- hledá jesli je něco axiom, či přepoklad meta def proof : tactic unit := `[ { left, refine (exintro2 _ _ rfl)} <|> --pro 3 axiomy z definice in_proof {right,left, refine (exintro3 _ _ _ rfl) } <|> {right,right, left, refine (exintro2 _ _ rfl) } <|> {right,right, right, left, assump } --pro přepoklad z definice in_proof <|> -- to samé pro důkaz s řezem (in_proof_with_cut) {right, {{left, refine (exintro2 _ _ rfl)} <|> {right,left, refine (exintro3 _ _ _ rfl) } <|> {right,right, left, refine (exintro2 _ _ rfl) } <|> {right,right, right, left, assump } }} ]
--odvození s MP meta def MP: tactic unit := `[ --{repeat {right}, existsi _ , split; assump} <|> {repeat {right}, existsi _ , split, tactic.swap, assump, assump} ] --seznam dokázaných binárních pravidel meta def bin_rules_list: tactic unit := `[ {refine (@trans _ _ _), repeat {assump}} <|> { refine (@RAA _ _), repeat {assump} } <|> {assumption} ]
-- odvození pomocí dokázaných pravidel meta def rules: tactic unit := `[ --binary rules (verze 1) {left, left, existsi _, existsi _, split, tactic.swap, split, assump, bin_rules_list, assump}
<|> --binary rulas (verze 2) (pro binární pravidla je pro Lean těžké doplnit správně předpoklady) {left, left, existsi _, existsi _, split, tactic.swap, split, tactic.swap, bin_rules_list, repeat {assump}} <|> --unary rules {left,right, left, existsi _, split, tactic.swap,
{ {assumption} <|> {exact contraposition }<|> {exact contraposition2} <|> {exact double_neg<|> {exact double_neg_law}}} ,assump }
<|> -- theorems (žádný konkrétní teorém zatím není dokázaný) {left,right, right, assumption}
] --souhrnná taktika meta def collection: tactic unit := `[ {MP} <|> {rules} <|> {assump} <|> {proof}]
--finální taktika pro ověření Hilbertovského důkazu meta def HK_verifier : tactic unit := `[ repeat { split, collection }, assump]
lemma exintro2 {P: α → β → Prop} (A: α) (B:β) : P A B → ∃ A:α, ∃ B: β, P A B := λ h, exists.intro A (exists.intro B h) lemma exintro3 {P: α → β →γ → Prop} (A: α) (B:β) (C:γ): P A B C → ∃ A:α, ∃ B: β,∃ C:γ, P A B C := λ h, exists.intro A (exists.intro B (exists.intro C h)) -- to do: the same for exists.elim--konec
--Syntax
--základní pojmy
--množina formulí (induktivní typ)
inductive Form : Type | p : ℕ → Form | imp : Form → Form → Form | neg : Form → Form
local infixr ⇒:80 := Form.imp local prefix ~:100 := Form.neg open Form
--konec
--deklarace proměnných def eval:= ℕ → bool
variables {v e:eval} variables {A B C D:Form} variables {Γ Δ :set Form} variables {m n:ℕ} variables {a b:bool} variables {l li:list Form}
--konec
--Axiomy Hilbertovského kalkulu
def A1 (A B: Form) := A ⇒ ( B ⇒ A ) def A2 (A B C: Form) := ( A ⇒ (B ⇒ C) ) ⇒ (A ⇒ B) ⇒ A ⇒ C def A3 (A B: Form) := (~B ⇒ ~A) ⇒ (~B ⇒ A) ⇒ B
--konec --příklady na nerovnosti formulí theorem theor: (~A) ≠ (A ⇒ B):= by contradiction --case of different constructuors theorem constructor_p_injective: (p m)= (p n) → m = n:= assume e, Form.no_confusion e (λ e: m= n, e)
theorem constructor_imp_injective: (A ⇒ B) = (C ⇒ D) → A=C ∧ B=D:= assume h, Form.no_confusion h (λ h1 h2, ⟨h1,h2 ⟩) lemma s: 1≤ n → m + n ≠ m:= assume ineq eq, have h: n=0, from nat.add_left_cancel (@eq.subst ℕ (λ k, m+n=k) m (m+0) (nat.add_zero m).symm eq), nat.le_lt_antisymm ineq (nat.succ_le_succ (nat.le_of_eq h))
example: 6≠5 := s (nat.le_of_eq (@rfl ℕ 1))
lemma ne_51_6: (p 51) ≠ (p 6):= assume eq, have h: 51=6, from constructor_p_injective eq, absurd h (s (@nat.add_pos_left 1 (nat.le_of_eq (@rfl ℕ 1)) 44))
example: (p 51 ⇒ p 1) ≠ (p 6 ⇒ p 2 ):= assume eq, have h: (p 51) = (p 6), from (constructor_imp_injective eq).1, absurd h ne_51_6
--konec
-- pojem důkazu
def in_proof (Γ:set Form )(A:Form) (l:list Form): Prop := ( (∃ B C, A = A1 B C) ∨ (∃ B C D, A = A2 B C D) ∨ (∃ B C, A = A3 B C) ∨ (A ∈ Γ) ∨ (∃ B, B ∈ l ∧ (B⇒ A) ∈ l) )
def is_proof (Γ :set Form) (l:list Form) : Prop := list.rec_on l (1=1) (assume A li IH, in_proof Γ A li ∧ IH)
def is_provable (Γ: set Form ) (A:Form) := ∃ l: list Form, is_proof Γ (A::l)
local infixr `⊢`:40 := is_provable local prefix `⊢`: 40 := is_provable ∅
-- příklad lemma modus_ponens_rule: {A,A ⇒ B} ⊢ B:= --proof exists.intro [ --B A, A ⇒ B ] begin split , MP, split, proof, split, proof, exact rfl end --proof of proof /--/ ⟨by MP, by proof, by proof, rfl ⟩ -/ --následující definice je vhodná konvence pro psaní důkazů
def is_proof_with_cut (Γ :set Form) (l:list Form) : Prop := list.rec_on l (1=1) (assume A li IH, ( ((∃ B C, B ∈ li ∧ C∈ li ∧ {B,C} ⊢ A) ∨ (∃ B , B ∈ li ∧ {B} ⊢ A) ∨ ⊢ A ) ∨ in_proof Γ A li) ∧ IH)
def is_provable_with_cut (Γ:set Form) (A:Form): Prop:= ∃ l, is_proof_with_cut Γ (A::l) local infixr `⊢_cut `:40 := is_provable_with_cut
--konec --konec
--vlasnosti Hilbertovského důkazu
lemma is_proof_ind: is_proof Γ (A::l) → is_proof Γ l:= λ hp, hp.2 lemma in_proof_extend: in_proof Γ A l → l <+ li→ in_proof Γ A li:= begin intros, repeat {cases a,HK_verifier}, cases a, cases a_2 with hl hr, have hp: l ⊆ li, exact list.subset_of_sublist a_1, repeat {right}, existsi a, exact ⟨ hp hl, hp hr⟩
end
/- verze bez taktik assume Hpr H, or.elim Hpr (λ h, by tac) (or.rec (λ h, or.inr (or.inl h) ) (or.rec (λ h, or.inr (or.inr (or.inl h)))
(or.rec (λ h,or.inr( or.inr (or.inr (or.inl h)))) (λ h, exists.elim h (λ B (hp: B ∈ l ∧ (B ⇒ A) ∈ l), have hpp: l ⊆ li, from list.subset_of_sublist H,
or.inr( or.inr (or.inr (or.inr ( @exists.intro Form (λ B:Form, B ∈ li ∧ (B⇒ A) ∈ li) B ⟨ hpp (hp.1), hpp (hp.2)⟩ )))))))) ) -/
theorem is_proof_concat: is_proof Γ l → is_proof Γ li → is_proof Γ (l++li):= list.rec_on l (λ h hp, hp) (assume A lis IH Hl Hli, ⟨ in_proof_extend Hl.1 (list.sublist_append_left lis li) , IH (is_proof_ind Hl) Hli ⟩) . lemma is_proof_extend: is_proof Γ l → A ∈ l → in_proof Γ A l := list.rec_on l (λ h hp, absurd rfl (list.ne_nil_of_mem hp)) (λ D lis IH h hp,
have sub: lis<+D::lis, from by simp, or.elim (list.eq_or_ne_mem_of_mem hp) (assume H, H.symm ▸ in_proof_extend h.1 sub)
(λ H, in_proof_extend (IH (is_proof_ind h) H.2) sub)) .
theorem binary_cut: Γ ⊢ A → Γ ⊢ B → {A, B} ⊢ C → Γ ⊢ C := assume hA hB hAB, exists.elim hA (assume proofA is_proofA, exists.elim hB (assume proofB is_proofB, exists.elim hAB (assume proofAB,
let pr:=(A::proofA++B::proofB) in
have lem: ∀ l:list Form, is_proof {A,B} l → is_proof Γ (l ++ pr) , from begin intro l, induction l with D lis IH,
intro, exact (@is_proof_concat Γ (A::proofA) (B::proofB) is_proofA is_proofB), intros, split,
show is_proof Γ (lis++pr), -- přepsání cílů na něco přehlednějšího show in_proof Γ D (lis++pr), --totéž --D je axiom cases a.1, repeat {HK_verifier,cases a_1}, --předpoklad D∈ {A,B} --současně případy D=B a D=A repeat {cases a_1,
have h: D ∈ lis++pr, from by simp [a_1], exact is_proof_extend (IH (is_proof_ind a)) h}, apply false.elim a_1,
-- modus ponens
have subset: lis ⊆ ((lis ++ pr)), from by simp, cases a_1, have h: a_1 ∈ lis++pr, exact subset a_2.1, have h2: a_1 ⇒ D ∈ lis++pr, exact subset a_2.2, MP,
--indukční krok
exact IH (is_proof_ind a) end, --QED lem /- zkratka za následující: (λ D lis IH hp, show is_proof Γ (D::(lis ++ pr)), from ⟨ show in_proof Γ D (lis ++ (pr)), from or.elim hp.1 (λ hpp, or.inl hpp) --axiom1 (or.rec (λ hpp , or.inr (or.inl hpp)) --axiom2
(or.rec (λ hpp, or.inr (or.inr (or.inl hpp))) --axiom3
--předpoklad D∈ {A,B} (or.rec (
have hA: A∈ lis++pr, from by simp, have hB: B∈ lis++pr, from by simp, λ hlpp: ( D=B ∨ D = A ∨ false) , or.elim hlpp --předpoklad D∈ {A,B}
(λ hppp: D=B, have hb: D∈ lis++pr, from hppp.symm ▸ hB,
is_proof_extend (IH (is_proof_ind hp)) hb )
(λ hppp, or.elim hppp (λ hipp,
have ha: D∈ lis++pr, from hipp.symm ▸ hA,
is_proof_extend (IH (is_proof_ind hp)) ha )
false.elim ))
(λ Hpp:(∃ x:Form, x∈ lis ∧ (x⇒ D) ∈ lis), or.inr( or.inr (or.inr (or.inr( --modeus ponens
exists.elim Hpp (assume E hypp,
have subset: lis ⊆ ((lis ++ pr)), from by simp, @exists.intro Form (λ F:Form , F ∈ (lis ++ pr) ∧ (F⇒ D) ∈ (lis ++ pr)) E ⟨ subset hypp.1,subset hypp.2⟩ )))) )))))
, --Indukční krok IH (is_proof_ind hp) ⟩ ), -/--QED lem
assume hp, exists.intro (proofAB ++ pr) (lem (C::proofAB) hp) ))) . theorem unary_cut: Γ ⊢ A → {A} ⊢ B → Γ ⊢ B:=
assume pr1 pr2,
have hp: ({A}:set Form)=({A,A}:set Form), from funext (λ A, propext ⟨ λ h, or.inr h, λ h, or.elim h (λ hp, or.inl hp) (λ hp, hp)⟩ ),
binary_cut pr1 pr1 (hp ▸ pr2) .
theorem monotony: Γ ⊆ Δ → Γ ⊢ A → Δ ⊢ A := assume sub, have lem: ∀ l , is_proof Γ l → is_proof Δ l, begin intro l, induction l with B lis IH,
intro, exact rfl, intro hp, split, cases hp.1, repeat {HK_verifier,cases a}, have hpp: B ∈ Δ, from (sub a), repeat {HK_verifier},
exact IH hp.2 end, assume pr, exists.elim pr (λ proof hp, ⟨proof, lem (A::proof) hp ⟩ ) .
lemma wc_imp_proo: Γ ⊢_cut A → Γ ⊢ A :=
have lem : ∀ l A, is_proof_with_cut Γ l → A∈ l → Γ ⊢ A, from begin intro l, induction l with B lis IH, --empty list: intros, exact absurd rfl (list.ne_nil_of_mem a_1), --list indukce intros E hp ha, cases ha, rw[a], cases hp.1, cases a_1, --binární cases a_1 with C, cases a_1 with D, have HC: Γ ⊢ C, from IH C hp.2 a_1.1 , have HD: Γ ⊢ D, from IH D hp.2 a_1.2.1, exact binary_cut HC HD a_1.2.2,
--unární cases a_1, cases a_1 with C hC, have HC: Γ ⊢ C, from IH C hp.2 hC.1 , exact unary_cut HC hC.2,
--nulární have hyp: ∅ ⊆ Γ, from assume A hp, false.elim hp, exact monotony hyp a_1,
--norm proof repeat {cases a_1, existsi ([]: list Form), split; HK_verifier}, cases a_1 with G hG,
have Ha: Γ ⊢ G, exact IH G hp.2 (hG.1), have Hb: Γ ⊢ G ⇒ B, exact IH (G ⇒ B) hp.2 (hG.2), exact binary_cut Ha Hb modus_ponens_rule, --indukční krok exact IH E hp.2 a, end, begin intros, cases a with l hpp, have h: A∈ A::l, from by simp, exact lem (A::l) A hpp h end /- méně taktický důkaz assume l, list.rec_on l
(λ B h hp, absurd rfl (list.ne_nil_of_mem hp))
(λ B lis IH E hp ha, or.elim ha
(λ H: E=B, or.elim hp.1 (λ HP, or.elim HP (λ HPa, exists.elim HPa (λ C hC, exists.elim hC (λ D hD,
have HC: Γ ⊢ C, from IH C hp.2 hD.1 , have HD: Γ ⊢ D, from IH D hp.2 hD.2.1 ,
H.symm ▸ binary_cut HC HD hD.2.2 )) ) (λ HPa, or.elim HPa (λ HPa', exists.elim HPa' (λ C hC,
have HC: Γ ⊢ C, from IH C hp.2 hC.1 , H.symm ▸ unary_cut HC hC.2 ) )
(λ HPa', have hyp: ∅ ⊆ Γ, from assume A hp, false.elim hp, H.symm ▸ monotony hyp HPa' ) )) ( begin intro a, have lem: ∃ li,is_proof Γ (B::li), repeat {cases a, existsi ([]: list Form), split; proof}, cases a with G hG,
have Ha: Γ ⊢ G, exact IH G hp.2 (hG.1), have Hb: Γ ⊢ G ⇒ B, exact IH (G ⇒ B) hp.2 (hG.2), exact binary_cut Ha Hb modus_ponens_rule,
exact H.symm▸ lem end )) (λ H: E∈ lis, IH E hp.2 H)
), --QED lemma λ hp, exists.elim hp
(λ l hpp, have h: A∈ A::l, from by simp, lem (A::l) A hpp h) -/
. lemma proof_imp_wc: is_proof Γ l → is_proof_with_cut Γ l:= begin intro, induction l, exact rfl, cases a with a c, exact ⟨or.inr a, ih_1 c⟩ end
--konec
-- důkazy v HK
--deduction theorem lemma sets_eqv: ( {A,B}:set Form)= {A}∪ {B}:= funext (λ C, propext begin split, intro, repeat {cases a, assump}, apply false.elim, exact a,
intro, repeat {cases a, cases a, assump, apply false.elim, exact a} end )
lemma empty_union {a: set α }: a = ∅ ∪ a := begin apply funext, intro, apply propext, split, intro, assump, intro, cases a_1, apply false.elim, exact a_1, exact a_1 end
lemma A_imp_A: Γ ⊢ A ⇒ A := --proof exists.intro [ --A ⇒ A, (A ⇒ A ⇒ A) ⇒ (A ⇒ A), A ⇒ ((A ⇒ A) ⇒ A), (A ⇒ ((A ⇒ A) ⇒ A)) ⇒ (A ⇒ (A ⇒ A)) ⇒ (A ⇒ A), A ⇒ (A ⇒ A) ] --proof that it is a proof ⟨ by MP, by MP, by proof, by proof, by proof, rfl ⟩ lemma exchange: {A ⇒ B, A ⇒ B ⇒ C} ⊢ A ⇒ C:= begin existsi ([ (A ⇒ B) ⇒ A ⇒ C, A2 A B C, A ⇒ B, A ⇒ B ⇒ C]), HK_verifier end theorem deduction_theorem: Γ ∪ {A} ⊢ B → Γ ⊢ A ⇒ B:= have lem: ∀ l: list Form, is_proof (Γ ∪ {A}) l → ∀ B, B ∈ l → (Γ ⊢ A ⇒ B), from begin intro l, induction l with C li IH, --prázdný list intros, exact absurd rfl (list.ne_nil_of_mem a_1),
--indukční krok intros h B hp, cases hp,
--B=C rw[a],cases h.1,
--když je C axiom repeat {existsi ([C, A1 C A]), HK_verifier,cases a_1}, --když C∈ Γ ∪ {A} cases a_1, existsi ([C, A1 C A]), HK_verifier, cases a_1,rw[a_1], exact A_imp_A, apply false.elim, exact a_1,
--modus ponens cases a_1 with D hyp,
have Hd: Γ ⊢ A ⇒ D, exact IH h.2 D hyp.1, have Himp: Γ ⊢ A ⇒ D ⇒ C, exact IH h.2 (D ⇒ C) hyp.2, exact (binary_cut Hd Himp exchange), --Indukční krok exact IH h.2 B a end, assume h, exists.elim h (λ list hyp, have is_in: B∈ B::list, from by simp,
lem (B::list) hyp B is_in )
--pro ilustrace zelené bylo nahrazeno za počínaje begin) /- assume hpp: B=C,
or.elim h.1 --axiom 1 (λ Ax1, exists.elim Ax1 (λ E hE, exists.elim hE (λ F hF, exists.intro [ A1 (A1 E F) A , C] ⟨ begin repeat {right}, existsi C,exact ⟨by proof, or.inl (hpp.symm ▸ hF ▸ rfl)⟩ end, by proof, by proof, rfl ⟩ ))) (or.rec --axiom 2 (λ Ax2: (∃ E F G, C = A2 E F G), exists.elim Ax2 (λ E hE, exists.elim hE (λ F hF, exists.elim hF (λ G hG, @exists.intro (list Form) (λ li:list Form, (is_proof Γ ((A⇒ B)::li))) [ A1 (A2 E F G) A , C]
⟨ begin repeat {right}, existsi C,exact ⟨by proof, or.inl (hpp.symm ▸ hG ▸ rfl)⟩ end, by proof, by proof, rfl ⟩ ))))
(or.rec --axiom 3 (λ Ax3:(∃ B D, C = A3 B D), exists.elim Ax3 (λ E hE, exists.elim hE (λ F hF, @exists.intro (list Form) (λ li:list Form, (is_proof Γ ((A⇒ B)::li)) ) [ A1 (A3 E F) A , C] ⟨ begin repeat {right}, existsi C,exact ⟨by proof, or.inl (hpp.symm ▸ hF ▸ rfl)⟩ end, by proof, by proof, rfl ⟩ ))) (or.rec --předpoklad (assume as:C∈ Γ∪ {A}, or.elim as (assume ass: C∈ Γ, @exists.intro (list Form) (λ li:list Form, (is_proof Γ ((A⇒ B)::li))) [ A1 C A , C] ⟨ begin repeat {right}, existsi C,exact ⟨by proof, or.inl (hpp.symm ▸ rfl)⟩ end, by proof, by proof, rfl ⟩ )
(assume ass: C∈ {A}, or.elim ass (λ h:C=A, @eq.subst Form (λ E:Form, Γ⊢ A⇒ E) A B (eq.trans hpp h).symm (@A_imp_A A Γ )) false.elim) ) --modus ponens (assume as: (∃ B, B ∈ li ∧ (B⇒ C) ∈ li), exists.elim as (λ D, λ Hyp: D ∈ li ∧ (D⇒ C) ∈ li, have Hb: Γ ⊢ A ⇒ D, from IH h.2 D Hyp.1, have Himp: Γ ⊢ A ⇒ D ⇒ C, from IH h.2 (D ⇒ C) Hyp.2, have Hfin: Γ ⊢ A ⇒ C, from binary_cut Hb Himp exchange, hpp.symm ▸ Hfin ))
))) -/
-- theorem deduction_theorem2: {A} ⊢ B → ⊢ A ⇒ B:=
--konec --rules lemma trans: {A ⇒ B, B ⇒ C} ⊢ A ⇒ C:= sorry
lemma contraposition2: {~B ⇒ ~A} ⊢ A ⇒ B:= begin have h:{~B ⇒ ~A} ∪ {A} ⊢ B, existsi ([ (~B ⇒ A) ⇒ B, ~B ⇒ ~A, A3 A B, ~B ⇒ A, A1 A ~B, A]), HK_verifier,
exact deduction_theorem h end
lemma ex_falso_quodlibet: {~A,A} ⊢ B := begin existsi
([ (~B ⇒ A) ⇒ B, A3 A B, ~B ⇒ ~A, ~B ⇒ A, A1 ~A ~B, A1 A ~B, A , ~A ]),
HK_verifier end
lemma double_neg_law: {~~A} ⊢ A:= begin have h: ⊢ ~A ⇒ ~A, from A_imp_A, have hp: {~~A} ⊢_cut A, existsi ([ -- A (~A ⇒ ~A) ⇒ A, ~A ⇒ ~A, ~A ⇒ ~~A, A3 (~A) A, ~~A ⇒ ~A ⇒ ~~A, ~~A ]),
HK_verifier, exact wc_imp_proo hp end
lemma double_neg: {A} ⊢ ~~A:= begin have h: ⊢ ~~~A ⇒ ~A, exact deduction_theorem (@empty_union Form {~~~A} ▸ double_neg_law), have hp: {A} ⊢_cut ~~A, existsi
([ -- ~~A (~~~A ⇒ A) ⇒ ~~A, A3 A ~~A, ~~~A ⇒ ~A, ~~~A ⇒ A, A1 A ~~~A, A ]),
HK_verifier,exact wc_imp_proo hp end lemma RAA: {A ⇒ B, A ⇒ ~B} ⊢ ~A:= begin have h: ⊢ ~~A ⇒ A, from deduction_theorem (@empty_union Form {~~A} ▸ double_neg_law), have h1: {A ⇒ B} ⊢ ~~A ⇒ B, exact wc_imp_proo (exists.intro ([ ~~A ⇒ A, A ⇒ B ]) (by HK_verifier)), have h2: {A ⇒ ~B} ⊢ ~~A ⇒ ~B, exact wc_imp_proo (exists.intro ([ ~~A ⇒ A, A ⇒ ~B ]) (by HK_verifier)),
have lem: {A ⇒ B, A ⇒ ~B} ⊢_cut ~A, existsi ([(~~A ⇒ B) ⇒ ~A, A3 B (~A),~~A ⇒ ~B,~~A ⇒ B, A ⇒ B, A ⇒ ~B]), HK_verifier,
exact wc_imp_proo lem end
lemma contraposition: {A ⇒ B} ⊢ ~B ⇒ ~A:= begin -- have hp: {A ⇒ B, A ⇒ ~B} ⊢ ~A, from RAA,
have h: {A ⇒ B} ∪ {~B} ⊢_cut ~A, existsi ([A⇒ ~B, ~B ⇒ A ⇒ ~B, ~B, A ⇒ B]), HK_verifier,
exact deduction_theorem (wc_imp_proo h) end
lemma proof_by_cases_rule: {A ⇒ B, ~A ⇒ B} ⊢ B:= --proof
have lem: {A ⇒ B, ~A ⇒ B} ⊢_cut B, from exists.intro
( [ --B, ~B ⇒ ~A, (~B ⇒ ~A ) ⇒ B, ~B ⇒ ~~A, (~B ⇒ ~~A) ⇒ (~B ⇒ ~A) ⇒ B, ~A ⇒ B, A ⇒ B ] ) --proof that it is a proof --either: (by HK_verifier), -- or /- ⟨ by MP, by rules, by MP, by rules, by proof, by proof, by proof, rfl ⟩, -/
wc_imp_proo lem . --konec
--metarules
theorem PCP : Γ∪{A} ⊢ B → Γ ∪ {~A} ⊢ B → Γ ⊢ B :=
(assume h hneg, have hp: Γ ⊢ A ⇒ B, from deduction_theorem h, have hpp: Γ ⊢ ~A ⇒ B, from deduction_theorem hneg, binary_cut hp hpp proof_by_cases_rule )
lemma pr1 : Γ ⊢ A → Γ ⊢ B ⇒ A := begin intro, cases a, existsi ([A1 A B,A]++a), HK_verifier end
lemma pr2 : Γ ⊢ ~A → Γ ⊢ A ⇒ B := assume pr, unary_cut pr (deduction_theorem (@sets_eqv (~A) A ▸ ex_falso_quodlibet) ) lemma pr3: Γ ⊢ A → Γ ⊢ ~A ⇒ B:=
λ pr, pr2 (unary_cut pr double_neg)
--konec
--konec
--konec
--sémantika a korektnost def val (v:eval) :Form→ bool := λ A:Form, Form.rec_on A (λ n:ℕ, v n ) (λ A B:Form,λ a b:bool, bnot a || b ) (λ A:Form,λ a:bool, bnot a)
local postfix `∗ ` : 70 := val def is_taut (A : Form) := ∀ v : eval, v∗ A = tt
--korektnost axiomů: až takhle jednoduché to je, využije s toho, že lean umí dopočítat konkrétní hodnoty, když počítáme s ff a tt theorem A3_taut (A B:Form): is_taut (A3 A B):=assume v, have lem: ∀ a b:bool, bnot ((bnot (bnot b)) || (bnot a)) || ((bnot (bnot (bnot b) || a)) || b)=tt, from assume a b,
bool.rec_on a (bool.rec_on b rfl rfl) (bool.rec_on b rfl rfl), lem (v∗ A) (v∗ B)
--Konec
--konec --věta o úplnosti
--příprava def swap (A : Form) (v:eval): Form := if v∗A = tt then A else ~A def varswap (n:ℕ) (v:eval): Form:= if v (n)=tt then (p n) else ~(p n)
def flae (n:ℕ ) (v: eval): set Form:= { A |∃ i:ℕ , i<n ∧ A= varswap i v}
lemma flae_inclusion: ∀ n≤ m, flae n v ⊆ flae m v:= begin intros, intro, intro, cases a_1, split, tactic.swap, exact a_1, exact ⟨ (nat.le_trans a_2.1 H), a_2.2⟩ end
lemma flae_empty: flae 0 v = {} := funext (λ A:Form, show flae 0 v A = false , from propext ⟨ λ h, begin cases h, exact nat.succ_ne_zero a (nat.eq_zero_of_le_zero a_1.1) end , false.elim⟩ ) lemma flae_ind (n:ℕ ) (f :eval) : (flae n f ) ∪ {p n} = flae (n+1) (λ m:ℕ, nat.lt_by_cases (λ h: m<n+1, f m) (λ h: m=n+1, tt) (λ h: m>n+1, tt)) := let g:=(λ m:ℕ, nat.lt_by_cases (λ h: m<n+1, f m) (λ h: m=n+1, tt) (λ h: m>n+1, tt)) in
(funext (λ A:Form, show ((flae n f ) ∪ {p n}) A = (flae (n+1) g) A, from --rozdělíme důkaz na dvě implikace, první: propext (⟨λ h:((flae n f ) ∪ {p n}) A, or.elim h (sorry) (assume h1: A = p n ∨ false, show (flae (n+1) g) A, from or.elim h1 (assume h2: A = p n, or.inr (exists.intro n ⟨(nat.le_of_eq rfl), sorry, --neumím! h2 ⟩) ) false.elim) , --druhá implikace sorry ⟩ ) ) )
def nprovable (A:Form) (n:ℕ ):= ∀ v:eval, is_provable (flae n v) A
lemma PCP_app : ∀ n:ℕ, nprovable A (n+1) → nprovable A n:= assume n:ℕ, assume hp: nprovable A (n+1), assume f:eval,
let g1:= (λ m:ℕ, nat.lt_by_cases (λ h: m<n+1, f m) (λ h: m=n+1, tt) (λ h: m>n+1, tt)) in let g2:= λ m:ℕ, nat.lt_by_cases (λ h: m<n, f m) (λ h: m=n, ff) (λ h: m>n, tt) in
show (flae n f) ⊢ A, from PCP --důkaz Γ∪ {p (n+1)} ⊢ A:
(@eq.subst (set Form) (λ Γ, Γ ⊢ A) ( flae (n+1) g1) ((flae n f) ∪ {p n}) (flae_ind n f).symm (hp g1)) --důkaz Γ∪ {neg p (n+1)}⊢ A: (sorry )
theorem nprov_theorem: nprovable A n → ⊢ A := have H: nprovable A n → nprovable A 0, from nat.rec_on n (λ h, h ) (assume n IH hp, IH (PCP_app n hp) ), assume h: nprovable A n,
(@flae_empty (λ n:ℕ, tt)) ▸ (H h) (λ n:ℕ, tt )
theorem swaptt: v∗ A=tt → swap A v = A:= by {intro h, simp[h,swap]}
theorem swapff: v∗ A=ff → swap A v= neg A:= by {intro h, simp[h,swap]}
lemma ff_imp_tt: v∗ A = ff → v∗ (A ⇒ B) = tt:= assume h, calc v∗ (A ⇒ B) = bnot ff || v∗ B: h ▸ rfl .
def var_index (A:Form): ℕ := Form.rec_on A (λ n:ℕ, n+1) (λ A B:Form, λ na nb:ℕ, max na nb) (λ A:Form, λ m:ℕ, m)
lemma swap_in_flae: (swap (p n) v) ∈ flae (var_index (p n)) v := have h: var_index (p n) = n+1, from rfl, exists.intro n ⟨nat.lt_succ_self n, rfl⟩ .
lemma var_index_max: var_index A ≤ var_index (A ⇒ B):= le_max_left (var_index A) (var_index B) --konec --hlavní lemma lemma main : flae (var_index A) v ⊢ swap A v:=
Form.rec_on A --for variables (assume n:ℕ, begin have h: (swap (p n) v) ∈ flae (var_index (p n)) v, from swap_in_flae, existsi ([]), HK_verifier end ) --for implication (assume A B, let Γa := (flae (var_index A) v), Γb :set Form := (flae (var_index B) v), Γimp:= (flae (var_index ( A ⇒ B)) v) in assume IHa: Γa ⊢ swap A v, assume IHb: Γb ⊢ swap B v,
or.elim (bool.dichotomy (v∗ A)) --if A false (assume hpa: v∗A=ff,
have himp: swap ( A ⇒ B) v = A ⇒ B, from swaptt (ff_imp_tt hpa), have h: Γa ⊆ Γimp , from flae_inclusion (var_index A) var_index_max,
(calc Γa ⊢ swap A v → Γa ⊢ ~A : λ h, swapff hpa ▸ IHa ... → Γa ⊢ A ⇒ B : λ h, pr2 h ... → Γimp ⊢ A ⇒ B : λ hp, monotony h hp ... → Γimp ⊢ swap ( A ⇒ B) v : λ h, himp.symm ▸ h ) IHa ) -- if A true (assume hpa: v∗A=tt, or.elim (bool.dichotomy (v∗ B)) --if B is false (assume hpb: v∗B=ff, sorry)
--if B is true (assume hpb: v∗B=tt, sorry) )) --for negation (assume A, let Γa := (flae (var_index A) v) in
assume ha: Γa ⊢ swap A v, sorry )
theorem completeness: is_taut A → is_provable {} A := assume h:is_taut A, have H: nprovable A (var_index A), from λ v:eval, @eq.subst Form (λ B:Form, is_provable (flae (var_index A) v) B) (swap A v) A (swaptt (h v)) (main),
nprov_theorem H