section ‹Meta-theory of propositional logic›
theory PropLog imports Main begin
text ‹
Datatype definition of propositional logic formulae and inductive
definition of the propositional tautologies.
Inductive definition of propositional logic. Soundness and
completeness w.r.t.\ truth-tables.
Prove: If ‹H |= p› then ‹G |= p› where ‹G ∈
Fin(H)›
›
subsection ‹The datatype of propositions›
datatype 'a pl =
false |
var 'a ("#_" [1000]) |
imp "'a pl" "'a pl" (infixr "->" 90)
subsection ‹The proof system›
inductive thms :: "['a pl set, 'a pl] => bool" (infixl "|-" 50)
for H :: "'a pl set"
where
H: "p∈H ==> H |- p"
| K: "H |- p->q->p"
| S: "H |- (p->q->r) -> (p->q) -> p->r"
| DN: "H |- ((p->false) -> false) -> p"
| MP: "[| H |- p->q; H |- p |] ==> H |- q"
subsection ‹The semantics›
subsubsection ‹Semantics of propositional logic.›
primrec eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100)
where
"tt[[false]] = False"
| "tt[[#v]] = (v ∈ tt)"
| eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])"
text ‹
A finite set of hypotheses from ‹t› and the ‹Var›s in
‹p›.
›
primrec hyps :: "['a pl, 'a set] => 'a pl set"
where
"hyps false tt = {}"
| "hyps (#v) tt = {if v ∈ tt then #v else #v->false}"
| "hyps (p->q) tt = hyps p tt Un hyps q tt"
subsubsection ‹Logical consequence›
text ‹
For every valuation, if all elements of ‹H› are true then so
is ‹p›.
›
definition sat :: "['a pl set, 'a pl] => bool" (infixl "|=" 50)
where "H |= p = (∀tt. (∀q∈H. tt[[q]]) --> tt[[p]])"
subsection ‹Proof theory of propositional logic›
lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"
apply (rule predicate1I)
apply (erule thms.induct)
apply (auto intro: thms.intros)
done
lemma thms_I: "H |- p->p"
― ‹Called ‹I› for Identity Combinator, not for Introduction.›
by (best intro: thms.K thms.S thms.MP)
subsubsection ‹Weakening, left and right›
lemma weaken_left: "[| G ⊆ H; G|-p |] ==> H|-p"
― ‹Order of premises is convenient with ‹THEN››
by (erule thms_mono [THEN predicate1D])
lemma weaken_left_insert: "G |- p ⟹ insert a G |- p"
by (rule weaken_left) (rule subset_insertI)
lemma weaken_left_Un1: "G |- p ⟹ G ∪ B |- p"
by (rule weaken_left) (rule Un_upper1)
lemma weaken_left_Un2: "G |- p ⟹ A ∪ G |- p"
by (rule weaken_left) (rule Un_upper2)
lemma weaken_right: "H |- q ==> H |- p->q"
by (fast intro: thms.K thms.MP)
subsubsection ‹The deduction theorem›
theorem deduction: "insert p H |- q ==> H |- p->q"
apply (induct set: thms)
apply (fast intro: thms_I thms.H thms.K thms.S thms.DN
thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+
done
subsubsection ‹The cut rule›
lemma cut: "insert p H |- q ⟹ H |- p ⟹ H |- q"
by (rule thms.MP) (rule deduction)
lemma thms_falseE: "H |- false ⟹ H |- q"
by (rule thms.MP, rule thms.DN) (rule weaken_right)
lemma thms_notE: "H |- p -> false ⟹ H |- p ⟹ H |- q"
by (rule thms_falseE) (rule thms.MP)
subsubsection ‹Soundness of the rules wrt truth-table semantics›
theorem soundness: "H |- p ==> H |= p"
by (induct set: thms) (auto simp: sat_def)
subsection ‹Completeness›
subsubsection ‹Towards the completeness proof›
lemma false_imp: "H |- p->false ==> H |- p->q"
apply (rule deduction)
apply (metis H insert_iff weaken_left_insert thms_notE)
done
lemma imp_false:
"[| H |- p; H |- q->false |] ==> H |- (p->q)->false"
apply (rule deduction)
apply (metis H MP insert_iff weaken_left_insert)
done
lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
― ‹Typical example of strengthening the induction statement.›
apply simp
apply (induct p)
apply (simp_all add: thms_I thms.H)
apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right
imp_false false_imp)
done
lemma sat_thms_p: "{} |= p ==> hyps p tt |- p"
― ‹Key lemma for completeness; yields a set of assumptions
satisfying ‹p››
unfolding sat_def
by (metis (full_types) empty_iff hyps_thms_if)
text ‹
For proving certain theorems in our new propositional logic.
›
declare deduction [intro!]
declare thms.H [THEN thms.MP, intro]
text ‹
The excluded middle in the form of an elimination rule.
›
lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q"
apply (rule deduction [THEN deduction])
apply (rule thms.DN [THEN thms.MP], best intro: H)
done
lemma thms_excluded_middle_rule:
"[| insert p H |- q; insert (p->false) H |- q |] ==> H |- q"
― ‹Hard to prove directly because it requires cuts›
by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto)
subsection‹Completeness -- lemmas for reducing the set of assumptions›
text ‹
For the case @{prop "hyps p t - insert #v Y |- p"} we also have @{prop
"hyps p t - {#v} ⊆ hyps p (t-{v})"}.
›
lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"
by (induct p) auto
text ‹
For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have
@{prop "hyps p t-{#v->Fls} ⊆ hyps p (insert v t)"}.
›
lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"
by (induct p) auto
text ‹Two lemmas for use with ‹weaken_left››
lemma insert_Diff_same: "B-C <= insert a (B-insert a C)"
by fast
lemma insert_Diff_subset2: "insert a (B-{c}) - D <= insert a (B-insert c D)"
by fast
text ‹
The set @{term "hyps p t"} is finite, and elements have the form
@{term "#v"} or @{term "#v->Fls"}.
›
lemma hyps_finite: "finite(hyps p t)"
by (induct p) auto
lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})"
by (induct p) auto
lemma Diff_weaken_left: "A ⊆ C ⟹ A - B |- p ⟹ C - B |- p"
by (rule Diff_mono [OF _ subset_refl, THEN weaken_left])
subsubsection ‹Completeness theorem›
text ‹
Induction on the finite set of assumptions @{term "hyps p t0"}. We
may repeatedly subtract assumptions until none are left!
›
lemma completeness_0_lemma:
"{} |= p ==> ∀t. hyps p t - hyps p t0 |- p"
apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
apply (simp add: sat_thms_p, safe)
txt‹Case ‹hyps p t-insert(#v,Y) |- p››
apply (iprover intro: thms_excluded_middle_rule
insert_Diff_same [THEN weaken_left]
insert_Diff_subset2 [THEN weaken_left]
hyps_Diff [THEN Diff_weaken_left])
txt‹Case ‹hyps p t-insert(#v -> false,Y) |- p››
apply (iprover intro: thms_excluded_middle_rule
insert_Diff_same [THEN weaken_left]
insert_Diff_subset2 [THEN weaken_left]
hyps_insert [THEN Diff_weaken_left])
done
text‹The base case for completeness›
lemma completeness_0: "{} |= p ==> {} |- p"
by (metis Diff_cancel completeness_0_lemma)
text‹A semantic analogue of the Deduction Theorem›
lemma sat_imp: "insert p H |= q ==> H |= p->q"
by (auto simp: sat_def)
theorem completeness: "finite H ==> H |= p ==> H |- p"
apply (induct arbitrary: p rule: finite_induct)
apply (blast intro: completeness_0)
apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
done
theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
by (blast intro: soundness completeness)
end