Theory FOL-Fitting.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
    See also the Natural Deduction Assistant: https://nadea.compute.dtu.dk/
*)

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›
  by (simp add: shift_def)

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

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

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›
    by (simp add: Assum)
  moreover { have ‹[Pred p [], Neg ?or] ⊢ Neg ?or›
      by (simp add: Assum)
    moreover have ‹[Pred p [], Neg ?or] ⊢ Pred p []›
      by (simp add: Assum)
    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›
    by (simp add: Assum)
  moreover { have ‹[?forall[App 1 []/0], Exists ?forall] ⊢ Forall (Pred p [App 1 [], Var 0])›
      by (simp add: Assum)
    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]›
      by (simp add: Assum)
    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)›
    by (simp add: Assum)
  moreover have ‹Pred P [App 0 []] # ?G ⊢ Neg (Pred P [App 0 []])›
    and ‹Pred P [App 0 []] # ?G ⊢ Pred P [App 0 []]›
    by (simp_all add: Assum)
  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›
    by (simp add: Assum)
  moreover { have ‹[Pred P [], ?PQP, Neg ?PQPP] ⊢ Neg ?PQPP›
      by (simp add: Assum)
    moreover have ‹[?PQP, Pred P [], ?PQP, Neg ?PQPP] ⊢ Pred P []›
      by (simp add: Assum)
    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
qed (simp_all add: model_def, blast+)

section ‹Completeness›

text ‹
The goal of this section is to prove completeness of the natural deduction
calculus introduced in \secref{sec:proof-calculus}. Before we start with the
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