# Theory Countermodel

```section ‹Countermodels from Hintikka sets›

theory Countermodel
imports Hintikka Usemantics ProverLemmas
begin

text ‹In this theory, we will construct a countermodel in the bounded semantics from a Hintikka
set. This will allow us to prove completeness of the prover.›

text ‹A predicate is satisfied in the model based on a set of formulas S when its negation is in S.›
abbreviation (input)
‹G S n ts ≡ Neg (Pre n ts) ∈ S›

text ‹Alternate interpretation for environments: if a variable is not present, we interpret it as
some existing term.›
abbreviation
‹E S n ≡ if Var n ∈ terms S then Var n else SOME t. t ∈ terms S›

text ‹Alternate interpretation for functions: if a function application is not present, we interpret
it as some existing term.›
abbreviation
‹F S i l ≡ if Fun i l ∈ terms S then Fun i l else SOME t. t ∈ terms S›

text ‹The terms function never returns the empty set (because it will add ‹Fun 0 []› if that is the
case).›
lemma terms_ne [simp]: ‹terms S ≠ {}›
unfolding terms_def by simp

text ‹If a term is in the set of terms, it is either the default term or a subterm of some formula
in the set.›
lemma terms_cases: ‹t ∈ terms S ⟹ t = Fun 0 [] ∨ (∃p ∈ S. t ∈ set (subtermFm p))›
unfolding terms_def by (simp split: if_splits)

text ‹The set of terms is downwards closed under the subterm function.›
lemma terms_downwards_closed: ‹t ∈ terms S ⟹ set (subtermTm t) ⊆ terms S›
proof (induct t)
case (Fun n ts)
moreover have ‹∀t ∈ set ts. t ∈ set ts›
by simp
moreover have ‹∀t ∈ set ts. t ∈ terms S›
proof
fix t
assume *: ‹t ∈ set ts›
then show ‹t ∈ terms S›
proof (cases ‹terms S = {Fun 0 []}›)
case True
then show ?thesis
using Fun * by simp
next
case False
moreover obtain p where p: ‹p ∈ S› ‹Fun n ts ∈ set (subtermFm p)›
using Fun(2) terms_cases * by fastforce
then have ‹set ts ⊆ set (subtermFm p)›
using fun_arguments_subterm by blast
ultimately show ‹t ∈ terms S›
unfolding terms_def using * p(1) by (metis UN_iff in_mono)
qed
qed
ultimately have ‹∀t ∈ set ts. set (subtermTm t) ⊆ terms S›
using Fun by meson
moreover note ‹Fun n ts ∈ terms S›
ultimately show ?case
by auto
next
case (Var x)
then show ?case
by simp
qed

text ‹If terms are actually in a set of formulas, interpreting the environment over these formulas
allows for a Herbrand interpretation.›
lemma usemantics_E:
‹t ∈ terms S ⟹ semantics_term (E S) (F S) t = t›
‹list_all (λt. t ∈ terms S) ts ⟹ semantics_list (E S) (F S) ts = ts›
proof (induct t and ts arbitrary: ts rule: semantics_term.induct semantics_list.induct)
case (Fun i ts')
moreover have ‹∀t' ∈ set ts'. t' ∈ set (subtermTm (Fun i ts'))›
using subterm_Fun_refl by blast
ultimately have ‹list_all (λt. t ∈ terms S) ts'›
using terms_downwards_closed unfolding list_all_def by (metis (no_types, lifting) subsetD)
then show ?case
using Fun by simp
qed simp_all

text ‹Our alternate interpretation of environments is well-formed for the terms function.›
lemma is_env_E:
‹is_env (terms S) (E S)›
unfolding is_env_def
proof
fix n
show ‹E S n ∈ terms S›
by (cases ‹Var n ∈ terms S›) (simp_all add: some_in_eq)
qed

text ‹Our alternate function interpretation is well-formed for the terms function.›
lemma is_fdenot_F:
‹is_fdenot (terms S) (F S)›
unfolding is_fdenot_def
proof (intro allI impI)
fix i l
assume ‹list_all (λx. x ∈ terms S) l›
then show ‹F S i l ∈ terms S›
by (cases ‹∀n. Var n ∈ terms S›) (simp_all add: some_in_eq)
qed

abbreviation
‹M S ≡ usemantics (terms S) (E S) (F S) (G S)›

text ‹If S is a Hintikka set, then we can construct a countermodel for any formula using our
bounded semantics and a Herbrand interpretation.›
theorem Hintikka_counter_model:
assumes ‹Hintikka S›
shows ‹(p ∈ S ⟶ ¬ M S p) ∧ (Neg p ∈ S ⟶ M S p)›
proof (induct p rule: wf_induct [where r=‹measure size›])
case 1
then show ?case ..
next
fix x
assume wf: ‹∀q. (q, x) ∈ measure size ⟶
(q ∈ S ⟶ ¬ M S q) ∧ (Neg q ∈ S ⟶ M S q)›
show ‹(x ∈ S ⟶ ¬ M S x) ∧ (Neg x ∈ S ⟶ M S x)›
proof (cases x)
case (Pre n ts)
show ?thesis
proof (intro conjI impI)
assume ‹x ∈ S›
then have ‹Neg (Pre n ts) ∉ S›
using assms Pre Hintikka.Basic by blast
moreover have ‹list_all (λt. t ∈ terms S) ts›
using ‹x ∈ S› Pre subterm_Pre_refl unfolding terms_def list_all_def by force
ultimately show ‹¬ M S x›
using Pre usemantics_E
by (metis (no_types, lifting) usemantics.simps(1))
next
assume ‹Neg x ∈ S›
then have ‹G S n ts›
using assms Pre Hintikka.Basic by blast
moreover have ‹list_all (λt. t ∈ terms S) ts›
using ‹Neg x ∈ S› Pre subterm_Pre_refl unfolding terms_def list_all_def by force
ultimately show ‹M S x›
using Pre usemantics_E
by (metis (no_types, lifting) usemantics.simps(1))
qed
next
case (Imp p q)
show ?thesis
proof (intro conjI impI)
assume ‹x ∈ S›
then have ‹Neg p ∈ S› ‹q ∈ S›
using Imp assms Hintikka.AlphaImp by blast+
then show ‹¬ M S x›
using wf Imp by fastforce
next
assume ‹Neg x ∈ S›
then have ‹p ∈ S ∨ Neg q ∈ S›
using Imp assms Hintikka.BetaImp by blast
then show ‹M S x›
using wf Imp by fastforce
qed
next
case (Dis p q)
show ?thesis
proof (intro conjI impI)
assume ‹x ∈ S›
then have ‹p ∈ S› ‹q ∈ S›
using Dis assms Hintikka.AlphaDis by blast+
then show ‹¬ M S x›
using wf Dis by fastforce
next
assume ‹Neg x ∈ S›
then have ‹Neg p ∈ S ∨ Neg q ∈ S›
using Dis assms Hintikka.BetaDis by blast
then show ‹M S x›
using wf Dis by fastforce
qed
next
case (Con p q)
show ?thesis
proof (intro conjI impI)
assume ‹x ∈ S›
then have ‹p ∈ S ∨ q ∈ S›
using Con assms Hintikka.BetaCon by blast
then show ‹¬ M S x›
using wf Con by fastforce
next
assume ‹Neg x ∈ S›
then have ‹Neg p ∈ S› ‹Neg q ∈ S›
using Con assms Hintikka.AlphaCon by blast+
then show ‹M S x›
using wf Con by fastforce
qed
next
case (Exi p)
show ?thesis
proof (intro conjI impI)
assume ‹x ∈ S›
then have ‹∀t ∈ terms S. sub 0 t p ∈ S›
using Exi assms Hintikka.GammaExi by blast
then have ‹∀t ∈ terms S. ¬ M S (sub 0 t p)›
using wf Exi size_sub
moreover have ‹∀t ∈ terms S. semantics_term (E S) (F S) t = t›
using usemantics_E(1) terms_downwards_closed unfolding list_all_def by blast
ultimately have ‹∀t ∈ terms S. ¬ usemantics (terms S) (SeCaV.shift (E S) 0 t) (F S) (G S) p›
by simp
then show ‹¬ M S x›
using Exi by simp
next
assume ‹Neg x ∈ S›
then obtain t where ‹t ∈ terms S› ‹Neg (sub 0 t p) ∈ S›
using Exi assms Hintikka.DeltaExi by metis
then have ‹M S (sub 0 t p)›
using wf Exi size_sub
moreover have ‹semantics_term (E S) (F S) t = t›
using ‹t ∈ terms S› usemantics_E(1) terms_downwards_closed unfolding list_all_def by blast
ultimately show ‹M S x›
using Exi ‹t ∈ terms S› by auto
qed
next
case (Uni p)
show ?thesis
proof (intro conjI impI)
assume ‹x ∈ S›
then obtain t where ‹t ∈ terms S› ‹sub 0 t p ∈ S›
using Uni assms Hintikka.DeltaUni by metis
then have ‹¬ M S (sub 0 t p)›
using wf Uni size_sub
moreover have ‹semantics_term (E S) (F S) t = t›
using ‹t ∈ terms S› usemantics_E(1) terms_downwards_closed unfolding list_all_def by blast
ultimately show ‹¬ M S x›
using Uni ‹t ∈ terms S› by auto
next
assume ‹Neg x ∈ S›
then have ‹∀t ∈ terms S. Neg (sub 0 t p) ∈ S›
using Uni assms Hintikka.GammaUni by blast
then have ‹∀t ∈ terms S. M S (sub 0 t p)›
using wf Uni size_sub
moreover have ‹∀t ∈ terms S. semantics_term (E S) (F S) t = t›
using usemantics_E(1) terms_downwards_closed unfolding list_all_def by blast
ultimately have ‹∀t ∈ terms S. ¬ usemantics (terms S) (SeCaV.shift (E S) 0 t) (F S) (G S) (Neg p)›
by simp
then show ‹M S x›
using Uni by simp
qed
next
case (Neg p)
show ?thesis
proof (intro conjI impI)
assume ‹x ∈ S›
then show ‹¬ M S x›
using wf Neg by fastforce
next
assume ‹Neg x ∈ S›
then have ‹p ∈ S›
using Neg assms Hintikka.Neg by blast
then show ‹M S x›
using wf Neg by fastforce
qed
qed
qed

end
```