# Theory FOL_Fitting

(*  Author:     Stefan Berghofer, TU Muenchen, 2003
Author: Asta Halkjær From, DTU Compute, 2019
Thanks to John Bruntse Larsen, Anders Schlichtkrull & Jørgen Villadsen
*)

section ‹First-Order Logic According to Fitting›

theory FOL_Fitting
imports "HOL-Library.Countable"
begin

section ‹Miscellaneous Utilities›

text ‹Some facts about (in)finite sets›

theorem set_inter_compl_diff [simp]: ‹- A ∩ B = B - A› by blast

section ‹Terms and formulae›

text ‹
\label{sec:terms}
The datatypes of terms and formulae in {\em de Bruijn notation}
are defined as follows:
›

datatype 'a "term"
= Var nat
| App 'a ‹'a term list›

datatype ('a, 'b) form
= FF
| TT
| Pred 'b ‹'a term list›
| And ‹('a, 'b) form› ‹('a, 'b) form›
| Or ‹('a, 'b) form› ‹('a, 'b) form›
| Impl ‹('a, 'b) form› ‹('a, 'b) form›
| Neg ‹('a, 'b) form›
| Forall ‹('a, 'b) form›
| Exists ‹('a, 'b) form›

text ‹
We use ‹'a› and ‹'b› to denote the type of
{\em function symbols} and {\em predicate symbols}, respectively.
In applications ‹App a ts› and predicates
‹Pred a ts›, the length of ‹ts› is considered
to be a part of the function or predicate name, so ‹App a [t]›
and ‹App a [t,u]› refer to different functions.

The size of a formula is used later for wellfounded induction. The
default implementation provided by the datatype package is not quite
what we need, so here is an alternative version:
›

primrec size_form :: ‹('a, 'b) form ⇒ nat› where
‹size_form FF = 0›
| ‹size_form TT = 0›
| ‹size_form (Pred _ _) = 0›
| ‹size_form (And p q) = size_form p + size_form q + 1›
| ‹size_form (Or p q) = size_form p + size_form q + 1›
| ‹size_form (Impl p q) = size_form p + size_form q + 1›
| ‹size_form (Neg p) = size_form p + 1›
| ‹size_form (Forall p) = size_form p + 1›
| ‹size_form (Exists p) = size_form p + 1›

subsection ‹Closed terms and formulae›

text ‹
Many of the results proved in the following sections are restricted
to closed terms and formulae. We call a term or formula {\em closed at
level ‹i›}, if it only contains loose'' bound variables with
indices smaller than ‹i›.
›

