# Theory FOL_Axiomatic

```(*
File:      FOL_Axiomatic.thy
Author:    Asta Halkjær From

This work is a formalization of the soundness and completeness of an axiomatic system
for first-order logic. The proof system is based on System Q1 by Smullyan
and the completeness proof follows his textbook "First-Order Logic" (Springer-Verlag 1968).
The completeness proof is in the Henkin style where a consistent set
is extended to a maximal consistent set using Lindenbaum's construction
and Henkin witnesses are added during the construction to ensure saturation as well.
The resulting set is a Hintikka set which, by the model existence theorem, is satisfiable
in the Herbrand universe.
*)

theory FOL_Axiomatic imports "HOL-Library.Countable" begin

section ‹Syntax›

datatype (params_tm: 'f) tm
= Var nat (‹❙#›)
| Fun 'f ‹'f tm list› (‹❙†›)

abbreviation Const (‹❙⋆›) where ‹❙⋆a ≡ ❙†a []›

datatype (params_fm: 'f, 'p) fm
= Falsity (‹❙⊥›)
| Pre 'p ‹'f tm list› (‹❙‡›)
| Imp ‹('f, 'p) fm› ‹('f, 'p) fm› (infixr ‹❙⟶› 55)
| Uni ‹('f, 'p) fm› (‹❙∀›)

abbreviation Neg (‹❙¬ _› [70] 70) where ‹❙¬ p ≡ p ❙⟶ ❙⊥›

term ‹❙∀(❙⊥ ❙⟶ ❙‡''P'' [❙†''f'' [❙#0]])›

section ‹Semantics›

definition shift (‹_⟨_:_⟩›) where
‹E⟨n:x⟩ m ≡ if m < n then E m else if m = n then x else E (m-1)›

primrec semantics_tm (‹⦇_, _⦈›) where
‹⦇E, F⦈ (❙#n) = E n›
| ‹⦇E, F⦈ (❙†f ts) = F f (map ⦇E, F⦈ ts)›

primrec semantics_fm (‹⟦_, _, _⟧›) where
‹⟦_, _, _⟧ ❙⊥ = False›
| ‹⟦E, F, G⟧ (❙‡P ts) = G P (map ⦇E, F⦈ ts)›
| ‹⟦E, F, G⟧ (p ❙⟶ q) = (⟦E, F, G⟧ p ⟶ ⟦E, F, G⟧ q)›
| ‹⟦E, F, G⟧ (❙∀p) = (∀x. ⟦E⟨0:x⟩, F, G⟧ p)›

proposition ‹⟦E, F, G⟧ (❙∀(❙‡P [❙# 0]) ❙⟶ ❙‡P [❙⋆a])›

section ‹Operations›

subsection ‹Shift›

context fixes n m :: nat begin

lemma shift_eq [simp]: ‹n = m ⟹ E⟨n:x⟩ m = x›

lemma shift_gt [simp]: ‹m < n ⟹ E⟨n:x⟩ m = E m›

lemma shift_lt [simp]: ‹n < m ⟹ E⟨n:x⟩ m = E (m-1)›

lemma shift_commute [simp]: ‹(E⟨n:y⟩⟨0:x⟩) = (E⟨0:x⟩⟨n+1:y⟩)›
proof
fix m
show ‹(E⟨n:y⟩⟨0:x⟩) m = (E⟨0:x⟩⟨n+1:y⟩) m›
unfolding shift_def by (cases m) simp_all
qed

end

subsection ‹Parameters›

abbreviation ‹params S ≡ ⋃p ∈ S. params_fm p›

lemma upd_params_tm [simp]: ‹f ∉ params_tm t ⟹ ⦇E, F(f := x)⦈ t = ⦇E, F⦈ t›
by (induct t) (auto cong: map_cong)

lemma upd_params_fm [simp]: ‹f ∉ params_fm p ⟹ ⟦E, F(f := x), G⟧ p = ⟦E, F, G⟧ p›
by (induct p arbitrary: E) (auto cong: map_cong)

lemma finite_params_tm [simp]: ‹finite (params_tm t)›
by (induct t) simp_all

lemma finite_params_fm [simp]: ‹finite (params_fm p)›
by (induct p) simp_all

subsection ‹Instantiation›

primrec lift_tm (‹❙↑›) where
‹❙↑(❙#n) = ❙#(n+1)›
| ‹❙↑(❙†f ts) = ❙†f (map ❙↑ ts)›

primrec inst_tm (‹⟪_'/_⟫›) where
‹⟪s/m⟫(❙#n) = (if n < m then ❙#n else if n = m then s else ❙#(n-1))›
| ‹⟪s/m⟫(❙†f ts) = ❙†f (map ⟪s/m⟫ ts)›

primrec inst_fm (‹⟨_'/_⟩›) where
‹⟨_/_⟩❙⊥ = ❙⊥›
| ‹⟨s/m⟩(❙‡P ts) = ❙‡P (map ⟪s/m⟫ ts)›
| ‹⟨s/m⟩(p ❙⟶ q) = ⟨s/m⟩p ❙⟶ ⟨s/m⟩q›
| ‹⟨s/m⟩(❙∀p) = ❙∀(⟨❙↑s/m+1⟩p)›

lemma lift_lemma [simp]: ‹⦇E⟨0:x⟩, F⦈ (❙↑t) = ⦇E, F⦈ t›
by (induct t) (auto cong: map_cong)

lemma inst_tm_semantics [simp]: ‹⦇E, F⦈ (⟪s/m⟫t) = ⦇E⟨m:⦇E, F⦈ s⟩, F⦈ t›
by (induct t) (auto cong: map_cong)

lemma inst_fm_semantics [simp]: ‹⟦E, F, G⟧ (⟨t/m⟩p) = ⟦E⟨m:⦇E, F⦈ t⟩, F, G⟧ p›
by (induct p arbitrary: E m t) (auto cong: map_cong)

subsection ‹Size›

text ‹The built-in ‹size› is not invariant under substitution.›

primrec size_fm where
‹size_fm ❙⊥ = 1›
| ‹size_fm (❙‡_ _) = 1›
| ‹size_fm (p ❙⟶ q) = 1 + size_fm p + size_fm q›
| ‹size_fm (❙∀p) = 1 + size_fm p›

lemma size_inst_fm [simp]: ‹size_fm (⟨t/m⟩p) = size_fm p›
by (induct p arbitrary: m t) simp_all

section ‹Propositional Semantics›

primrec boolean where
‹boolean _ _ ❙⊥ = False›
| ‹boolean G _ (❙‡P ts) = G P ts›
| ‹boolean G A (p ❙⟶ q) = (boolean G A p ⟶ boolean G A q)›
| ‹boolean _ A (❙∀p) = A (❙∀p)›

abbreviation ‹tautology p ≡ ∀G A. boolean G A p›

proposition ‹tautology (❙∀(❙‡P [❙#0]) ❙⟶ ❙∀(❙‡P [❙#0]))›
by simp

lemma boolean_semantics: ‹boolean (λa. G a ∘ map ⦇E, F⦈) ⟦E, F, G⟧ = ⟦E, F, G⟧›
proof
fix p
show ‹boolean (λa. G a ∘ map ⦇E, F⦈) ⟦E, F, G⟧ p = ⟦E, F, G⟧ p›
by (induct p) simp_all
qed

lemma tautology[simp]: ‹tautology p ⟹ ⟦E, F, G⟧ p›
using boolean_semantics by metis

proposition ‹∃p. (∀E F G. ⟦E, F, G⟧ p) ∧ ¬ tautology p›
by (metis boolean.simps(4) fm.simps(36) semantics_fm.simps(1,3,4))

section ‹Calculus›

text ‹Adapted from System Q1 by Smullyan in First-Order Logic (1968).›

inductive Axiomatic (‹⊢ _› [50] 50) where
TA: ‹tautology p ⟹ ⊢ p›
| IA: ‹⊢ ❙∀p ❙⟶ ⟨t/0⟩p›
| MP: ‹⊢ p ❙⟶ q ⟹ ⊢ p ⟹ ⊢ q›
| GR: ‹⊢ q ❙⟶ ⟨❙⋆a/0⟩p ⟹ a ∉ params {p, q} ⟹ ⊢ q ❙⟶ ❙∀p›

text ‹We simulate assumptions on the lhs of ‹⊢› with a chain of implications on the rhs.›

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

abbreviation Axiomatic_assms (‹_ ⊢ _› [50, 50] 50) where
‹ps ⊢ q ≡ ⊢ ps ❙↝ q›

section ‹Soundness›

theorem soundness: ‹⊢ p ⟹ ⟦E, F, G⟧ p›
proof (induct p arbitrary: F rule: Axiomatic.induct)
case (GR q a p)
moreover from this have ‹⟦E, F(a := x), G⟧ (q ❙⟶ ⟨❙⋆a/0⟩p)› for x
by blast
ultimately show ?case
by fastforce
qed auto

corollary ‹¬ (⊢ ❙⊥)›
using soundness by fastforce

section ‹Derived Rules›

lemma Imp1: ‹⊢ q ❙⟶ p ❙⟶ q›
and Imp2: ‹⊢ (p ❙⟶ q ❙⟶ r) ❙⟶ (p ❙⟶ q) ❙⟶ p ❙⟶ r›
and Neg: ‹⊢ ❙¬ ❙¬ p ❙⟶ p›
by (auto intro: TA)

text ‹The tautology axiom TA is not used directly beyond this point.›

lemma Tran': ‹⊢ (q ❙⟶ r) ❙⟶ (p ❙⟶ q) ❙⟶ p ❙⟶ r›
by (meson Imp1 Imp2 MP)

lemma Swap: ‹⊢ (p ❙⟶ q ❙⟶ r) ❙⟶ q ❙⟶ p ❙⟶ r›
by (meson Imp1 Imp2 Tran' MP)

lemma Tran: ‹⊢ (p ❙⟶ q) ❙⟶ (q ❙⟶ r) ❙⟶ p ❙⟶ r›
by (meson Swap Tran' MP)

text ‹Note that contraposition in the other direction is an instance of the lemma Tran.›

lemma contraposition: ‹⊢ (❙¬ q ❙⟶ ❙¬ p) ❙⟶ p ❙⟶ q›
by (meson Neg Swap Tran MP)

lemma GR': ‹⊢ ❙¬ ⟨❙⋆a/0⟩p ❙⟶ q ⟹ a ∉ params {p, q} ⟹ ⊢ ❙¬ (❙∀p) ❙⟶ q›
proof -
assume *: ‹⊢ ❙¬ ⟨❙⋆a/0⟩p ❙⟶ q› and a: ‹a ∉ params {p, q}›
have ‹⊢ ❙¬ q ❙⟶ ❙¬ ❙¬ ⟨❙⋆a/0⟩p›
using * Tran MP by metis
then have ‹⊢ ❙¬ q ❙⟶ ⟨❙⋆a/0⟩p›
using Neg Tran MP by metis
then have ‹⊢ ❙¬ q ❙⟶ ❙∀p›
using a by (auto intro: GR)
then have ‹⊢ ❙¬ (❙∀p) ❙⟶ ❙¬ ❙¬ q›
using Tran MP by metis
then show ?thesis
using Neg Tran MP by metis
qed

lemma imply_ImpE: ‹⊢ ps ❙↝ p ❙⟶ ps ❙↝ (p ❙⟶ q) ❙⟶ ps ❙↝ q›
proof (induct ps)
case Nil
then show ?case
by (metis Imp1 Swap MP imply.simps(1))
next
case (Cons r ps)
have ‹⊢ (r ❙⟶ ps ❙↝ p) ❙⟶ r ❙⟶ ps ❙↝ (p ❙⟶ q) ❙⟶ ps ❙↝ q›
by (meson Cons.hyps Imp1 Imp2 MP)
then have ‹⊢ (r ❙⟶ ps ❙↝ p) ❙⟶ (r ❙⟶ ps ❙↝ (p ❙⟶ q)) ❙⟶ r ❙⟶ ps ❙↝ q›
by (meson Imp1 Imp2 MP)
then show ?case
by simp
qed

lemma MP': ‹ps ⊢ p ❙⟶ q ⟹ ps ⊢ p ⟹ ps ⊢ q›
using imply_ImpE MP by metis

lemma imply_Cons [intro]: ‹ps ⊢ q ⟹ p # ps ⊢ q›
by (auto intro: MP Imp1)

lemma imply_head [intro]: ‹p # ps ⊢ p›
by (induct ps) (metis Imp1 Imp2 MP imply.simps, metis Imp1 Imp2 MP imply.simps(2))

lemma add_imply [simp]: ‹⊢ q ⟹ ps ⊢ q›
using imply_head by (metis MP imply.simps(2))

lemma imply_mem [simp]: ‹p ∈ set ps ⟹ ps ⊢ p›
using imply_head imply_Cons by (induct ps) fastforce+

lemma deduct1: ‹ps ⊢ p ❙⟶ q ⟹ p # ps ⊢ q›

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

lemma imply_swap_append: ‹ps @ qs ⊢ r ⟹ qs @ ps ⊢ r›
proof (induct qs arbitrary: ps)
case Cons
then show ?case
by (metis deduct1 imply.simps(2) imply_append)
qed simp

lemma deduct2: ‹p # ps ⊢ q ⟹ ps ⊢ p ❙⟶ q›
by (metis imply.simps imply_append imply_swap_append)

lemmas deduct [iff] = deduct1 deduct2

lemma cut: ‹p # ps ⊢ r ⟹ q # ps ⊢ p ⟹ q # ps ⊢ r›
by (meson MP' deduct(2) imply_Cons)

lemma Boole: ‹(❙¬ p) # ps ⊢ ❙⊥ ⟹ ps ⊢ p›
by (meson MP' Neg add_imply deduct(2))

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

section ‹Consistent›

definition ‹consistent S ≡ ∄S'. set S' ⊆ S ∧ S' ⊢ ❙⊥›

lemma UN_finite_bound:
assumes ‹finite A› and ‹A ⊆ (⋃n. f n)›
shows ‹∃m :: nat. A ⊆ (⋃n ≤ m. f n)›
using assms
proof (induct rule: finite_induct)
case (insert x A)
then obtain m where ‹A ⊆ (⋃n ≤ m. f n)›
by fast
then have ‹A ⊆ (⋃n ≤ (m + k). f n)› for k
by fastforce
moreover obtain m' where ‹x ∈ f m'›
using insert(4) by blast
ultimately have ‹{x} ∪ A ⊆ (⋃n ≤ m + m'. f n)›
by auto
then show ?case
by blast
qed simp

lemma split_list:
assumes ‹x ∈ set A›
shows ‹set (x # removeAll x A) = set A ∧ x ∉ set (removeAll x A)›
using assms by auto

lemma imply_params_fm: ‹params_fm (ps ❙↝ q) = params_fm q ∪ (⋃p ∈ set ps. params_fm p)›
by (induct ps) auto

lemma inconsistent_fm:
assumes ‹consistent S› and ‹¬ consistent ({p} ∪ S)›
obtains S' where ‹set S' ⊆ S› and ‹p # S' ⊢ ❙⊥›
proof -
obtain S' where S': ‹set S' ⊆ {p} ∪ S› ‹p ∈ set S'› ‹S' ⊢ ❙⊥›
using assms unfolding consistent_def by blast
then obtain S'' where S'': ‹set (p # S'') = set S'› ‹p ∉ set S''›
using split_list by metis
then have ‹p # S'' ⊢ ❙⊥›
using ‹S' ⊢ ❙⊥› imply_weaken by blast
then show ?thesis
using that S'' S'(1) Diff_insert_absorb Diff_subset_conv list.simps(15) by metis
qed

assumes ‹consistent S› and ‹❙¬ (❙∀p) ∈ S› and ‹a ∉ params S›
shows ‹consistent ({❙¬ ⟨❙⋆a/0⟩p} ∪ S)›
unfolding consistent_def
proof
assume ‹∃S'. set S' ⊆ {❙¬ ⟨❙⋆a/0⟩p} ∪ S ∧ S' ⊢ ❙⊥›
then obtain S' where ‹set S' ⊆ S› and ‹(❙¬ ⟨❙⋆a/0⟩p) # S' ⊢ ❙⊥›
using assms inconsistent_fm unfolding consistent_def by metis
then have ‹⊢ ❙¬ ⟨❙⋆a/0⟩p ❙⟶ S' ❙↝ ❙⊥›
by simp
moreover have ‹a ∉ params_fm p›
using assms(2-3) by auto
moreover have ‹∀p ∈ set S'. a ∉ params_fm p›
using ‹set S' ⊆ S› assms(3) by auto
then have ‹a ∉ params_fm (S' ❙↝ ❙⊥)›
ultimately have ‹⊢ ❙¬ (❙∀p) ❙⟶ S' ❙↝ ❙⊥›
using GR' by fast
then have ‹❙¬ (❙∀p) # S' ⊢ ❙⊥›
by simp
moreover have ‹set ((❙¬ (❙∀p)) # S') ⊆ S›
using ‹set S' ⊆ S› assms(2) by simp
ultimately show False
using assms(1) unfolding consistent_def by blast
qed

assumes ‹consistent S› and ‹❙∀p ∈ S›
shows ‹consistent ({⟨t/0⟩p} ∪ S)›
unfolding consistent_def
proof
assume ‹∃S'. set S' ⊆ {⟨t/0⟩p} ∪ S ∧ S' ⊢ ❙⊥›
then obtain S' where ‹set S' ⊆ S› and ‹⟨t/0⟩p # S' ⊢ ❙⊥›
using assms inconsistent_fm unfolding consistent_def by blast
moreover have ‹⊢ ❙∀p ❙⟶ ⟨t/0⟩p›
using IA by blast
ultimately have ‹❙∀p # S' ⊢ ❙⊥›
moreover have ‹set ((❙∀p) # S') ⊆ S›
using ‹set S' ⊆ S› assms(2) by simp
ultimately show False
using assms(1) unfolding consistent_def by blast
qed

section ‹Extension›

fun witness where
‹witness used (❙¬ (❙∀p)) = {❙¬ ⟨❙⋆(SOME a. a ∉ used)/0⟩p}›
| ‹witness _ _ = {}›

primrec extend where
‹extend S f 0 = S›
| ‹extend S f (Suc n) =
(let Sn = extend S f n in
if consistent ({f n} ∪ Sn)
then witness (params ({f n} ∪ Sn)) (f n) ∪ {f n} ∪ Sn
else Sn)›

definition ‹Extend S f ≡ ⋃n. extend S f n›

lemma extend_subset: ‹S ⊆ extend S f n›
by (induct n) (fastforce simp: Let_def)+

lemma Extend_subset: ‹S ⊆ Extend S f›
unfolding Extend_def by (metis Union_upper extend.simps(1) range_eqI)

lemma extend_bound: ‹(⋃n ≤ m. extend S f n) = extend S f m›
by (induct m) (simp_all add: atMost_Suc Let_def)

lemma finite_params_witness [simp]: ‹finite (params (witness used p))›
by (induct used p rule: witness.induct) simp_all

lemma finite_params_extend [simp]: ‹finite (params (extend S f n) - params S)›
by (induct n) (simp_all add: Let_def Un_Diff)

lemma Set_Diff_Un: ‹X - (Y ∪ Z) = X - Y - Z›
by blast

lemma infinite_params_extend:
assumes ‹infinite (UNIV - params S)›
shows ‹infinite (UNIV - params (extend S f n))›
proof -
have ‹finite (params (extend S f n) - params S)›
by simp
then obtain extra where ‹finite extra› ‹params (extend S f n) = extra ∪ params S›
using extend_subset by fast
then have ‹?thesis = infinite (UNIV - (extra ∪ params S))›
by simp
also have ‹… = infinite (UNIV - extra - params S)›
also have ‹… = infinite (UNIV - params S)›
using ‹finite extra› by (metis Set_Diff_Un Un_commute finite_Diff2)
finally show ?thesis
using assms ..
qed

lemma consistent_witness:
assumes ‹consistent S› and ‹p ∈ S› and ‹params S ⊆ used›
and ‹infinite (UNIV - used)›
shows ‹consistent (witness used p ∪ S)›
using assms
proof (induct used p rule: witness.induct)
case (1 used p)
moreover have ‹∃a. a ∉ used›
using 1(4) by (meson Diff_iff finite_params_fm finite_subset subset_iff)
ultimately obtain a where a: ‹witness used (❙¬ (❙∀p)) = {❙¬ ⟨❙⋆a/0⟩p}› and ‹a ∉ used›
by (metis someI_ex witness.simps(1))
then have ‹a ∉ params S›
using 1(3) by fast
then show ?case
using 1(1-2) a(1) consistent_add_witness by metis
qed (auto simp: assms)

lemma consistent_extend:
assumes ‹consistent S› and ‹infinite (UNIV - params S)›
shows ‹consistent (extend S f n)›
proof (induct n)
case (Suc n)
have ‹infinite (UNIV - params (extend S f n))›
using assms(2) infinite_params_extend by fast
with finite_params_fm have ‹infinite (UNIV - (params_fm (f n) ∪ params (extend S f n)))›
by (metis Set_Diff_Un Un_commute finite_Diff2)
with Suc consistent_witness[where S=‹{f n} ∪ extend S f n›] show ?case
qed (use assms(1) in simp)

lemma consistent_Extend:
assumes ‹consistent S› and ‹infinite (UNIV - params S)›
shows ‹consistent (Extend S f)›
unfolding consistent_def
proof
assume ‹∃S'. set S' ⊆ Extend S f ∧ S' ⊢ ❙⊥›
then obtain S' where ‹S' ⊢ ❙⊥› and ‹set S' ⊆ Extend S f›
unfolding consistent_def by blast
then obtain m where ‹set S' ⊆ (⋃n ≤ m. extend S f n)›
unfolding Extend_def using UN_finite_bound by (metis finite_set)
then have ‹set S' ⊆ extend S f m›
using extend_bound by blast
moreover have ‹consistent (extend S f m)›
using assms consistent_extend by blast
ultimately show False
unfolding consistent_def using ‹S' ⊢ ❙⊥› by blast
qed

section ‹Maximal›

definition ‹maximal S ≡ ∀p. p ∉ S ⟶ ¬ consistent ({p} ∪ S)›

lemma maximal_exactly_one:
assumes ‹consistent S› and ‹maximal S›
shows ‹p ∈ S ⟷ (❙¬ p) ∉ S›
proof
assume ‹p ∈ S›
show ‹(❙¬ p) ∉ S›
proof
assume ‹(❙¬ p) ∈ S›
then have ‹set [p, ❙¬ p] ⊆ S›
using ‹p ∈ S› by simp
moreover have ‹[p, ❙¬ p] ⊢ ❙⊥›
by blast
ultimately show False
using ‹consistent S› unfolding consistent_def by blast
qed
next
assume ‹(❙¬ p) ∉ S›
then have ‹¬ consistent ({❙¬ p} ∪ S)›
using ‹maximal S› unfolding maximal_def by blast
then obtain S' where ‹set S' ⊆ S› ‹(❙¬ p) # S' ⊢ ❙⊥›
using ‹consistent S› inconsistent_fm by blast
then have ‹S' ⊢ p›
using Boole by blast
have ‹consistent ({p} ∪ S)›
unfolding consistent_def
proof
assume ‹∃S'. set S' ⊆ {p} ∪ S ∧ S' ⊢ ❙⊥›
then obtain S'' where ‹set S'' ⊆ S› and ‹p # S'' ⊢ ❙⊥›
using assms inconsistent_fm unfolding consistent_def by blast
then have ‹S' @ S'' ⊢ ❙⊥›
using ‹S' ⊢ p› by (metis MP' add_imply imply.simps(2) imply_append)
moreover have ‹set (S' @ S'') ⊆ S›
using ‹set S' ⊆ S› ‹set S'' ⊆ S› by simp
ultimately show False
using ‹consistent S› unfolding consistent_def by blast
qed
then show ‹p ∈ S›
using ‹maximal S› unfolding maximal_def by blast
qed

lemma maximal_Extend:
assumes ‹surj f›
shows ‹maximal (Extend S f)›
unfolding maximal_def
proof safe
fix p
assume ‹p ∉ Extend S f› and ‹consistent ({p} ∪ Extend S f)›
obtain k where k: ‹f k = p›
using ‹surj f› unfolding surj_def by metis
then have ‹p ∉ extend S f (Suc k)›
using ‹p ∉ Extend S f› unfolding Extend_def by blast
then have ‹¬ consistent ({p} ∪ extend S f k)›
using k by (auto simp: Let_def)
moreover have ‹{p} ∪ extend S f k ⊆ {p} ∪ Extend S f›
unfolding Extend_def by blast
ultimately have ‹¬ consistent ({p} ∪ Extend S f)›
unfolding consistent_def by auto
then show False
using ‹consistent ({p} ∪ Extend S f)› by blast
qed

section ‹Saturation›

definition ‹saturated S ≡ ∀p. ❙¬ (❙∀p) ∈ S ⟶ (∃a. (❙¬ ⟨❙⋆a/0⟩p) ∈ S)›

lemma saturated_Extend:
assumes ‹consistent (Extend S f)› and ‹surj f›
shows ‹saturated (Extend S f)›
unfolding saturated_def
proof safe
fix p
assume *: ‹❙¬ (❙∀p) ∈ Extend S f›
obtain k where k: ‹f k = ❙¬ (❙∀p)›
using ‹surj f› unfolding surj_def by metis
have ‹extend S f k ⊆ Extend S f›
unfolding Extend_def by auto
then have ‹consistent ({❙¬ (❙∀p)} ∪ extend S f k)›
using assms(1) * unfolding consistent_def by blast
then have ‹∃a. extend S f (Suc k) = {❙¬ ⟨❙⋆a/0⟩p} ∪ {❙¬ (❙∀p)} ∪ extend S f k›
using k by (auto simp: Let_def)
moreover have ‹extend S f (Suc k) ⊆ Extend S f›
unfolding Extend_def by blast
ultimately show ‹∃a. ❙¬ ⟨❙⋆ a/0⟩p ∈ Extend S f›
by blast
qed

section ‹Hintikka›

locale Hintikka =
fixes H :: ‹('f, 'p) fm set›
assumes
FlsH: ‹❙⊥ ∉ H› and
ImpH: ‹(p ❙⟶ q) ∈ H ⟷ (p ∈ H ⟶ q ∈ H)› and
UniH: ‹(❙∀p ∈ H) ⟷ (∀t. ⟨t/0⟩p ∈ H)›

subsection ‹Model Existence›

abbreviation hmodel (‹⟦_⟧›) where ‹⟦H⟧ ≡ ⟦❙#, ❙†, λP ts. ❙‡P ts ∈ H⟧›

lemma semantics_tm_id [simp]: ‹⦇❙#, ❙†⦈ t = t›
by (induct t) (auto cong: map_cong)

lemma semantics_tm_id_map [simp]: ‹map ⦇❙#, ❙†⦈ ts = ts›
by (auto cong: map_cong)

theorem Hintikka_model:
assumes ‹Hintikka H›
shows ‹p ∈ H ⟷ ⟦H⟧ p›
proof (induct p rule: wf_induct[where r=‹measure size_fm›])
case 1
then show ?case ..
next
case (2 x)
then show ?case
using assms unfolding Hintikka_def by (cases x) auto
qed

subsection ‹Maximal Consistent Sets are Hintikka Sets›

lemma deriv_iff_MCS:
assumes ‹consistent S› and ‹maximal S›
shows ‹(∃ps. set ps ⊆ S ∧ ps ⊢ p) ⟷ p ∈ S›
proof
from assms maximal_exactly_one[OF assms(1)] show ‹∃ps. set ps ⊆ S ∧ ps ⊢ p ⟹ p ∈ S›
unfolding consistent_def using MP add_imply deduct1 imply.simps(1) imply_ImpE
by (metis insert_absorb insert_mono list.simps(15))
next
show ‹p ∈ S ⟹ ∃ps. set ps ⊆ S ∧ ps ⊢ p›
using imply_head by (metis empty_subsetI insert_absorb insert_mono list.set(1) list.simps(15))
qed

lemma Hintikka_Extend:
assumes ‹consistent H› and ‹maximal H› and ‹saturated H›
shows ‹Hintikka H›
proof
show ‹❙⊥ ∉ H›
using assms deriv_iff_MCS unfolding consistent_def by fast
next
fix p q
show ‹(p ❙⟶ q) ∈ H ⟷ (p ∈ H ⟶ q ∈ H)›
using deriv_iff_MCS[OF assms(1-2)] maximal_exactly_one[OF assms(1-2)]
by (metis Imp1 contraposition add_imply deduct1 insert_subset list.simps(15))
next
fix p
show ‹(❙∀p ∈ H) ⟷ (∀t. ⟨t/0⟩p ∈ H)›
unfolding maximal_def saturated_def by metis
qed

section ‹Countable Formulas›

instance tm :: (countable) countable
by countable_datatype

instance fm :: (countable, countable) countable
by countable_datatype

section ‹Completeness›

lemma infinite_Diff_fin_Un: ‹infinite (X - Y) ⟹ finite Z ⟹ infinite (X - (Z ∪ Y))›

theorem strong_completeness:
fixes p :: ‹('f :: countable, 'p :: countable) fm›
assumes ‹∀(E :: _ ⇒ 'f tm) F G. (∀q ∈ X. ⟦E, F, G⟧ q) ⟶ ⟦E, F, G⟧ p›
and ‹infinite (UNIV - params X)›
shows ‹∃ps. set ps ⊆ X ∧ ps ⊢ p›
proof (rule ccontr)
assume ‹∄ps. set ps ⊆ X ∧ ps ⊢ p›
then have *: ‹∄ps. set ps ⊆ X ∧ ((❙¬ p) # ps ⊢ ❙⊥)›
using Boole by blast

let ?S = ‹{❙¬ p} ∪ X›
let ?H = ‹Extend ?S from_nat›

from inconsistent_fm have ‹consistent ?S›
unfolding consistent_def using * imply_Cons by metis
moreover have ‹infinite (UNIV - params ?S)›
using assms(2) finite_params_fm by (simp add: infinite_Diff_fin_Un)
ultimately have ‹consistent ?H› and ‹maximal ?H›
using consistent_Extend maximal_Extend surj_from_nat by blast+
moreover from this have ‹saturated ?H›
using saturated_Extend by fastforce
ultimately have ‹Hintikka ?H›
using assms(2) Hintikka_Extend by blast

have ‹⟦?H⟧ p› if ‹p ∈ ?S› for p
using that Extend_subset Hintikka_model ‹Hintikka ?H› by blast
then have ‹⟦?H⟧ (❙¬ p)› and ‹∀q ∈ X. ⟦?H⟧ q›
by blast+
moreover from this have ‹⟦?H⟧ p›
using assms(1) by blast
ultimately show False
by simp
qed

theorem completeness:
fixes p :: ‹(nat, nat) fm›
assumes ‹∀(E :: nat ⇒ nat tm) F G. ⟦E, F, G⟧ p›
shows ‹⊢ p›
using assms strong_completeness[where X=‹{}›] by auto

section ‹Main Result›

abbreviation valid :: ‹(nat, nat) fm ⇒ bool› where
‹valid p ≡ ∀(E :: nat ⇒ nat tm) F G. ⟦E, F, G⟧ p›

theorem main: ‹valid p ⟷ (⊢ p)›
using completeness soundness by blast

end
```