# Theory Classical_Logic_Completeness

chapter ‹ Classical Soundness and Completeness \label{sec:classical-propositional-calculus} ›

theory Classical_Logic_Completeness
imports Classical_Logic
begin

text ‹ The following presents soundness completeness of the classical propositional
calculus for propositional semantics. The classical propositional calculus
is sometimes referred to as the ∗‹sentential calculus›.
We give a concrete algebraic data type for propositional
formulae in \S\ref{sec:classical-calculus-syntax}. We inductively
define a logical judgement ‹⊢⇩p⇩r⇩o⇩p› for these formulae.
We also define the Tarski truth relation ‹⊨⇩p⇩r⇩o⇩p› inductively,
which we present in \S\ref{sec:propositional-semantics}.›

text ‹ The most significant results here are the ∗‹embedding theorems›.
These theorems show that the propositional calculus
can be embedded in any logic extending @{class classical_logic}.
These theorems are proved in \S\ref{sec:propositional-embedding}. ›

section ‹ Syntax \label{sec:classical-calculus-syntax} ›

text ‹ Here we provide the usual language for formulae in the propositional
calculus. It contains  ∗‹falsum› ‹❙⊥›, implication ‹(❙→)›, and a way of
constructing ∗‹atomic› propositions ‹λ φ . ❙⟨ φ ❙⟩›. Defining the
language is straight-forward using an algebraic data type. ›

datatype 'a classical_propositional_formula =
Falsum ("❙⊥")
| Proposition 'a ("❙⟨ _ ❙⟩" [45])
| Implication
"'a classical_propositional_formula"
"'a classical_propositional_formula" (infixr "❙→" 70)

section ‹ Propositional Calculus ›

text ‹ In this section we recursively define what a proof is in the classical
propositional calculus. We provide the familiar ∗‹K› and ∗‹S› axioms,
as well as ∗‹double negation› and ∗‹modus ponens›. ›

named_theorems classical_propositional_calculus
"Rules for the Propositional Calculus"

inductive classical_propositional_calculus ::
"'a classical_propositional_formula ⇒ bool" ("⊢⇩p⇩r⇩o⇩p _" [60] 55)
where
axiom_k [classical_propositional_calculus]:
"⊢⇩p⇩r⇩o⇩p φ ❙→ ψ ❙→ φ"
| axiom_s [classical_propositional_calculus]:
"⊢⇩p⇩r⇩o⇩p (φ ❙→ ψ ❙→ χ) ❙→ (φ ❙→ ψ) ❙→ φ ❙→ χ"
| double_negation [classical_propositional_calculus]:
"⊢⇩p⇩r⇩o⇩p ((φ ❙→ ❙⊥) ❙→ ❙⊥) ❙→ φ"
| modus_ponens [classical_propositional_calculus]:
"⊢⇩p⇩r⇩o⇩p φ ❙→ ψ ⟹ ⊢⇩p⇩r⇩o⇩p φ ⟹ ⊢⇩p⇩r⇩o⇩p ψ"

text ‹ Our proof system for our propositional calculus is trivially
an instance of @{class classical_logic}. The introduction rules
for ‹⊢⇩p⇩r⇩o⇩p› naturally reflect the axioms of the classical logic
axiom class. ›

instantiation classical_propositional_formula
:: (type) classical_logic
begin
definition [simp]: "⊥ = ❙⊥"
definition [simp]: "⊢ φ = ⊢⇩p⇩r⇩o⇩p φ"
definition [simp]: "φ → ψ = φ ❙→ ψ"
instance by standard (simp add: classical_propositional_calculus)+
end

section ‹ Propositional Semantics \label{sec:propositional-semantics} ›

text ‹ Below we give the typical definition of the Tarski truth relation
‹ ⊨⇩p⇩r⇩o⇩p›. ›

primrec classical_propositional_semantics ::
"'a set ⇒ 'a classical_propositional_formula ⇒ bool"
(infix "⊨⇩p⇩r⇩o⇩p" 65)
where
"𝔐 ⊨⇩p⇩r⇩o⇩p ❙⟨ p ❙⟩ = (p ∈ 𝔐)"
|  "𝔐 ⊨⇩p⇩r⇩o⇩p φ ❙→ ψ = (𝔐 ⊨⇩p⇩r⇩o⇩p φ ⟶ 𝔐 ⊨⇩p⇩r⇩o⇩p ψ)"
|  "𝔐 ⊨⇩p⇩r⇩o⇩p ❙⊥ = False"

