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 by (metis (no_types, lifting) add.right_neutral add_Suc_right fm.size(12) in_measure lessI) 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 by (metis (no_types, lifting) add.right_neutral add_Suc_right fm.size(12) in_measure lessI) 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 by (metis (no_types, lifting) add.right_neutral add_Suc_right fm.size(13) in_measure lessI) 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 by (metis (no_types, lifting) Nat.add_0_right add_Suc_right fm.size(13) in_measure lessI) 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