section ‹Completeness› theory Completeness imports Countermodel EPathHintikka begin text ‹In this theory, we prove that the prover is complete with regards to the SeCaV proof system using the abstract completeness framework.› text ‹We start out by specializing the abstract completeness theorem to our prover. It is necessary to reproduce the final theorem here so we can alter it to state that our prover produces a proof tree instead of simply stating that a proof tree exists.› theorem epath_prover_completeness: fixes A :: ‹tm list› and z :: ‹fm list› defines ‹t ≡ secavProver (A, z)› shows ‹(fst (root t) = (A, z) ∧ wf t ∧ tfinite t) ∨ (∃ steps. fst (shd steps) = (A, z) ∧ epath steps ∧ Saturated steps)› (is ‹?A ∨ ?B›) proof - { assume ‹¬ ?A› with assms have ‹¬ tfinite (mkTree rules (A, z))› unfolding secavProver_def using wf_mkTree fair_rules by simp then obtain steps where ‹ipath (mkTree rules (A, z)) steps› using Konig by blast with assms have ‹fst (shd steps) = (A, z) ∧ epath steps ∧ Saturated steps› by (metis UNIV_I fair_rules ipath.cases ipath_mkTree_Saturated mkTree.simps(1) prod.sel(1) wf_ipath_epath wf_mkTree) then have ?B by blast } then show ?thesis by blast qed text ‹This is an abbreviation for validity under our bounded semantics (for well-formed interpretations).› abbreviation ‹uvalid z ≡ ∀u (e :: nat ⇒ tm) f g. is_env u e ⟶ is_fdenot u f ⟶ (∃p ∈ set z. usemantics u e f g p)› text ‹The sequent in the first state of a saturated escape path is not valid. This follows from our results in the theories EPathHintikka and Countermodel.› lemma epath_countermodel: assumes ‹fst (shd steps) = (A, z)› and ‹epath steps› and ‹Saturated steps› shows ‹¬ uvalid z› proof assume ‹uvalid z› moreover have ‹Hintikka (tree_fms steps)› (is ‹Hintikka ?S›) using assms escape_path_Hintikka assms by simp moreover have ‹∀p ∈ set z. p ∈ tree_fms steps› using assms shd_sset by (metis Pair_inject prod.collapse pseq_def pseq_in_tree_fms) then have ‹∃g. ∀p ∈ set z. ¬ usemantics (terms ?S) (E ?S) (F ?S) g p› using calculation(2) Hintikka_counter_model assms by blast moreover have ‹is_env (terms ?S) (E ?S)› ‹is_fdenot (terms ?S) (F ?S)› using is_env_E is_fdenot_F by blast+ ultimately show False by blast qed text ‹Combining the results above, we can prove completeness with regards to our bounded semantics: if a sequent is valid under our bounded semantics, the prover will produce a finite, well-formed proof tree with the sequent at its root.› theorem prover_completeness_usemantics: fixes A :: ‹tm list› assumes ‹uvalid z› defines ‹t ≡ secavProver (A, z)› shows ‹fst (root t) = (A, z) ∧ wf t ∧ tfinite t› using assms epath_prover_completeness epath_countermodel by blast text ‹Since our bounded semantics are sound, we can derive our main completeness theorem as a corollary: if a sequent is provable in the SeCaV proof system, the prover will produce a finite, well-formed proof tree with the sequent at its root.› corollary prover_completeness_SeCaV: fixes A :: ‹tm list› assumes ‹⊩ z› defines ‹t ≡ secavProver (A, z)› shows ‹fst (root t) = (A, z) ∧ wf t ∧ tfinite t› proof - have ‹uvalid z› using assms sound_usemantics by blast then show ?thesis using assms prover_completeness_usemantics by blast qed end