# Theory Example_Propositional_SC

```(*
Title:  Example Completeness Proof for a Propositional Sequent Calculus
Author: Asta Halkjær From
*)

chapter ‹Example: Propositional Sequent Calculus›

theory Example_Propositional_SC imports Derivations begin

section ‹Syntax›

datatype 'p fm
= Fls (‹❙⊥›)
| Pro 'p (‹❙‡›)
| Imp ‹'p fm› ‹'p fm› (infixr ‹❙⟶› 55)

abbreviation Neg (‹❙¬ _› [70] 70) where ‹❙¬ p ≡ p ❙⟶ ❙⊥›

section ‹Semantics›

type_synonym 'p model = ‹'p ⇒ bool›

fun semantics :: ‹'p model ⇒ 'p fm ⇒ bool› (‹⟦_⟧›) where
‹⟦_⟧ ❙⊥ ⟷ False›
| ‹⟦I⟧ (❙‡P) ⟷ I P›
| ‹⟦I⟧ (p ❙⟶ q) ⟷ ⟦I⟧ p ⟶ ⟦I⟧ q›

section ‹Calculus›

inductive Calculus :: ‹'p fm list ⇒ 'p fm list ⇒ bool› (‹_ ⊢⇩S _› [50, 50] 50) where
Axiom [intro]: ‹p # A ⊢⇩S p # B›
| FlsL [intro]: ‹❙⊥ # A ⊢⇩S B›
| FlsR [dest]: ‹A ⊢⇩S ❙⊥ # B ⟹ A ⊢⇩S B›
| ImpL [intro]: ‹A ⊢⇩S p # B ⟹ q # A ⊢⇩S B ⟹ (p ❙⟶ q) # A ⊢⇩S B›
| ImpR [intro]: ‹p # A ⊢⇩S q # B ⟹ A ⊢⇩S (p ❙⟶ q) # B›
| Cut [elim]: ‹A ⊢⇩S p # B ⟹ p # C ⊢⇩S D ⟹ A @ C ⊢⇩S B @ D›
| WeakenL: ‹A ⊢⇩S B ⟹ set A ⊆ set A' ⟹ A' ⊢⇩S B›
| WeakenR: ‹A ⊢⇩S B ⟹ set B ⊆ set B' ⟹ A ⊢⇩S B'›

lemma Boole: ‹❙¬ p # A ⊢⇩S [] ⟹ A ⊢⇩S [p]›
by (metis Axiom Cut ImpR WeakenR append_self_conv2 self_append_conv set_subset_Cons)

section ‹Soundness›

theorem soundness: ‹A ⊢⇩S B ⟹ ∀q ∈ set A. ⟦I⟧ q ⟹ ∃p ∈ set B. ⟦I⟧ p›
by (induct A B rule: Calculus.induct) auto

corollary soundness': ‹[] ⊢⇩S [p] ⟹ ⟦I⟧ p›
using soundness by fastforce

corollary ‹¬ ([] ⊢⇩S [])›
using soundness by fastforce

section ‹Maximal Consistent Sets›

definition consistent :: ‹'p fm set ⇒ bool› where
‹consistent S ≡ ∄S'. set S' ⊆ S ∧ S' ⊢⇩S [❙⊥]›

interpretation MCS_No_Saturation consistent
proof
fix S S' :: ‹'p fm set›
assume ‹consistent S› ‹S' ⊆ S›
then show ‹consistent S'›
unfolding consistent_def by fast
next
fix S :: ‹'p fm set›
assume ‹¬ consistent S›
then show ‹∃S'⊆S. finite S' ∧ ¬ consistent S'›
unfolding consistent_def by blast
next
show ‹infinite (UNIV :: 'p fm set)›
using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
qed

interpretation Derivations_MCS_Cut ‹λA p. A ⊢⇩S [p]› consistent ‹❙⊥›
proof
fix A B and p :: ‹'p fm›
assume ‹A ⊢⇩S [p]› ‹set A ⊆ set B›
then show ‹B ⊢⇩S [p]›
using WeakenL by blast
next
fix S :: ‹'p fm set›
show ‹consistent S ⟷ (∄S'. set S' ⊆ S ∧ S' ⊢⇩S [❙⊥])›
unfolding consistent_def ..
next
fix A and p :: ‹'p fm›
assume ‹p ∈ set A›
then show ‹A ⊢⇩S [p]›
by (metis Axiom WeakenL set_ConsD subsetI)
next
fix A B and p q :: ‹'p fm›
assume ‹A ⊢⇩S [p]› ‹p # B ⊢⇩S [q]›
then show ‹A @ B ⊢⇩S [q]›
using Cut by fastforce
qed

section ‹Truth Lemma›

abbreviation hmodel :: ‹'p fm set ⇒ 'p model› where
‹hmodel H ≡ λP. ❙‡P ∈ H›

fun semics :: ‹'p model ⇒ ('p model ⇒ 'p fm ⇒ bool) ⇒ 'p fm ⇒ bool› where
‹semics _ _ ❙⊥ ⟷ False›
| ‹semics I _ (❙‡P) ⟷ I P›
| ‹semics I rel (p ❙⟶ q) ⟷ rel I p ⟶ rel I q›

fun rel :: ‹'p fm set ⇒ 'p model ⇒ 'p fm ⇒ bool› where
‹rel H _ p = (p ∈ H)›

theorem Hintikka_model':
assumes ‹⋀p. semics (hmodel H) (rel H) p ⟷ p ∈ H›
shows ‹p ∈ H ⟷ ⟦hmodel H⟧ p›
proof (induct p rule: wf_induct[where r=‹measure size›])
case 1
then show ?case ..
next
case (2 x)
then show ?case
using assms[of x] by (cases x) simp_all
qed

lemma Hintikka_Extend:
assumes ‹consistent H› ‹maximal H›
shows ‹semics (hmodel H) (rel H) p ⟷ p ∈ H›
proof (cases p)
case Fls
have ‹❙⊥ ∉ H›
using assms MCS_derive consistent_def by blast
then show ?thesis
using Fls by simp
next
case (Imp p q)
have ‹A ⊢⇩S [q] ⟹ A ⊢⇩S [p ❙⟶ q]› for A
by (meson ImpR WeakenL set_subset_Cons)
moreover have ‹p # A ⊢⇩S [❙⊥] ⟹ A ⊢⇩S [p ❙⟶ q]› for A
by (meson FlsR ImpR WeakenR set_subset_Cons)
moreover have ‹A ⊢⇩S [p ❙⟶ q] ⟹ B ⊢⇩S [p] ⟹ A @ B ⊢⇩S [q]› for A B
using Cut by (metis Axiom ImpL append_Nil append_Nil2)
ultimately have ‹(p ∈ H ⟶ q ∈ H) ⟷ p ❙⟶ q ∈ H›
using assms MCS_derive MCS_derive_fls Axiom
by (metis append_Cons append_Nil insert_subset list.simps(15))
then show ?thesis
using Imp by simp
qed simp

interpretation Truth_No_Saturation consistent semics semantics ‹λH. {hmodel H}› rel
proof
fix p and M :: ‹'p model›
show ‹⟦M⟧ p ⟷ semics M semantics p›
by (induct p) auto
next
fix p and H :: ‹'p fm set› and M :: ‹'p model›
assume ‹∀M ∈ {hmodel H}. ∀p. semics M (rel H) p ⟷ rel H M p› ‹M ∈ {hmodel H}›
then show ‹⟦M⟧ p ⟷ rel H M p›
using Hintikka_model' by auto
next
fix H :: ‹'p fm set›
assume ‹consistent H› ‹maximal H›
then show ‹∀M ∈ {hmodel H}. ∀p. semics M (rel H) p ⟷ rel H M p›
using Hintikka_Extend by auto
qed

section ‹Completeness›

theorem strong_completeness:
assumes ‹∀M :: 'p model. (∀q ∈ X. ⟦M⟧ q) ⟶ ⟦M⟧ p›
shows ‹∃A. set A ⊆ X ∧ A ⊢⇩S [p]›
proof (rule ccontr)
assume ‹∄A. set A ⊆ X ∧ A ⊢⇩S [p]›
then have ‹∄A. set A ⊆ X ∧ ❙¬ p # A ⊢⇩S []›
using Boole by blast
then have ‹∄A. set A ⊆ X ∧ ❙¬ p # A ⊢⇩S [❙⊥]›
by fast
then have *: ‹∄A. set A ⊆ {❙¬ p} ∪ X ∧ A ⊢⇩S [❙⊥]›
using derive_split1 by blast

let ?S = ‹{❙¬ p} ∪ X›
let ?H = ‹Extend ?S›

have ‹consistent ?S›
unfolding consistent_def using * by blast
then have ‹consistent ?H› ‹maximal ?H›
using MCS_Extend' by blast+
then have ‹p ∈ ?H ⟷ ⟦hmodel ?H⟧ p› for p
using truth_lemma_no_saturation by fastforce
then have ‹p ∈ ?S ⟶ ⟦hmodel ?H⟧ p› for p
using Extend_subset by blast
then have ‹⟦hmodel ?H⟧ (❙¬ p)› ‹∀q ∈ X. ⟦hmodel ?H⟧ q›
by blast+
moreover from this have ‹⟦hmodel ?H⟧ p›
using assms(1) by blast
ultimately show False
by simp
qed

abbreviation valid :: ‹'p fm ⇒ bool› where
‹valid p ≡ ∀M. ⟦M⟧ p›

theorem completeness:
assumes ‹valid p›
shows ‹[] ⊢⇩S [p]›
using assms strong_completeness[where X=‹{}›] by auto

theorem main: ‹valid p ⟷ [] ⊢⇩S [p]›
using completeness soundness' by blast

end
```