primrec
closedt :: ‹nat ⇒ 'a term ⇒ bool› and
closedts :: ‹nat ⇒ 'a term list ⇒ bool› where
‹closedt m (Var n) = (n < m)›
| ‹closedt m (App a ts) = closedts m ts›
| ‹closedts m [] = True›
| ‹closedts m (t # ts) = (closedt m t ∧ closedts m ts)›

primrec closed :: ‹nat ⇒ ('a, 'b) form ⇒ bool› where
‹closed m FF = True›
| ‹closed m TT = True›
| ‹closed m (Pred b ts) = closedts m ts›
| ‹closed m (And p q) = (closed m p ∧ closed m q)›
| ‹closed m (Or p q) = (closed m p ∧ closed m q)›
| ‹closed m (Impl p q) = (closed m p ∧ closed m q)›
| ‹closed m (Neg p) = closed m p›
| ‹closed m (Forall p) = closed (Suc m) p›
| ‹closed m (Exists p) = closed (Suc m) p›

theorem closedt_mono: assumes le: ‹i ≤ j›
shows ‹closedt i (t::'a term) ⟹ closedt j t›
and ‹closedts i (ts::'a term list) ⟹ closedts j ts›
using le by (induct t and ts rule: closedt.induct closedts.induct) simp_all

theorem closed_mono: assumes le: ‹i ≤ j›
shows ‹closed i p ⟹ closed j p›
using le
proof (induct p arbitrary: i j)
case (Pred i l)
then show ?case
using closedt_mono by simp
qed auto

subsection ‹Substitution›

text ‹
We now define substitution functions for terms and formulae. When performing
substitutions under quantifiers, we need to {\em lift} the terms to be substituted
for variables, in order for the loose'' bound variables to point to the right
position.
›

primrec
substt :: ‹'a term ⇒ 'a term ⇒ nat ⇒ 'a term› ("_[_'/_]" [300, 0, 0] 300) and
substts :: ‹'a term list ⇒ 'a term ⇒ nat ⇒ 'a term list› ("_[_'/_]" [300, 0, 0] 300) where
‹(Var i)[s/k] = (if k < i then Var (i - 1) else if i = k then s else Var i)›
| ‹(App a ts)[s/k] = App a (ts[s/k])›
| ‹[][s/k] = []›
| ‹(t # ts)[s/k] = t[s/k] # ts[s/k]›

primrec
liftt :: ‹'a term ⇒ 'a term› and
liftts :: ‹'a term list ⇒ 'a term list› where
‹liftt (Var i) = Var (Suc i)›
| ‹liftt (App a ts) = App a (liftts ts)›
| ‹liftts [] = []›
| ‹liftts (t # ts) = liftt t # liftts ts›

primrec subst :: ‹('a, 'b) form ⇒ 'a term ⇒ nat ⇒ ('a, 'b) form›
("_[_'/_]" [300, 0, 0] 300) where
‹FF[s/k] = FF›
| ‹TT[s/k] = TT›
| ‹(Pred b ts)[s/k] = Pred b (ts[s/k])›
| ‹(And p q)[s/k] = And (p[s/k]) (q[s/k])›
| ‹(Or p q)[s/k] = Or (p[s/k]) (q[s/k])›
| ‹(Impl p q)[s/k] = Impl (p[s/k]) (q[s/k])›
| ‹(Neg p)[s/k] = Neg (p[s/k])›
| ‹(Forall p)[s/k] = Forall (p[liftt s/Suc k])›
| ‹(Exists p)[s/k] = Exists (p[liftt s/Suc k])›

theorem lift_closed [simp]:
‹closedt 0 (t::'a term) ⟹ closedt 0 (liftt t)›
‹closedts 0 (ts::'a term list) ⟹ closedts 0 (liftts ts)›
by (induct t and ts rule: closedt.induct closedts.induct) simp_all

theorem subst_closedt [simp]:
assumes u: ‹closedt 0 u›
shows ‹closedt (Suc i) t ⟹ closedt i (t[u/i])›
and ‹closedts (Suc i) ts ⟹ closedts i (ts[u/i])›
using u closedt_mono(1)
by (induct t and ts rule: closedt.induct closedts.induct) auto

theorem subst_closed [simp]:
‹closedt 0 t ⟹ closed (Suc i) p ⟹ closed i (p[t/i])›
by (induct p arbitrary: i t) simp_all

theorem subst_size_form [simp]: ‹size_form (subst p t i) = size_form p›
by (induct p arbitrary: i t) simp_all

subsection ‹Parameters›

text ‹
The introduction rule ‹ForallI› for the universal quantifier,
as well as the elimination rule ‹ExistsE› for the existential
quantifier introduced in \secref{sec:proof-calculus} require the
quantified variable to be replaced by a fresh'' parameter. Fitting's
solution is to use a new nullary function symbol for this purpose.
To express that a function symbol is fresh'', we introduce functions
for collecting all function symbols occurring in a term or formula.
›

primrec
paramst :: ‹'a term ⇒ 'a set› and
paramsts :: ‹'a term list ⇒ 'a set› where
‹paramst (Var n) = {}›
| ‹paramst (App a ts) = {a} ∪ paramsts ts›
| ‹paramsts [] = {}›
| ‹paramsts (t # ts) = (paramst t ∪ paramsts ts)›

primrec params :: ‹('a, 'b) form ⇒ 'a set› where
‹params FF = {}›
| ‹params TT = {}›
| ‹params (Pred b ts) = paramsts ts›
| ‹params (And p q) = params p ∪ params q›
| ‹params (Or p q) = params p ∪ params q›
| ‹params (Impl p q) = params p ∪ params q›
| ‹params (Neg p) = params p›
| ‹params (Forall p) = params p›
| ‹params (Exists p) = params p›

text‹
We also define parameter substitution functions on terms and formulae
that apply a function ‹f› to all function symbols.
›

primrec
psubstt :: ‹('a ⇒ 'c) ⇒ 'a term ⇒ 'c term› and
psubstts :: ‹('a ⇒ 'c) ⇒ 'a term list ⇒ 'c term list› where
‹psubstt f (Var i) = Var i›
| ‹psubstt f (App x ts) = App (f x) (psubstts f ts)›
| ‹psubstts f [] = []›
| ‹psubstts f (t # ts) = psubstt f t # psubstts f ts›

primrec psubst :: ‹('a ⇒ 'c) ⇒ ('a, 'b) form ⇒ ('c, 'b) form› where
‹psubst f FF = FF›
| ‹psubst f TT = TT›
| ‹psubst f (Pred b ts) = Pred b (psubstts f ts)›
| ‹psubst f (And p q) = And (psubst f p) (psubst f q)›
| ‹psubst f (Or p q) = Or (psubst f p) (psubst f q)›
| ‹psubst f (Impl p q) = Impl (psubst f p) (psubst f q)›
| ‹psubst f (Neg p) = Neg (psubst f p)›
| ‹psubst f (Forall p) = Forall (psubst f p)›
| ‹psubst f (Exists p) = Exists (psubst f p)›

theorem psubstt_closed [simp]:
‹closedt i (psubstt f t) = closedt i t›
‹closedts i (psubstts f ts) = closedts i ts›
by (induct t and ts rule: closedt.induct closedts.induct) simp_all

theorem psubst_closed [simp]:
‹closed i (psubst f p) = closed i p›
by (induct p arbitrary: i) simp_all

theorem psubstt_subst [simp]:
‹psubstt f (substt t u i) = substt (psubstt f t) (psubstt f u) i›
‹psubstts f (substts ts u i) = substts (psubstts f ts) (psubstt f u) i›
by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all

theorem psubstt_lift [simp]:
‹psubstt f (liftt t) = liftt (psubstt f t)›
‹psubstts f (liftts ts) = liftts (psubstts f ts)›
by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all

theorem psubst_subst [simp]:
‹psubst f (subst P t i) = subst (psubst f P) (psubstt f t) i›
by (induct P arbitrary: i t) simp_all

theorem psubstt_upd [simp]:
‹x ∉ paramst (t::'a term) ⟹ psubstt (f(x := y)) t = psubstt f t›
‹x ∉ paramsts (ts::'a term list) ⟹ psubstts (f(x := y)) ts = psubstts f ts›
by (induct t and ts rule: psubstt.induct psubstts.induct) (auto split: sum.split)

theorem psubst_upd [simp]: ‹x ∉ params P ⟹ psubst (f(x := y)) P = psubst f P›
by (induct P) (simp_all del: fun_upd_apply)

theorem psubstt_id:
fixes t :: ‹'a term› and ts :: ‹'a term list›
shows ‹psubstt id t = t› and ‹psubstts (λx. x) ts = ts›
by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all

theorem psubst_id [simp]: ‹psubst id = id›
proof
fix p :: ‹('a, 'b) form›
show ‹psubst id p = id p›
by (induct p) (simp_all add: psubstt_id)
qed

theorem psubstt_image [simp]:
‹paramst (psubstt f t) = f  paramst t›
‹paramsts (psubstts f ts) = f  paramsts ts›
by (induct t and ts rule: paramst.induct paramsts.induct) (simp_all add: image_Un)

theorem psubst_image [simp]: ‹params (psubst f p) = f  params p›
by (induct p) (simp_all add: image_Un)

section ‹Semantics›

text ‹
\label{sec:semantics}
In this section, we define evaluation functions for terms and formulae.
Evaluation is performed relative to an environment mapping indices of variables
to values. We also introduce a function, denoted by ‹e⟨i:a⟩›, for inserting
a value ‹a› at position ‹i› into the environment. All values of variables
with indices less than ‹i› are left untouched by this operation, whereas the
values of variables with indices greater or equal than ‹i› are shifted one
position up.
›

definition shift :: ‹(nat ⇒ 'a) ⇒ nat ⇒ 'a ⇒ nat ⇒ 'a› ("_⟨_:_⟩" [90, 0, 0] 91) where
‹e⟨i:a⟩ = (λj. if j < i then e j else if j = i then a else e (j - 1))›

lemma shift_eq [simp]: ‹i = j ⟹ (e⟨i:T⟩) j = T›

lemma shift_gt [simp]: ‹j < i ⟹ (e⟨i:T⟩) j = e j›

lemma shift_lt [simp]: ‹i < j ⟹ (e⟨i:T⟩) j = e (j - 1)›

lemma shift_commute [simp]: ‹e⟨i:U⟩⟨0:T⟩ = e⟨0:T⟩⟨Suc i:U⟩›
proof
fix x
show ‹(e⟨i:U⟩⟨0:T⟩) x = (e⟨0:T⟩⟨Suc i:U⟩) x›
by (cases x) (simp_all add: shift_def)
qed

primrec
evalt :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒ 'a term ⇒ 'c› and
evalts :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒ 'a term list ⇒ 'c list› where
‹evalt e f (Var n) = e n›
| ‹evalt e f (App a ts) = f a (evalts e f ts)›
| ‹evalts e f [] = []›
| ‹evalts e f (t # ts) = evalt e f t # evalts e f ts›

primrec eval :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒
('b ⇒ 'c list ⇒ bool) ⇒ ('a, 'b) form ⇒ bool› where
‹eval e f g FF = False›
| ‹eval e f g TT = True›
| ‹eval e f g (Pred a ts) = g a (evalts e f ts)›
| ‹eval e f g (And p q) = ((eval e f g p) ∧ (eval e f g q))›
| ‹eval e f g (Or p q) = ((eval e f g p) ∨ (eval e f g q))›
| ‹eval e f g (Impl p q) = ((eval e f g p) ⟶ (eval e f g q))›
| ‹eval e f g (Neg p) = (¬ (eval e f g p))›
| ‹eval e f g (Forall p) = (∀z. eval (e⟨0:z⟩) f g p)›
| ‹eval e f g (Exists p) = (∃z. eval (e⟨0:z⟩) f g p)›

text ‹
We write ‹e,f,g,ps ⊨ p› to mean that the formula ‹p› is a
semantic consequence of the list of formulae ‹ps› with respect to an
environment ‹e› and interpretations ‹f› and ‹g› for
function and predicate symbols, respectively.
›

definition model :: ‹(nat ⇒ 'c) ⇒ ('a ⇒ 'c list ⇒ 'c) ⇒ ('b ⇒ 'c list ⇒ bool) ⇒
('a, 'b) form list ⇒ ('a, 'b) form ⇒ bool› ("_,_,_,_ ⊨ _" [50,50] 50) where
‹(e,f,g,ps ⊨ p) = (list_all (eval e f g) ps ⟶ eval e f g p)›

text ‹
The following substitution lemmas relate substitution and evaluation functions:
›

theorem subst_lemma' [simp]:
‹evalt e f (substt t u i) = evalt (e⟨i:evalt e f u⟩) f t›
‹evalts e f (substts ts u i) = evalts (e⟨i:evalt e f u⟩) f ts›
by (induct t and ts rule: substt.induct substts.induct) simp_all

theorem lift_lemma [simp]:
‹evalt (e⟨0:z⟩) f (liftt t) = evalt e f t›
‹evalts (e⟨0:z⟩) f (liftts ts) = evalts e f ts›
by (induct t and ts rule: liftt.induct liftts.induct) simp_all

theorem subst_lemma [simp]:
‹eval e f g (subst a t i) = eval (e⟨i:evalt e f t⟩) f g a›
by (induct a arbitrary: e i t) simp_all

theorem upd_lemma' [simp]:
‹n ∉ paramst t ⟹ evalt e (f(n := x)) t = evalt e f t›
‹n ∉ paramsts ts ⟹ evalts e (f(n := x)) ts = evalts e f ts›
by (induct t and ts rule: paramst.induct paramsts.induct) auto

theorem upd_lemma [simp]:
‹n ∉ params p ⟹ eval e (f(n := x)) g p = eval e f g p›
by (induct p arbitrary: e) simp_all

theorem list_upd_lemma [simp]: ‹list_all (λp. n ∉ params p) G ⟹
list_all (eval e (f(n := x)) g) G = list_all (eval e f g) G›
by (induct G) simp_all

theorem psubst_eval' [simp]:
‹evalt e f (psubstt h t) = evalt e (λp. f (h p)) t›
‹evalts e f (psubstts h ts) = evalts e (λp. f (h p)) ts›
by (induct t and ts rule: psubstt.induct psubstts.induct) simp_all

theorem psubst_eval:
‹eval e f g (psubst h p) = eval e (λp. f (h p)) g p›
by (induct p arbitrary: e) simp_all

text ‹
In order to test the evaluation function defined above, we apply it
to an example:
›

theorem ex_all_commute_eval:
‹eval e f g (Impl (Exists (Forall (Pred p [Var 1, Var 0])))
(Forall (Exists (Pred p [Var 0, Var 1]))))›
apply simp
txt ‹
Simplification yields the following proof state:
@{subgoals [display]}
This is easily proved using intuitionistic logic:
›
by iprover

section ‹Proof calculus›

text ‹
\label{sec:proof-calculus}
We now introduce a natural deduction proof calculus for first order logic.
The derivability judgement ‹G ⊢ a› is defined as an inductive predicate.
›

inductive deriv :: ‹('a, 'b) form list ⇒ ('a, 'b) form ⇒ bool› ("_ ⊢ _" [50,50] 50) where
Assum: ‹a ∈ set G ⟹ G ⊢ a›
| TTI: ‹G ⊢ TT›
| FFE: ‹G ⊢ FF ⟹ G ⊢ a›
| NegI: ‹a # G ⊢ FF ⟹ G ⊢ Neg a›
| NegE: ‹G ⊢ Neg a ⟹ G ⊢ a ⟹ G ⊢ FF›
| Class: ‹Neg a # G ⊢ FF ⟹ G ⊢ a›
| AndI: ‹G ⊢ a ⟹ G ⊢ b ⟹ G ⊢ And a b›
| AndE1: ‹G ⊢ And a b ⟹ G ⊢ a›
| AndE2: ‹G ⊢ And a b ⟹ G ⊢ b›
| OrI1: ‹G ⊢ a ⟹ G ⊢ Or a b›
| OrI2: ‹G ⊢ b ⟹ G ⊢ Or a b›
| OrE: ‹G ⊢ Or a b ⟹ a # G ⊢ c ⟹ b # G ⊢ c ⟹ G ⊢ c›
| ImplI: ‹a # G ⊢ b ⟹ G ⊢ Impl a b›
| ImplE: ‹G ⊢ Impl a b ⟹ G ⊢ a ⟹ G ⊢ b›
| ForallI: ‹G ⊢ a[App n []/0] ⟹ list_all (λp. n ∉ params p) G ⟹
n ∉ params a ⟹ G ⊢ Forall a›
| ForallE: ‹G ⊢ Forall a ⟹ G ⊢ a[t/0]›
| ExistsI: ‹G ⊢ a[t/0] ⟹ G ⊢ Exists a›
| ExistsE: ‹G ⊢ Exists a ⟹ a[App n []/0] # G ⊢ b ⟹
list_all (λp. n ∉ params p) G ⟹ n ∉ params a ⟹ n ∉ params b ⟹ G ⊢ b›

text ‹
The following derived inference rules are sometimes useful in applications.
›

theorem Class': ‹Neg A # G ⊢ A ⟹ G ⊢ A›
by (rule Class, rule NegE, rule Assum) (simp, iprover)

theorem cut: ‹G ⊢ A ⟹ A # G ⊢ B ⟹ G ⊢ B›
by (rule ImplE, rule ImplI)

theorem ForallE': ‹G ⊢ Forall a ⟹ subst a t 0 # G ⊢ B ⟹ G ⊢ B›
by (rule cut, rule ForallE)

text ‹
As an example, we show that the excluded middle, a commutation property
for existential and universal quantifiers, the drinker principle, as well
as Peirce's law are derivable in the calculus given above.
›

theorem tnd: ‹[] ⊢ Or (Pred p []) (Neg (Pred p []))› (is ‹_ ⊢ ?or›)
proof -
have ‹[Neg ?or] ⊢ Neg ?or›
moreover { have ‹[Pred p [], Neg ?or] ⊢ Neg ?or›
moreover have ‹[Pred p [], Neg ?or] ⊢ Pred p []›
then have ‹[Pred p [], Neg ?or] ⊢ ?or›
by (rule OrI1)
ultimately have ‹[Pred p [], Neg ?or] ⊢ FF›
by (rule NegE)
then have ‹[Neg ?or] ⊢ Neg (Pred p [])›
by (rule NegI)
then have ‹[Neg ?or] ⊢ ?or›
by (rule OrI2) }
ultimately have ‹[Neg ?or] ⊢ FF›
by (rule NegE)
then show ?thesis
by (rule Class)
qed

theorem ex_all_commute:
‹([]::(nat, 'b) form list) ⊢ Impl (Exists (Forall (Pred p [Var 1, Var 0])))
(Forall (Exists (Pred p [Var 0, Var 1])))›
proof -
let ?forall = ‹Forall (Pred p [Var 1, Var 0]) :: (nat, 'b) form›

have ‹[Exists ?forall] ⊢ Exists ?forall›
moreover { have ‹[?forall[App 1 []/0], Exists ?forall] ⊢ Forall (Pred p [App 1 [], Var 0])›
moreover have ‹[Pred p [App 1 [], Var 0][App 0 []/0], ?forall[App 1 []/0],
Exists ?forall] ⊢ Pred p [Var 0, App 0 []][App 1 []/0]›
ultimately have ‹[?forall[App 1 []/0], Exists ?forall] ⊢ (Pred p [Var 0, App 0 []])[App 1 []/0]›
by (rule ForallE') }
then have ‹[?forall[App 1 []/0], Exists ?forall] ⊢ Exists (Pred p [Var 0, App 0 []])›
by (rule ExistsI)
moreover have ‹list_all (λp. 1 ∉ params p) [Exists ?forall]›
by simp
moreover have ‹1 ∉ params ?forall›
by simp
moreover have ‹1 ∉ params (Exists (Pred p [Var 0, App (0 :: nat) []]))›
by simp
ultimately have ‹[Exists ?forall] ⊢ Exists (Pred p [Var 0, App 0 []])›
by (rule ExistsE)
then have ‹[Exists ?forall] ⊢ (Exists (Pred p [Var 0, Var 1]))[App 0 []/0]›
by simp
moreover have ‹list_all (λp. 0 ∉ params p) [Exists ?forall]›
by simp
moreover have ‹0 ∉ params (Exists (Pred p [Var 0, Var 1]))›
by simp
ultimately have ‹[Exists ?forall] ⊢ Forall (Exists (Pred p [Var 0, Var 1]))›
by (rule ForallI)
then show ?thesis
by (rule ImplI)
qed

theorem drinker: ‹([]::(nat, 'b) form list) ⊢
Exists (Impl (Pred P [Var 0]) (Forall (Pred P [Var 0])))›
proof -
let ?impl = ‹(Impl (Pred P [Var 0]) (Forall (Pred P [Var 0]))) :: (nat, 'b) form›
let ?G' = ‹[Pred P [Var 0], Neg (Exists ?impl)]›
let ?G = ‹Neg (Pred P [App 0 []]) # ?G'›

have ‹?G ⊢ Neg (Exists ?impl)›
moreover have ‹Pred P [App 0 []] # ?G ⊢ Neg (Pred P [App 0 []])›
and ‹Pred P [App 0 []] # ?G ⊢ Pred P [App 0 []]›
then have ‹Pred P [App 0 []] # ?G ⊢ FF›
by (rule NegE)
then have ‹Pred P [App 0 []] # ?G ⊢ Forall (Pred P [Var 0])›
by (rule FFE)
then have ‹?G ⊢ ?impl[App 0 []/0]›
using ImplI by simp
then have ‹?G ⊢ Exists ?impl›
by (rule ExistsI)
ultimately have ‹?G ⊢ FF›
by (rule NegE)
then have ‹?G' ⊢ Pred P [Var 0][App 0 []/0]›
using Class by simp
moreover have ‹list_all (λp. (0 :: nat) ∉ params p) ?G'›
by simp
moreover have ‹(0 :: nat) ∉ params (Pred P [Var 0])›
by simp
ultimately have ‹?G' ⊢ Forall (Pred P [Var 0])›
by (rule ForallI)
then have ‹[Neg (Exists ?impl)] ⊢ ?impl[Var 0/0]›
using ImplI by simp
then have ‹[Neg (Exists ?impl)] ⊢ Exists ?impl›
by (rule ExistsI)
then show ?thesis
by (rule Class')
qed

theorem peirce:
‹[] ⊢ Impl (Impl (Impl (Pred P []) (Pred Q [])) (Pred P [])) (Pred P [])›
(is ‹[] ⊢ Impl ?PQP (Pred P [])›)
proof -
let ?PQPP = ‹Impl ?PQP (Pred P [])›

have ‹[?PQP, Neg ?PQPP] ⊢ ?PQP›
moreover { have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ Neg ?PQPP›
moreover have ‹[?PQP, Pred P [], ?PQP, Neg ?PQPP] ⊢ Pred P []›
then have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ ?PQPP›
by (rule ImplI)
ultimately have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ FF›
by (rule NegE) }
then have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ Pred Q []›
by (rule FFE)
then have ‹[?PQP, Neg ?PQPP] ⊢ Impl (Pred P []) (Pred Q [])›
by (rule ImplI)
ultimately have ‹[?PQP, Neg ?PQPP] ⊢ Pred P []›
by (rule ImplE)
then have ‹[Neg ?PQPP] ⊢ ?PQPP›
by (rule ImplI)
then show ‹[] ⊢ ?PQPP›
by (rule Class')
qed

section ‹Correctness›

text ‹
The correctness of the proof calculus introduced in \secref{sec:proof-calculus}
can now be proved by induction on the derivation of @{term ‹G ⊢ p›}, using the
substitution rules proved in \secref{sec:semantics}.
›

theorem correctness: ‹G ⊢ p ⟹ ∀e f g. e,f,g,G ⊨ p›
proof (induct p rule: deriv.induct)
case (Assum a G)
then show ?case by (simp add: model_def list_all_iff)
next
case (ForallI G a n)
show ?case
proof (intro allI)
fix f g and e :: ‹nat ⇒ 'c›
have ‹∀z. e, (f(n := λx. z)), g, G ⊨ (a[App n []/0])›
using ForallI by blast
then have ‹∀z. list_all (eval e f g) G ⟶ eval (e⟨0:z⟩) f g a›
using ForallI unfolding model_def by simp
then show ‹e,f,g,G ⊨ Forall a› unfolding model_def by simp
qed
next
case (ExistsE G a n b)
show ?case
proof (intro allI)
fix f g and e :: ‹nat ⇒ 'c›
obtain z where ‹list_all (eval e f g) G ⟶ eval (e⟨0:z⟩) f g a›
using ExistsE unfolding model_def by simp blast
then have ‹e, (f(n := λx. z)), g, G ⊨ b›
using ExistsE unfolding model_def by simp
then show ‹e,f,g,G ⊨ b›
using ExistsE unfolding model_def by simp
qed

section ‹Completeness›

text ‹
The goal of this section is to prove completeness of the natural deduction
actual proof, it is useful to note that the following two formulations of
completeness are equivalent:
\begin{enumerate}
\item All valid formulae are derivable, i.e.
‹ps ⊨ p ⟹ ps ⊢ p›
\item All consistent sets are satisfiable
\end{enumerate}
The latter property is called the {\em model existence theorem}. To see why 2
implies 1, observe that ‹Neg p, ps \<notturnstile> FF› implies
that ‹Neg p, ps› is consistent, which, by the model existence theorem,
implies that ‹Neg p, ps› has a model, which in turn implies that
‹ps \<notTurnstile> p›. By contraposition, it therefore follows
from ‹ps ⊨ p› that ‹Neg p, ps ⊢ FF›, which allows us to
deduce ‹ps ⊢ p› using rule ‹Class›.

In most textbooks on logic, a set ‹S› of formulae is called {\em consistent},
if no contradiction can be derived from ‹S› using a {\em specific proof calculus},
i.e.\ ‹S \<notturnstile> FF›. Rather than defining consistency relative to
a {\em specific} calculus, Fitting uses the more general approach of describing
properties that all consistent sets must have (see \secref{sec:consistent-sets}).

The key idea behind the proof of the model existence theorem is to
extend a consistent set to one that is {\em maximal} (see \secref{sec:extend}).
In order to do this, we use the fact that the set of formulae is enumerable
(see \secref{sec:enumeration}), which allows us to form a sequence
$\phi_0$, $\phi_1$, $\phi_2$, $\ldots$ containing all formulae.
We can then construct a sequence $S_i$ of consistent sets as follows:
$\begin{array}{l} S_0 = S \\ S_{i+1} = \left\{\begin{array}{ll} S_i \cup \{\phi_i\} & \hbox{if } S_i \cup \{\phi_i\} \hbox{ consistent} \\ S_i & \hbox{otherwise} \end{array}\right. \end{array}$
To obtain a maximal consistent set, we form the union $\bigcup_i S_i$ of these
sets. To ensure that this union is still consistent, additional closure
(see \secref{sec:closure}) and finiteness (see \secref{sec:finiteness})
properties are needed.
It can be shown that a maximal consistent set is a {\em Hintikka set}
(see \secref{sec:hintikka}). Hintikka sets are satisfiable in {\em Herbrand}
models, where closed terms coincide with their interpretation.
›

subsection ‹Consistent sets›

text ‹
\label{sec:consistent-sets}
In this section, we describe an abstract criterion for consistent sets.
A set of sets of formulae is called a {\em consistency property}, if the
following holds:
›

definition consistency :: ‹('a, 'b) form set set ⇒ bool› where
‹consistency C = (∀S. S ∈ C ⟶
(∀p ts. ¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)) ∧
FF ∉ S ∧ Neg TT ∉ S ∧
(∀Z. Neg (Neg Z) ∈ S ⟶ S ∪ {Z} ∈ C) ∧
(∀A B. And A B ∈ S ⟶ S ∪ {A, B} ∈ C) ∧
(∀A B. Neg (Or A B) ∈ S ⟶ S ∪ {Neg A, Neg B} ∈ C) ∧
(∀A B. Or A B ∈ S ⟶ S ∪ {A} ∈ C ∨ S ∪ {B} ∈ C) ∧
(∀A B. Neg (And A B) ∈ S ⟶ S ∪ {Neg A} ∈ C ∨ S ∪ {Neg B} ∈ C) ∧
(∀A B. Impl A B ∈ S ⟶ S ∪ {Neg A} ∈ C ∨ S ∪ {B} ∈ C) ∧
(∀A B. Neg (Impl A B) ∈ S ⟶ S ∪ {A, Neg B} ∈ C) ∧
(∀P t. closedt 0 t ⟶ Forall P ∈ S ⟶ S ∪ {P[t/0]} ∈ C) ∧
(∀P t. closedt 0 t ⟶ Neg (Exists P) ∈ S ⟶ S ∪ {Neg (P[t/0])} ∈ C) ∧
(∀P. Exists P ∈ S ⟶ (∃x. S ∪ {P[App x []/0]} ∈ C)) ∧
(∀P. Neg (Forall P) ∈ S ⟶ (∃x. S ∪ {Neg (P[App x []/0])} ∈ C)))›

text ‹
In \secref{sec:finiteness}, we will show how to extend a consistency property
to one that is of {\em finite character}. However, the above
definition of a consistency property cannot be used for this, since there is
a problem with the treatment of formulae of the form ‹Exists P› and
‹Neg (Forall P)›. Fitting therefore suggests to define an {\em alternative
consistency property} as follows:
›

definition alt_consistency :: ‹('a, 'b) form set set ⇒ bool› where
‹alt_consistency C = (∀S. S ∈ C ⟶
(∀p ts. ¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)) ∧
FF ∉ S ∧ Neg TT ∉ S ∧
(∀Z. Neg (Neg Z) ∈ S ⟶ S ∪ {Z} ∈ C) ∧
(∀A B. And A B ∈ S ⟶ S ∪ {A, B} ∈ C) ∧
(∀A B. Neg (Or A B) ∈ S ⟶ S ∪ {Neg A, Neg B} ∈ C) ∧
(∀A B. Or A B ∈ S ⟶ S ∪ {A} ∈ C ∨ S ∪ {B} ∈ C) ∧
(∀A B. Neg (And A B) ∈ S ⟶ S ∪ {Neg A} ∈ C ∨ S ∪ {Neg B} ∈ C) ∧
(∀A B. Impl A B ∈ S ⟶ S ∪ {Neg A} ∈ C ∨ S ∪ {B} ∈ C) ∧
(∀A B. Neg (Impl A B) ∈ S ⟶ S ∪ {A, Neg B} ∈ C) ∧
(∀P t. closedt 0 t ⟶ Forall P ∈ S ⟶ S ∪ {P[t/0]} ∈ C) ∧
(∀P t. closedt 0 t ⟶ Neg (Exists P) ∈ S ⟶ S ∪ {Neg (P[t/0])} ∈ C) ∧
(∀P x. (∀a ∈ S. x ∉ params a) ⟶ Exists P ∈ S ⟶
S ∪ {P[App x []/0]} ∈ C) ∧
(∀P x. (∀a ∈ S. x ∉ params a) ⟶ Neg (Forall P) ∈ S ⟶
S ∪ {Neg (P[App x []/0])} ∈ C))›

text ‹
Note that in the clauses for ‹Exists P› and ‹Neg (Forall P)›,
the first definition requires the existence of a parameter ‹x› with a certain
property, whereas the second definition requires that all parameters ‹x› that
are new for ‹S› have a certain property. A consistency property can easily be
turned into an alternative consistency property by applying a suitable parameter
substitution:
›

definition mk_alt_consistency :: ‹('a, 'b) form set set ⇒ ('a, 'b) form set set› where
‹mk_alt_consistency C = {S. ∃f. psubst f  S ∈ C}›

theorem alt_consistency:
assumes conc: ‹consistency C›
shows ‹alt_consistency (mk_alt_consistency C)› (is ‹alt_consistency ?C'›)
unfolding alt_consistency_def
proof (intro allI impI conjI)
fix f :: ‹'a ⇒ 'a› and S :: ‹('a, 'b) form set›

assume ‹S ∈ mk_alt_consistency C›
then obtain f where sc: ‹psubst f  S ∈ C› (is ‹?S' ∈ C›)
unfolding mk_alt_consistency_def by blast

fix p ts
show ‹¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)›
proof
assume *: ‹Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S›
then have ‹psubst f (Pred p ts) ∈ ?S'›
by blast
then have ‹Pred p (psubstts f ts) ∈ ?S'›
by simp
then have ‹Neg (Pred p (psubstts f ts)) ∉ ?S'›
using conc sc by (simp add: consistency_def)
then have ‹Neg (Pred p ts) ∉ S›
by force
then show False
using * by blast
qed

have ‹FF ∉ ?S'› and ‹Neg TT ∉ ?S'›
using conc sc unfolding consistency_def by simp_all
then show ‹FF ∉ S› and ‹Neg TT ∉ S›
by (force, force)

{ fix Z
assume ‹Neg (Neg Z) ∈ S›
then have ‹psubst f (Neg (Neg Z)) ∈ ?S'›
by blast
then have ‹?S' ∪ {psubst f Z} ∈ C›
using conc sc by (simp add: consistency_def)
then show ‹S ∪ {Z} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix A B
assume ‹And A B ∈ S›
then have ‹psubst f (And A B) ∈ ?S'›
by blast
then have ‹?S' ∪ {psubst f A, psubst f B} ∈ C›
using conc sc by (simp add: consistency_def)
then show ‹S ∪ {A, B} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix A B
assume ‹Neg (Or A B) ∈ S›
then have ‹psubst f (Neg (Or A B)) ∈ ?S'›
by blast
then have ‹?S' ∪ {Neg (psubst f A), Neg (psubst f B)} ∈ C›
using conc sc by (simp add: consistency_def)
then show ‹S ∪ {Neg A, Neg B} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix A B
assume ‹Neg (Impl A B) ∈ S›
then have ‹psubst f (Neg (Impl A B)) ∈ ?S'›
by blast
then have ‹?S' ∪ {psubst f A, Neg (psubst f B)} ∈ C›
using conc sc by (simp add: consistency_def)
then show ‹S ∪ {A, Neg B} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix A B
assume ‹Or A B ∈ S›
then have ‹psubst f (Or A B) ∈ ?S'›
by blast
then have ‹?S' ∪ {psubst f A} ∈ C ∨ ?S' ∪ {psubst f B} ∈ C›
using conc sc by (simp add: consistency_def)
then show ‹S ∪ {A} ∈ ?C' ∨ S ∪ {B} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix A B
assume ‹Neg (And A B) ∈ S›
then have ‹psubst f (Neg (And A B)) ∈ ?S'›
by blast
then have ‹?S' ∪ {Neg (psubst f A)} ∈ C ∨ ?S' ∪ {Neg (psubst f B)} ∈ C›
using conc sc by (simp add: consistency_def)
then show ‹S ∪ {Neg A} ∈ ?C' ∨ S ∪ {Neg B} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix A B
assume ‹Impl A B ∈ S›
then have ‹psubst f (Impl A B) ∈ ?S'›
by blast
then have ‹?S' ∪ {Neg (psubst f A)} ∈ C ∨ ?S' ∪ {psubst f B} ∈ C›
using conc sc by (simp add: consistency_def)
then show ‹S ∪ {Neg A} ∈ ?C' ∨ S ∪ {B} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix P and t :: ‹'a term›
assume ‹closedt 0 t› and ‹Forall P ∈ S›
then have ‹psubst f (Forall P) ∈ ?S'›
by blast
then have ‹?S' ∪ {psubst f P[psubstt f t/0]} ∈ C›
using ‹closedt 0 t› conc sc by (simp add: consistency_def)
then show ‹S ∪ {P[t/0]} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix P and t :: ‹'a term›
assume ‹closedt 0 t› and ‹Neg (Exists P) ∈ S›
then have ‹psubst f (Neg (Exists P)) ∈ ?S'›
by blast
then have ‹?S' ∪ {Neg (psubst f P[psubstt f t/0])} ∈ C›
using ‹closedt 0 t› conc sc by (simp add: consistency_def)
then show ‹S ∪ {Neg (P[t/0])} ∈ ?C'›
unfolding mk_alt_consistency_def by auto }

{ fix P :: ‹('a, 'b) form› and x f'
assume ‹∀a ∈ S. x ∉ params a› and ‹Exists P ∈ S›
moreover have ‹psubst f (Exists P) ∈ ?S'›
using calculation by blast
then have ‹∃y. ?S' ∪ {psubst f P[App y []/0]} ∈ C›
using conc sc by (simp add: consistency_def)
then obtain y where ‹?S' ∪ {psubst f P[App y []/0]} ∈ C›
by blast

moreover have ‹psubst (f(x := y))  S = ?S'›
using calculation by (simp cong add: image_cong)
moreover have ‹psubst (f(x := y))
S ∪ {psubst (f(x := y)) P[App ((f(x := y)) x) []/0]} ∈ C›
using calculation by auto
ultimately have ‹∃f. psubst f  S ∪ {psubst f P[App (f x) []/0]} ∈ C›
by blast
then show ‹S ∪ {P[App x []/0]} ∈ ?C'›
unfolding mk_alt_consistency_def by simp }

{ fix P :: ‹('a, 'b) form› and x
assume ‹∀a ∈ S. x ∉ params a› and ‹Neg (Forall P) ∈ S›
moreover have ‹psubst f (Neg (Forall P)) ∈ ?S'›
using calculation by blast
then have ‹∃y. ?S' ∪ {Neg (psubst f P[App y []/0])} ∈ C›
using conc sc by (simp add: consistency_def)
then obtain y where ‹?S' ∪ {Neg (psubst f P[App y []/0])} ∈ C›
by blast

moreover have ‹psubst (f(x := y))  S = ?S'›
using calculation by (simp cong add: image_cong)
moreover have ‹psubst (f(x := y)) 
S ∪ {Neg (psubst (f(x := y)) P[App ((f(x := y)) x) []/0])} ∈ C›
using calculation by auto
ultimately have ‹∃f. psubst f  S ∪ {Neg (psubst f P[App (f x) []/0])} ∈ C›
by blast
then show ‹S ∪ {Neg (P[App x []/0])} ∈ ?C'›
unfolding mk_alt_consistency_def by simp }
qed

theorem mk_alt_consistency_subset: ‹C ⊆ mk_alt_consistency C›
unfolding mk_alt_consistency_def
proof
fix x assume ‹x ∈ C›
then have ‹psubst id  x ∈ C›
by simp
then have ‹(∃f. psubst f  x ∈ C)›
by blast
then show ‹x ∈ {S. ∃f. psubst f  S ∈ C}›
by simp
qed

subsection ‹Closure under subsets›

text ‹
\label{sec:closure}
We now show that a consistency property can be extended to one
that is closed under subsets.
›

definition close :: ‹('a, 'b) form set set ⇒ ('a, 'b) form set set› where
‹close C = {S. ∃S' ∈ C. S ⊆ S'}›

definition subset_closed :: ‹'a set set ⇒ bool› where
‹subset_closed C = (∀S' ∈ C. ∀S. S ⊆ S' ⟶ S ∈ C)›

lemma subset_in_close:
assumes ‹S ⊆ S'›
shows ‹S' ∪ x ∈ C ⟶ S ∪ x ∈ close C›
proof -
have ‹S' ∪ x ∈ close C ⟶ S ∪ x ∈ close C›
unfolding close_def using ‹S ⊆ S'› by blast
then show ?thesis unfolding close_def by blast
qed

theorem close_consistency:
assumes conc: ‹consistency C›
shows ‹consistency (close C)›
unfolding consistency_def
proof (intro allI impI conjI)
fix S
assume ‹S ∈ close C›
then obtain x where ‹x ∈ C› and ‹S ⊆ x›
unfolding close_def by blast

{ fix p ts
have ‹¬ (Pred p ts ∈ x ∧ Neg (Pred p ts) ∈ x)›
using ‹x ∈ C› conc unfolding consistency_def by simp
then show ‹¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)›
using ‹S ⊆ x› by blast }

{ have ‹FF ∉ x›
using ‹x ∈ C› conc unfolding consistency_def by blast
then show ‹FF ∉ S›
using ‹S ⊆ x› by blast }

{ have ‹Neg TT ∉ x›
using ‹x ∈ C› conc unfolding consistency_def by blast
then show ‹Neg TT ∉ S›
using ‹S ⊆ x› by blast }

{ fix Z
assume ‹Neg (Neg Z) ∈ S›
then have ‹Neg (Neg Z) ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {Z} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by simp
then show ‹S ∪ {Z} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix A B
assume ‹And A B ∈ S›
then have ‹And A B ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {A, B} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by simp
then show ‹S ∪ {A, B} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix A B
assume ‹Neg (Or A B) ∈ S›
then have ‹Neg (Or A B) ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {Neg A, Neg B} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by simp
then show ‹S ∪ {Neg A, Neg B} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix A B
assume ‹Or A B ∈ S›
then have ‹Or A B ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {A} ∈ C ∨ x ∪ {B} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by simp
then show ‹S ∪ {A} ∈ close C ∨ S ∪ {B} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix A B
assume ‹Neg (And A B) ∈ S›
then have ‹Neg (And A B) ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {Neg A} ∈ C ∨ x ∪ {Neg B} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by simp
then show ‹S ∪ {Neg A} ∈ close C ∨ S ∪ {Neg B} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix A B
assume ‹Impl A B ∈ S›
then have ‹Impl A B ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {Neg A} ∈ C ∨ x ∪ {B} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by simp
then show ‹S ∪ {Neg A} ∈ close C ∨ S ∪ {B} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix A B
assume ‹Neg (Impl A B) ∈ S›
then have ‹Neg (Impl A B) ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {A, Neg B} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by blast
then show ‹S ∪ {A, Neg B} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix P and t :: ‹'a term›
assume ‹closedt 0 t› and ‹Forall P ∈ S›
then have ‹Forall P ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {P[t/0]} ∈ C›
using ‹closedt 0 t› ‹x ∈ C› conc unfolding consistency_def by blast
then show ‹S ∪ {P[t/0]} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix P and t :: ‹'a term›
assume ‹closedt 0 t› and ‹Neg (Exists P) ∈ S›
then have ‹Neg (Exists P) ∈ x›
using ‹S ⊆ x› by blast
then have ‹x ∪ {Neg (P[t/0])} ∈ C›
using ‹closedt 0 t› ‹x ∈ C› conc unfolding consistency_def by blast
then show ‹S ∪ {Neg (P[t/0])} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix P
assume ‹Exists P ∈ S›
then have ‹Exists P ∈ x›
using ‹S ⊆ x› by blast
then have ‹∃c. x ∪ {P[App c []/0]} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by blast
then show ‹∃c. S ∪ {P[App c []/0]} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }

{ fix P
assume ‹Neg (Forall P) ∈ S›
then have ‹Neg (Forall P) ∈ x›
using ‹S ⊆ x› by blast
then have ‹∃c. x ∪ {Neg (P[App c []/0])} ∈ C›
using ‹x ∈ C› conc unfolding consistency_def by simp
then show ‹∃c. S ∪ {Neg (P[App c []/0])} ∈ close C›
using ‹S ⊆ x› subset_in_close by blast }
qed

theorem close_closed: ‹subset_closed (close C)›
unfolding close_def subset_closed_def by blast

theorem close_subset: ‹C ⊆ close C›
unfolding close_def by blast

text ‹
If a consistency property ‹C› is closed under subsets, so is the
corresponding alternative consistency property:
›

theorem mk_alt_consistency_closed:
assumes ‹subset_closed C›
shows ‹subset_closed (mk_alt_consistency C)›
unfolding subset_closed_def mk_alt_consistency_def
proof (intro ballI allI impI)
fix S S' :: ‹('a, 'b) form set›
assume ‹S ⊆ S'› and ‹S' ∈ {S. ∃f. psubst f  S ∈ C}›
then obtain f where *: ‹psubst f  S' ∈ C›
by blast
moreover have ‹psubst f  S ⊆ psubst f  S'›
using ‹S ⊆ S'› by blast
moreover have ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
using ‹subset_closed C› unfolding subset_closed_def by blast
ultimately have ‹psubst f  S ∈ C›
by blast
then show ‹S ∈ {S. ∃f. psubst f  S ∈ C}›
by blast
qed

subsection ‹Finite character›

text ‹
\label{sec:finiteness}
In this section, we show that an alternative consistency property can
be extended to one of finite character. A set of sets ‹C› is said
to be of finite character, provided that ‹S› is a member of ‹C›
if and only if every subset of ‹S› is.
›

definition finite_char :: ‹'a set set ⇒ bool› where
‹finite_char C = (∀S. S ∈ C = (∀S'. finite S' ⟶ S' ⊆ S ⟶ S' ∈ C))›

definition mk_finite_char :: ‹'a set set ⇒ 'a set set› where
‹mk_finite_char C = {S. ∀S'. S' ⊆ S ⟶ finite S' ⟶ S' ∈ C}›

theorem finite_alt_consistency:
assumes altconc: ‹alt_consistency C›
and ‹subset_closed C›
shows ‹alt_consistency (mk_finite_char C)›
unfolding alt_consistency_def
proof (intro allI impI conjI)
fix S
assume ‹S ∈ mk_finite_char C›
then have finc: ‹∀S' ⊆ S. finite S' ⟶ S' ∈ C›
unfolding mk_finite_char_def by blast

have ‹∀S' ∈ C. ∀S ⊆ S'. S ∈ C›
using ‹subset_closed C› unfolding subset_closed_def by blast
then have sc: ‹∀S' x. S' ∪ x ∈ C ⟶ (∀S ⊆ S' ∪ x. S ∈ C)›
by blast

{ fix p ts
show ‹¬ (Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S)›
proof
assume ‹Pred p ts ∈ S ∧ Neg (Pred p ts) ∈ S›
then have ‹{Pred p ts, Neg (Pred p ts)} ∈ C›
using finc by simp
then show False
using altconc unfolding alt_consistency_def by fast
qed }

show ‹FF ∉ S›
proof
assume ‹FF ∈ S›
then have ‹{FF} ∈ C›
using finc by simp
then show False
using altconc unfolding alt_consistency_def by fast
qed

show ‹Neg TT ∉ S›
proof
assume ‹Neg TT ∈ S›
then have ‹{Neg TT} ∈ C›
using finc by simp
then show False
using altconc unfolding alt_consistency_def by fast
qed

{ fix Z
assume *: ‹Neg (Neg Z) ∈ S›
show ‹S ∪ {Z} ∈ mk_finite_char C›
unfolding mk_finite_char_def
proof (intro allI impI CollectI)
fix S'
let ?S' = ‹S' - {Z} ∪ {Neg (Neg Z)}›

assume ‹S' ⊆ S ∪ {Z}› and ‹finite S'›
then have ‹?S' ⊆ S›
using * by blast
moreover have ‹finite ?S'›
using ‹finite S'› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {Z} ∈ C›
using altconc unfolding alt_consistency_def by simp
then show ‹S' ∈ C›
using sc by blast
qed }

{ fix A B
assume *: ‹And A B ∈ S›
show ‹S ∪ {A, B} ∈ mk_finite_char C›
unfolding mk_finite_char_def
proof (intro allI impI CollectI)
fix S'
let ?S' = ‹S' - {A, B} ∪ {And A B}›

assume ‹S' ⊆ S ∪ {A, B}› and ‹finite S'›
then have ‹?S' ⊆ S›
using * by blast
moreover have ‹finite ?S'›
using ‹finite S'› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {A, B} ∈ C›
using altconc unfolding alt_consistency_def by simp
then show ‹S' ∈ C›
using sc by blast
qed }

{ fix A B
assume *: ‹Neg (Or A B) ∈ S›
show ‹S ∪ {Neg A, Neg B} ∈ mk_finite_char C›
unfolding mk_finite_char_def
proof (intro allI impI CollectI)
fix S'
let ?S' = ‹S' - {Neg A, Neg B} ∪ {Neg (Or A B)}›

assume ‹S' ⊆ S ∪ {Neg A, Neg B}› and ‹finite S'›
then have ‹?S' ⊆ S›
using * by blast
moreover have ‹finite ?S'›
using ‹finite S'› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {Neg A, Neg B} ∈ C›
using altconc unfolding alt_consistency_def by simp
then show ‹S' ∈ C›
using sc by blast
qed }

{ fix A B
assume *: ‹Neg (Impl A B) ∈ S›
show ‹S ∪ {A, Neg B} ∈ mk_finite_char C›
unfolding mk_finite_char_def
proof (intro allI impI CollectI)
fix S'
let ?S' = ‹S' - {A, Neg B} ∪ {Neg (Impl A B)}›

assume ‹S' ⊆ S ∪ {A, Neg B}› and ‹finite S'›
then have ‹?S' ⊆ S›
using * by blast
moreover have ‹finite ?S'›
using ‹finite S'› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {A, Neg B} ∈ C›
using altconc unfolding alt_consistency_def by simp
then show ‹S' ∈ C›
using sc by blast
qed }

{ fix A B
assume *: ‹Or A B ∈ S›
show ‹S ∪ {A} ∈ mk_finite_char C ∨ S ∪ {B} ∈ mk_finite_char C›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain Sa and Sb
where ‹Sa ⊆ S ∪ {A}› and ‹finite Sa› and ‹Sa ∉ C›
and ‹Sb ⊆ S ∪ {B}› and ‹finite Sb› and ‹Sb ∉ C›
unfolding mk_finite_char_def by blast

let ?S' = ‹(Sa - {A}) ∪ (Sb - {B}) ∪ {Or A B}›

have ‹?S' ⊆ S›
using ‹Sa ⊆ S ∪ {A}› ‹Sb ⊆ S ∪ {B}› * by blast
moreover have ‹finite ?S'›
using ‹finite Sa› ‹finite Sb› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {A} ∈ C ∨ ?S' ∪ {B} ∈ C›
using altconc unfolding alt_consistency_def by simp
then have ‹Sa ∈ C ∨ Sb ∈ C›
using sc by blast
then show False
using ‹Sa ∉ C› ‹Sb ∉ C› by blast
qed }

{ fix A B
assume *: ‹Neg (And A B) ∈ S›
show ‹S ∪ {Neg A} ∈ mk_finite_char C ∨ S ∪ {Neg B} ∈ mk_finite_char C›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain Sa and Sb
where ‹Sa ⊆ S ∪ {Neg A}› and ‹finite Sa› and ‹Sa ∉ C›
and ‹Sb ⊆ S ∪ {Neg B}› and ‹finite Sb› and ‹Sb ∉ C›
unfolding mk_finite_char_def by blast

let ?S' = ‹(Sa - {Neg A}) ∪ (Sb - {Neg B}) ∪ {Neg (And A B)}›

have ‹?S' ⊆ S›
using ‹Sa ⊆ S ∪ {Neg A}› ‹Sb ⊆ S ∪ {Neg B}› * by blast
moreover have ‹finite ?S'›
using ‹finite Sa› ‹finite Sb› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {Neg A} ∈ C ∨ ?S' ∪ {Neg B} ∈ C›
using altconc unfolding alt_consistency_def by simp
then have ‹Sa ∈ C ∨ Sb ∈ C›
using sc by blast
then show False
using ‹Sa ∉ C› ‹Sb ∉ C› by blast
qed }

{ fix A B
assume *: ‹Impl A B ∈ S›
show ‹S ∪ {Neg A} ∈ mk_finite_char C ∨ S ∪ {B} ∈ mk_finite_char C›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain Sa and Sb
where ‹Sa ⊆ S ∪ {Neg A}› and ‹finite Sa› and ‹Sa ∉ C›
and ‹Sb ⊆ S ∪ {B}› and ‹finite Sb› and ‹Sb ∉ C›
unfolding mk_finite_char_def by blast

let ?S' = ‹(Sa - {Neg A}) ∪ (Sb - {B}) ∪ {Impl A B}›

have ‹?S' ⊆ S›
using ‹Sa ⊆ S ∪ {Neg A}› ‹Sb ⊆ S ∪ {B}› * by blast
moreover have ‹finite ?S'›
using ‹finite Sa› ‹finite Sb› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {Neg A} ∈ C ∨ ?S' ∪ {B} ∈ C›
using altconc unfolding alt_consistency_def by simp
then have ‹Sa ∈ C ∨ Sb ∈ C›
using sc by blast
then show False
using ‹Sa ∉ C› ‹Sb ∉ C› by blast
qed }

{ fix P and t :: ‹'a term›
assume *: ‹Forall P ∈ S› and ‹closedt 0 t›
show ‹S ∪ {P[t/0]} ∈ mk_finite_char C›
unfolding mk_finite_char_def
proof (intro allI impI CollectI)
fix S'
let ?S' = ‹S' - {P[t/0]} ∪ {Forall P}›

assume ‹S' ⊆ S ∪ {P[t/0]}› and ‹finite S'›
then have ‹?S' ⊆ S›
using * by blast
moreover have ‹finite ?S'›
using ‹finite S'› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {P[t/0]} ∈ C›
using altconc ‹closedt 0 t› unfolding alt_consistency_def by simp
then show ‹S' ∈ C›
using sc by blast
qed }

{ fix P and t :: ‹'a term›
assume *: ‹Neg (Exists P) ∈ S› and ‹closedt 0 t›
show ‹S ∪ {Neg (P[t/0])} ∈ mk_finite_char C›
unfolding mk_finite_char_def
proof (intro allI impI CollectI)
fix S'
let ?S' = ‹S' - {Neg (P[t/0])} ∪ {Neg (Exists P)}›

assume ‹S' ⊆ S ∪ {Neg (P[t/0])}› and ‹finite S'›
then have ‹?S' ⊆ S›
using * by blast
moreover have ‹finite ?S'›
using ‹finite S'› by blast
ultimately have ‹?S' ∈ C›
using finc by blast
then have ‹?S' ∪ {Neg