text ‹ Soundness of our calculus for these semantics is trivial. ›

theorem classical_propositional_calculus_soundness:
"⊢⇩p⇩r⇩o⇩p φ ⟹ 𝔐 ⊨⇩p⇩r⇩o⇩p φ"
by (induct rule: classical_propositional_calculus.induct, simp+)

section ‹ Soundness and Completeness Proofs \label{sec:classical-logic-completeness}›

definition strong_classical_propositional_deduction ::
"'a classical_propositional_formula set
⇒ 'a classical_propositional_formula ⇒ bool"
(infix "⊩⇩p⇩r⇩o⇩p" 65)
where
[simp]: "Γ ⊩⇩p⇩r⇩o⇩p φ ≡ Γ ⊩ φ"

definition strong_classical_propositional_tarski_truth ::
"'a classical_propositional_formula set
⇒ 'a classical_propositional_formula ⇒ bool"
(infix "⊫⇩p⇩r⇩o⇩p" 65)
where
[simp]: "Γ ⊫⇩p⇩r⇩o⇩p φ ≡ ∀ 𝔐.(∀ γ ∈ Γ. 𝔐 ⊨⇩p⇩r⇩o⇩p γ) ⟶ 𝔐 ⊨⇩p⇩r⇩o⇩p φ"

definition theory_propositions ::
"'a classical_propositional_formula set ⇒ 'a set" ("❙⦃ _ ❙⦄" [50])
where
[simp]: "❙⦃ Γ ❙⦄ = {p . Γ ⊩⇩p⇩r⇩o⇩p ❙⟨ p ❙⟩}"

text ‹ Below we give the main lemma for completeness: the ∗‹truth lemma›.
This proof connects the maximally consistent sets developed in \S\ref{sec:implicational-maximally-consistent-sets}
and \S\ref{sec:mcs} with the semantics given in
\S\ref{sec:propositional-semantics}. ›

text ‹ All together, the technique we are using essentially follows the
approach by Blackburn et al. @{cite ‹\S 4.2, pgs. 196-201› blackburnSectionCanonicalModels2001}. ›

lemma truth_lemma:
assumes "MCS Γ"
shows "Γ ⊩⇩p⇩r⇩o⇩p φ ≡ ❙⦃ Γ ❙⦄ ⊨⇩p⇩r⇩o⇩p φ"
proof (induct φ)
case Falsum
then show ?case using assms by auto
next
case (Proposition x)
then show ?case by simp
next
case (Implication ψ χ)
thus ?case
unfolding strong_classical_propositional_deduction_def
by (metis
assms
maximally_consistent_set_def
formula_maximally_consistent_set_def_implication
classical_propositional_semantics.simps(2)
implication_classical_propositional_formula_def
set_deduction_modus_ponens
set_deduction_reflection)
qed

text ‹ Here the truth lemma above is combined with @{thm formula_maximally_consistent_extension [no_vars]}
proven in \S\ref{sec:propositional-semantics}.  These theorems together
give rise to strong completeness for the propositional calculus. ›

