section \Propositional Logic - Soundness and Completeness\ text \ Soundness and completeness of a logic establish that the syntactic notion of provability is equivalent to the semantic notation of logical entailment. In this project you will formally prove soundness and completeness of a specific set of natural deduction rules for propositional logic. \ theory Project_Logic imports Main begin subsection \Syntax and Semantics\ text \ Propositional formulas are defined by the following data type (that comes with some syntactic sugar): \ type_synonym id = string datatype form = Atom id | Bot ("\\<^sub>p") | Neg form ("\\<^sub>p _" [68] 68) | Conj form form (infixr "\\<^sub>p" 67) | Disj form form (infixr "\\<^sub>p" 67) | Impl form form (infixr "\\<^sub>p" 66) text \ Define a function \eval\ that evaluates the truth value of a formula with respect to a given truth assignment. \ fun eval :: "(id \ bool) \ form \ bool" where "eval v \ \ undefined" text \ Using @{const eval}, define semantic entailment of a formula from a list of formulas. \ definition entails :: "form list \ form \ bool" (infix "\" 51) where "\ \ \ \ undefined" subsection \Natural Deduction\ text \ The natural deduction rules we consider are captured by the following inductive predicate \proves P \\, with infix syntax \P \ \\, that holds whenever a formula \\\ is provable from a list of premises \P\. \ inductive proves (infix "\" 58) where premise: "\ \ set P \ P \ \" | conjI: "P \ \ \ P \ \ \ P \ \ \\<^sub>p \" | conjE1: "P \ \ \\<^sub>p \ \ P \ \" | conjE2: "P \ \ \\<^sub>p \ \ P \ \" | impI: "\ # P \ \ \ P \ (\ \\<^sub>p \)" | impE: "P \ \ \ P \ \ \\<^sub>p \ \ P \ \" | disjI1: "P \ \ \ P \ \ \\<^sub>p \" | disjI2: "P \ \ \ P \ \ \\<^sub>p \" | disjE: "P \ \ \\<^sub>p \ \ \ # P \ \ \ \ # P \ \ \ P \ \" | negI: "\ # P \ \\<^sub>p \ P \ \\<^sub>p \" | negE: "P \ \ \ P \ \\<^sub>p \ \ P \ \\<^sub>p" | botE: "P \ \\<^sub>p \ P \ \" | dnegE: "P \ \\<^sub>p\\<^sub>p \ \ P \ \" text \ Prove that \\\ is monotone with respect to premises, that is, we can arbitrarily extend the list of premises in a valid prove. \ lemma proves_mono: assumes "P \ \" and "set P \ set Q" shows "Q \ \" sorry text \ Prove the following derived natural deduction rules that might be useful later on: \ lemma dnegI: assumes "P \ \" shows "P \ \\<^sub>p\\<^sub>p \" sorry lemma pbc: assumes "\\<^sub>p \ # P \ \\<^sub>p" shows "P \ \" sorry lemma lem: "P \ \ \\<^sub>p \\<^sub>p \" sorry lemma neg_conj: assumes "\ \ {\, \}" and "P \ \\<^sub>p \" shows "P \ \\<^sub>p (\ \\<^sub>p \)" sorry lemma neg_disj: assumes "P \ \\<^sub>p \" and "P \ \\<^sub>p \" shows "P \ \\<^sub>p (\ \\<^sub>p \)" sorry lemma trivial_imp: assumes "P \ \" shows "P \ \ \\<^sub>p \" sorry lemma vacuous_imp: assumes "P \ \\<^sub>p \" shows "P \ \ \\<^sub>p \" sorry lemma neg_imp: assumes "P \ \" and "P \ \\<^sub>p \" shows "P \ \\<^sub>p (\ \\<^sub>p \)" sorry subsection \Soundness\ text \ Prove soundness of \\\ with respect to \\\. \ lemma proves_sound: assumes "P \ \" shows "P \ \" sorry subsection \Completeness\ text \ Prove completeness of \\\ with respect to \\\ in absence of premises. \ lemma prove_complete_Nil: assumes "[] \ \" shows "[] \ \" sorry text \ No extend the above result to also incorporate premises. \ lemma proves_complete: assumes "P \ \" shows "P \ \" sorry text \ Conclude that semantic entailment is equivalent to provability. \ lemma entails_proves_conv: "P \ \ \ P \ \" sorry end