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
  fix S S' :: 'p fm set
  assume consistent S S'  S
  then show consistent S'
    unfolding consistent_def by fast
  fix S :: 'p fm set
  assume ¬ consistent S
  then show S'S. finite S'  ¬ consistent S'
    unfolding consistent_def by blast
  show infinite (UNIV :: 'p fm set)
    using infinite_UNIV_size[of λp. p  p] by simp

interpretation Derivations_MCS_Cut λA p. A S [p] consistent 
  fix A B and p :: 'p fm
  assume A S [p] set A  set B
  then show B S [p]
    using WeakenL by blast
  fix S :: 'p fm set
  show consistent S  (S'. set S'  S  S' S [])
    unfolding consistent_def ..
  fix A and p :: 'p fm
  assume p  set A
  then show A S [p]
    by (metis Axiom WeakenL set_ConsD subsetI)
  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

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 ..
  case (2 x)
  then show ?case
    using assms[of x] by (cases x) simp_all

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
  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
  fix p and M :: 'p model
  show M p  semics M semantics p
    by (induct p) auto
  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
  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

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

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