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 \