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
    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
  ei:a = (λj. if j < i then e j else if j = i then a else e (j - 1))

lemma shift_eq [simp]: i = j  (ei:T) j = T
  by (simp add: shift_def)

lemma shift_gt [simp]: j < i  (ei:T) j = e j
  by (simp add: shift_def)

lemma shift_lt [simp]: i < j  (ei:T) j = e (j - 1)
  by (simp add: shift_def)

lemma shift_commute [simp]: ei:U0:T = e0:TSuc i:U
proof
  fix x
  show (ei:U0:T) x = (e0:TSuc 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 (e0:z) f g p)
| eval e f g (Exists p) = (z. eval (e0: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 (ei:evalt e f u) f t
  evalts e f (substts ts u i) = evalts (ei:evalt e f u) f ts
  by (induct t and ts rule: substt.induct substts.induct) simp_all

theorem lift_lemma [simp]:
  evalt (e0:z) f (liftt t) = evalt e f t
  evalts (e0: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 (ei: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 (e0: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 (e0: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 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