theorem classical_propositional_calculus_strong_soundness_and_completeness:
"Γ ⊩⇩p⇩r⇩o⇩p φ = Γ ⊫⇩p⇩r⇩o⇩p φ"
proof -
have soundness: "Γ ⊩⇩p⇩r⇩o⇩p φ ⟹ Γ ⊫⇩p⇩r⇩o⇩p φ"
proof -
assume "Γ ⊩⇩p⇩r⇩o⇩p φ"
from this obtain Γ' where Γ': "set Γ' ⊆ Γ" "Γ' :⊢ φ"
{
fix 𝔐
assume "∀ γ ∈ Γ. 𝔐 ⊨⇩p⇩r⇩o⇩p γ"
hence "∀ γ ∈ set Γ'. 𝔐 ⊨⇩p⇩r⇩o⇩p γ" using Γ'(1) by auto
hence "∀ φ. Γ' :⊢ φ ⟶ 𝔐 ⊨⇩p⇩r⇩o⇩p φ"
proof (induct Γ')
case Nil
then show ?case
classical_propositional_calculus_soundness
list_deduction_def)
next
case (Cons ψ Γ')
thus ?case using list_deduction_theorem by fastforce
qed
with Γ'(2) have "𝔐 ⊨⇩p⇩r⇩o⇩p φ" by blast
}
thus "Γ ⊫⇩p⇩r⇩o⇩p φ"
using strong_classical_propositional_tarski_truth_def by blast
qed
have completeness: "Γ ⊫⇩p⇩r⇩o⇩p φ ⟹ Γ ⊩⇩p⇩r⇩o⇩p φ"
proof (erule contrapos_pp)
assume "¬ Γ ⊩⇩p⇩r⇩o⇩p φ"
hence "∃ 𝔐. (∀ γ ∈ Γ. 𝔐 ⊨⇩p⇩r⇩o⇩p γ) ∧ ¬ 𝔐 ⊨⇩p⇩r⇩o⇩p φ"
proof -
from ‹¬ Γ ⊩⇩p⇩r⇩o⇩p φ› obtain Ω where Ω: "Γ ⊆ Ω" "φ-MCS Ω"
by (meson
formula_consistent_def
formula_maximally_consistent_extension
strong_classical_propositional_deduction_def)
hence "(φ → ⊥) ∈ Ω"
using formula_maximally_consistent_set_def_negation by blast
hence "¬ ❙⦃ Ω ❙⦄ ⊨⇩p⇩r⇩o⇩p φ"
using Ω
formula_consistent_def
formula_maximal_consistency
formula_maximally_consistent_set_def_def
truth_lemma
unfolding strong_classical_propositional_deduction_def
by blast
moreover have "∀ γ ∈ Γ. ❙⦃ Ω ❙⦄ ⊨⇩p⇩r⇩o⇩p γ"
using
formula_maximal_consistency
truth_lemma
Ω
set_deduction_reflection
unfolding strong_classical_propositional_deduction_def
by blast
ultimately show ?thesis by auto
qed
thus "¬ Γ ⊫⇩p⇩r⇩o⇩p φ"
unfolding strong_classical_propositional_tarski_truth_def
by simp
qed
from soundness completeness show "Γ ⊩⇩p⇩r⇩o⇩p φ = Γ ⊫⇩p⇩r⇩o⇩p φ"
by linarith
qed

text ‹ For our applications in \S{sec:propositional-embedding},
we will only need a weaker form of soundness and completeness
rather than the stronger form proved above.›

theorem classical_propositional_calculus_soundness_and_completeness:
"⊢⇩p⇩r⇩o⇩p φ = (∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p φ)"
using classical_propositional_calculus_soundness [where φ="φ"]
classical_propositional_calculus_strong_soundness_and_completeness
[where φ="φ" and Γ="{}"]
strong_classical_propositional_deduction_def
[where φ="φ" and Γ="{}"]
strong_classical_propositional_tarski_truth_def
[where φ="φ" and Γ="{}"]
deduction_classical_propositional_formula_def [where φ="φ"]
set_deduction_base_theory [where φ="φ"]
by metis

instantiation classical_propositional_formula
:: (type) consistent_classical_logic
begin
instance by standard
end

section ‹ Embedding Theorem For the Propositional Calculus \label{sec:propositional-embedding} ›

text ‹ A recurring technique to prove theorems in logic moving forward is
∗‹embed› our theorem into the classical propositional calculus. ›

text ‹ Using our embedding, we can leverage completeness to turn our
problem into semantics and dispatch to Isabelle/HOL's classical
theorem provers.›

text ‹ In future work we may make a tactic for this, but for now we just
manually leverage the technique throughout our subsequent proofs. ›

primrec (in classical_logic)
classical_propositional_formula_embedding
:: "'a classical_propositional_formula ⇒ 'a" ("❙⦇ _ ❙⦈" [50]) where
"❙⦇ ❙⟨ p ❙⟩ ❙⦈ = p"
| "❙⦇ φ ❙→ ψ ❙⦈ = ❙⦇ φ ❙⦈ → ❙⦇ ψ ❙⦈"
| "❙⦇ ❙⊥ ❙⦈ = ⊥"

theorem (in classical_logic) propositional_calculus:
"⊢⇩p⇩r⇩o⇩p φ ⟹ ⊢ ❙⦇ φ ❙⦈"
by (induct rule: classical_propositional_calculus.induct,
(simp add: axiom_k axiom_s double_negation modus_ponens)+)

text ‹ The following theorem in particular shows that it suffices to
prove theorems using classical semantics to prove theorems about
the logic under investigation. ›

theorem (in classical_logic) propositional_semantics:
"∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p φ ⟹ ⊢ ❙⦇ φ ❙⦈"