# Theory Implicational_Logic

```(*
Authors: Asta Halkjær From & Jørgen Villadsen, DTU Compute
*)

section ‹Formalization of the Bernays-Tarski Axiom System for Classical Implicational Logic›

(* Uncomment for Full Classical Propositional Logic *)

subsection ‹Syntax, Semantics and Axiom System›

theory Implicational_Logic imports Main begin

datatype form =
(*Falsity (‹⊥›) |*)
Pro nat (‹⋅›) |
Imp form form (infixr ‹→› 55)

primrec semantics (infix ‹⊨› 50) where
(*‹I ⊨ ⊥ = False› |*)
‹I ⊨ ⋅ n = I n› |
‹I ⊨ p → q = (I ⊨ p ⟶ I ⊨ q)›

inductive Ax (‹⊢ _› 50) where
(*Expl: ‹⊢ ⊥ → p› |*)
Simp: ‹⊢ p → q → p› |
Tran: ‹⊢ (p → q) → (q → r) → p → r› |
MP: ‹⊢ p → q ⟹ ⊢ p ⟹ ⊢ q› |
PR: ‹⊢ (p → q) → p ⟹ ⊢ p›

subsection ‹Soundness and Derived Formulas›

theorem soundness: ‹⊢ p ⟹ I ⊨ p›
by (induct p rule: Ax.induct) auto

lemma Swap: ‹⊢ (p → q → r) → q → p → r›
proof -
have ‹⊢ q → (q → r) → r›
using MP PR Simp Tran by metis
then show ?thesis
using MP Tran by meson
qed

lemma Peirce: ‹⊢ ((p → q) → p) → p›
using MP PR Simp Swap Tran by meson

lemma Hilbert: ‹⊢ (p → p → q) → p → q›
using MP MP Tran Tran Peirce .

lemma Id: ‹⊢ p → p›
using MP Hilbert Simp .

lemma Tran': ‹⊢ (q → r) → (p → q) → p → r›
using MP Swap Tran .

lemma Frege: ‹⊢ (p → q → r) → (p → q) → p → r›
using MP MP Tran MP MP Tran Swap Tran' MP Tran' Hilbert .

lemma Imp1: ‹⊢ (q → s) → ((q → r) → s) → s›
using MP Peirce Tran Tran' by meson

lemma Imp2: ‹⊢ ((r → s) → s) → ((q → r) → s) → s›
using MP Tran MP Tran Simp .

lemma Imp3: ‹⊢ ((q → s) → s) → (r → s) → (q → r) → s›
using MP Swap Tran by meson

subsection ‹Completeness and Main Theorem›

fun pros where
‹pros (p → q) = remdups (pros p @ pros q)› |
‹pros p = (case p of (⋅ n) ⇒ [n] | _ ⇒ [])›

lemma distinct_pros: ‹distinct (pros p)›
by (induct p) simp_all

primrec imply (infixr ‹↝› 56) where
‹[] ↝ q = q› |
‹p # ps ↝ q = p → ps ↝ q›

lemma imply_append: ‹ps @ qs ↝ r = ps ↝ qs ↝ r›
by (induct ps) simp_all

abbreviation Ax_assms (infix ‹⊢› 50) where ‹ps ⊢ q ≡ ⊢ ps ↝ q›

lemma imply_Cons: ‹ps ⊢ q ⟹ p # ps ⊢ q›
proof -
assume ‹ps ⊢ q›
with MP Simp have ‹⊢ p → ps ↝ q› .
then show ?thesis
by simp
qed

lemma imply_head: ‹p # ps ⊢ p›
by (induct ps) (use MP Frege Simp imply.simps in metis)+

lemma imply_mem: ‹p ∈ set ps ⟹ ps ⊢ p›
by (induct ps) (use imply_Cons imply_head in auto)

lemma imply_MP: ‹⊢ ps ↝ (p → q) → ps ↝ p → ps ↝ q›
proof (induct ps)
case (Cons r ps)
then have ‹⊢ (r → ps ↝ (p → q)) → (r → ps ↝ p) → r → ps ↝ q›
using MP Frege Simp by meson
then show ?case
by simp
qed (auto intro: Id)

lemma MP': ‹ps ⊢ p → q ⟹ ps ⊢ p ⟹ ps ⊢ q›
using MP imply_MP by metis

lemma imply_swap_append: ‹ps @ qs ⊢ r ⟹ qs @ ps ⊢ r›
by (induct qs arbitrary: ps) (simp, metis MP' imply_append imply_Cons imply_head imply.simps(2))

lemma imply_deduct: ‹p # ps ⊢ q ⟹ ps ⊢ p → q›
using imply_append imply_swap_append imply.simps by metis

lemma add_imply [simp]: ‹⊢ p ⟹ ps ⊢ p›
proof -
note MP
moreover have ‹⊢ p → ps ↝ p›
moreover assume ‹⊢ p›
ultimately show ?thesis .
qed

lemma imply_weaken: ‹ps ⊢ p ⟹ set ps ⊆ set ps' ⟹ ps' ⊢ p›
by (induct ps arbitrary: p) (simp, metis MP' imply_deduct imply_mem insert_subset list.set(2))

abbreviation ‹lift t s p ≡ if t then (p → s) → s else p → s›

abbreviation ‹lifts I s ≡ map (λn. lift (I n) s (⋅ n))›

lemma lifts_weaken: ‹lifts I s l ⊢ p ⟹ set l ⊆ set l' ⟹ lifts I s l' ⊢ p›
using imply_weaken by (metis (no_types, lifting) image_mono set_map)

lemma lifts_pros_lift: ‹lifts I s (pros p) ⊢ lift (I ⊨ p) s p›
proof (induct p)
case (Imp q r)
consider ‹¬ I ⊨ q› | ‹I ⊨ r› | ‹I ⊨ q› ‹¬ I ⊨ r›
by blast
then show ?case
proof cases
case 1
then have ‹lifts I s (pros (q → r)) ⊢ q → s›
using Imp(1) lifts_weaken[where l' = ‹pros (q → r)›] by simp
then have ‹lifts I s (pros (q → r)) ⊢ ((q → r) → s) → s›
using Imp1 MP' add_imply by blast
with 1 show ?thesis
by simp
next
case 2
then have ‹lifts I s (pros (q → r)) ⊢ (r → s) → s›
using Imp(2) lifts_weaken[where l' = ‹pros (q → r)›] by simp
then have ‹lifts I s (pros (q → r)) ⊢ ((q → r) → s) → s›
using Imp2 MP' add_imply by blast
with 2 show ?thesis
by simp
next
case 3
then have ‹lifts I s (pros (q → r)) ⊢ (q → s) → s› ‹lifts I s (pros (q → r)) ⊢ r → s›
using Imp lifts_weaken[where l' = ‹pros (q → r)›] by simp_all
then have ‹lifts I s (pros (q → r)) ⊢ (q → r) → s›
using Imp3 MP' add_imply by blast
with 3 show ?thesis
by simp
qed
qed (auto intro: Id Ax.intros)

lemma lifts_pros: ‹I ⊨ p ⟹ lifts I p (pros p) ⊢ p›
proof -
assume ‹I ⊨ p›
then have ‹lifts I p (pros p) ⊢ (p → p) → p›
using lifts_pros_lift[of I p p] by simp
then show ?thesis
using Id MP' add_imply by blast
qed

theorem completeness: ‹∀I. I ⊨ p ⟹ ⊢ p›
proof -
let ?A = ‹λl I. lifts I p l ⊢ p›
let ?B = ‹λl. ∀I. ?A l I ∧ distinct l›
assume ‹∀I. I ⊨ p›
moreover have ‹?B l ⟹ (⋀n l. ?B (n # l) ⟹ ?B l) ⟹ ?B []› for l
by (induct l) blast+
moreover have ‹?B (n # l) ⟹ ?B l› for n l
proof -
assume *: ‹?B (n # l)›
show ‹?B l›
proof
fix I
from * have ‹?A (n # l) (I(n := True))› ‹?A (n # l) (I(n := False))›
by blast+
moreover from * have ‹∀m ∈ set l. ∀t. (I(n := t)) m = I m›
by simp
ultimately have ‹((⋅ n → p) → p) # lifts I p l ⊢ p› ‹(⋅ n → p) # lifts I p l ⊢ p›
by (simp_all cong: map_cong)
then have ‹?A l I›
using MP' imply_deduct by blast
moreover from * have ‹distinct (n # l)›
by blast
ultimately show ‹?A l I ∧ distinct l›
by simp
qed
qed
ultimately have ‹?B []›
using lifts_pros distinct_pros by blast
then show ?thesis
by simp
qed

theorem main: ‹(⊢ p) = (∀I. I ⊨ p)›
using soundness completeness by blast

subsection ‹Reference›

text ‹Wikipedia 🌐‹https://en.wikipedia.org/wiki/Implicational_propositional_calculus› July 2022›

end
```