Theory Classical_Connectives

chapter ‹ Classical Logic Connectives \label{sec:logical-connectives}›

theory Classical_Connectives
imports
Classical_Logic_Completeness
List_Utilities
begin

text ‹ Here we define the usual connectives for classical logic. ›

no_notation FuncSet.funcset (infixr "→" 60)

section ‹ Verum ›

definition (in classical_logic) verum :: "'a" ("⊤")
where
"⊤ = ⊥ → ⊥"

lemma (in classical_logic) verum_tautology [simp]: "⊢ ⊤"
by (metis list_implication.simps(1) list_implication_axiom_k verum_def)

lemma verum_semantics [simp]:
"𝔐 ⊨⇩p⇩r⇩o⇩p ⊤"
unfolding verum_def by simp

lemma (in classical_logic) verum_embedding [simp]:
"❙⦇ ⊤ ❙⦈ = ⊤"

section ‹ Conjunction ›

definition (in classical_logic)
conjunction :: "'a ⇒ 'a ⇒ 'a" (infixr "⊓" 67)
where
"φ ⊓ ψ = (φ → ψ → ⊥) → ⊥"

primrec (in classical_logic)
arbitrary_conjunction :: "'a list ⇒ 'a" ("⨅")
where
"⨅ [] = ⊤"
|  "⨅ (φ # Φ) = φ ⊓ ⨅ Φ"

lemma (in classical_logic) conjunction_introduction:
"⊢ φ → ψ → (φ ⊓ ψ)"
by (metis
modus_ponens
conjunction_def
list_flip_implication1
list_implication.simps(1)
list_implication.simps(2))

lemma (in classical_logic) conjunction_left_elimination:
"⊢ (φ ⊓ ψ) → φ"
by (metis (full_types)
Peirces_law
pseudo_scotus
conjunction_def
list_deduction_base_theory
list_deduction_modus_ponens
list_deduction_theorem
list_deduction_weaken)

lemma (in classical_logic) conjunction_right_elimination:
"⊢ (φ ⊓ ψ) → ψ"
by (metis (full_types)
axiom_k
Contraposition
modus_ponens
conjunction_def
flip_hypothetical_syllogism
flip_implication)

lemma (in classical_logic) conjunction_embedding [simp]:
"❙⦇ φ ⊓ ψ ❙⦈ = ❙⦇ φ ❙⦈ ⊓ ❙⦇ ψ ❙⦈"
unfolding conjunction_def classical_logic_class.conjunction_def
by simp

lemma conjunction_semantics [simp]:
"𝔐 ⊨⇩p⇩r⇩o⇩p φ ⊓ ψ = (𝔐 ⊨⇩p⇩r⇩o⇩p φ ∧ 𝔐 ⊨⇩p⇩r⇩o⇩p ψ)"
unfolding conjunction_def by simp

section ‹ Biconditional ›

definition (in classical_logic) biconditional :: "'a ⇒ 'a ⇒ 'a"   (infixr "↔" 75)
where
"φ ↔ ψ = (φ → ψ) ⊓ (ψ → φ)"

lemma (in classical_logic) biconditional_introduction:
"⊢ (φ → ψ) → (ψ → φ) → (φ ↔ ψ)"

lemma (in classical_logic) biconditional_left_elimination:
"⊢ (φ ↔ ψ) → φ → ψ"

lemma (in classical_logic) biconditional_right_elimination:
"⊢ (φ ↔ ψ) → ψ → φ"

lemma (in classical_logic) biconditional_embedding [simp]:
"❙⦇ φ ↔ ψ ❙⦈ = ❙⦇ φ ❙⦈ ↔ ❙⦇ ψ ❙⦈"
unfolding biconditional_def classical_logic_class.biconditional_def
by simp

lemma biconditional_semantics [simp]:
"𝔐 ⊨⇩p⇩r⇩o⇩p φ ↔ ψ = (𝔐 ⊨⇩p⇩r⇩o⇩p φ ⟷ 𝔐 ⊨⇩p⇩r⇩o⇩p ψ)"
unfolding biconditional_def
by (simp, blast)

section ‹ Negation ›

definition (in classical_logic) negation :: "'a ⇒ 'a"  ("∼")
where
"∼ φ = φ → ⊥"

lemma (in classical_logic) negation_introduction:
"⊢ (φ → ⊥) → ∼ φ"
unfolding negation_def
by (metis axiom_k modus_ponens implication_absorption)

lemma (in classical_logic) negation_elimination:
"⊢ ∼ φ → (φ → ⊥)"
unfolding negation_def
by (metis axiom_k modus_ponens implication_absorption)

lemma (in classical_logic) negation_embedding [simp]:
"❙⦇ ∼ φ ❙⦈ = ∼ ❙⦇ φ ❙⦈"
classical_logic_class.negation_def
negation_def)

lemma negation_semantics [simp]:
"𝔐 ⊨⇩p⇩r⇩o⇩p ∼ φ = (¬ 𝔐 ⊨⇩p⇩r⇩o⇩p φ)"
unfolding negation_def
by simp

section ‹ Disjunction ›

definition (in classical_logic) disjunction :: "'a ⇒ 'a ⇒ 'a"   (infixr "⊔" 67)
where
"φ ⊔ ψ = (φ → ⊥) → ψ"

primrec (in classical_logic) arbitrary_disjunction :: "'a list ⇒ 'a" ("⨆")
where
"⨆ [] = ⊥"
|  "⨆ (φ # Φ) = φ ⊔ ⨆ Φ"

lemma (in classical_logic) disjunction_elimination:
"⊢ (φ → χ) → (ψ → χ) → (φ ⊔ ψ) → χ"
proof -
let ?Γ = "[φ → χ, ψ → χ, φ ⊔ ψ]"
have "?Γ :⊢ (φ → ⊥) → χ"
unfolding disjunction_def
by (metis hypothetical_syllogism
list_deduction_def
list_implication.simps(1)
list_implication.simps(2)
set_deduction_base_theory
set_deduction_theorem
set_deduction_weaken)
hence "?Γ :⊢ χ"
using excluded_middle_elimination
list_deduction_modus_ponens
list_deduction_theorem
list_deduction_weaken
by blast
thus ?thesis
unfolding list_deduction_def
by simp
qed

lemma (in classical_logic) disjunction_left_introduction:
"⊢ φ → (φ ⊔ ψ)"
unfolding disjunction_def
by (metis modus_ponens
pseudo_scotus
flip_implication)

lemma (in classical_logic) disjunction_right_introduction:
"⊢ ψ → (φ ⊔ ψ)"
unfolding disjunction_def
using axiom_k
by simp

lemma (in classical_logic) disjunction_embedding [simp]:
"❙⦇ φ ⊔ ψ ❙⦈ = ❙⦇ φ ❙⦈ ⊔ ❙⦇ ψ ❙⦈"
unfolding disjunction_def classical_logic_class.disjunction_def
by simp

lemma disjunction_semantics [simp]:
"𝔐 ⊨⇩p⇩r⇩o⇩p φ ⊔ ψ = (𝔐 ⊨⇩p⇩r⇩o⇩p φ ∨ 𝔐 ⊨⇩p⇩r⇩o⇩p ψ)"
unfolding disjunction_def
by (simp, blast)

section ‹ Mutual Exclusion ›

primrec (in classical_logic) exclusive :: "'a list ⇒ 'a" ("∐")
where
"∐ [] = ⊤"
| "∐ (φ # Φ) = ∼ (φ ⊓ ⨆ Φ) ⊓ ∐ Φ"

section ‹ Subtraction ›

definition (in classical_logic) subtraction :: "'a ⇒ 'a ⇒ 'a" (infixl "∖" 69)
where "φ ∖ ψ = φ ⊓ ∼ ψ"

lemma (in classical_logic) subtraction_embedding [simp]:
"❙⦇ φ ∖ ψ ❙⦈ = ❙⦇ φ ❙⦈ ∖ ❙⦇ ψ ❙⦈"
unfolding subtraction_def classical_logic_class.subtraction_def
by simp

section ‹ Negated Lists ›

definition (in classical_logic) map_negation :: "'a list ⇒ 'a list" ("❙∼")
where [simp]: "❙∼ Φ ≡ map ∼ Φ"

section ‹ Common (\& Uncommon) Identities ›

subsection ‹ Biconditional Equivalence Relation ›

lemma (in classical_logic) biconditional_reflection:
"⊢ φ ↔ φ"
by (meson
axiom_k
modus_ponens
biconditional_introduction
implication_absorption)

lemma (in classical_logic) biconditional_symmetry:
"⊢ (φ ↔ ψ) ↔ (ψ ↔ φ)"
by (metis (full_types) modus_ponens
biconditional_def
conjunction_def
flip_hypothetical_syllogism
flip_implication)

lemma (in classical_logic) biconditional_symmetry_rule:
"⊢ φ ↔ ψ ⟹ ⊢ ψ ↔ φ"
by (meson modus_ponens
biconditional_introduction
biconditional_left_elimination
biconditional_right_elimination)

lemma (in classical_logic) biconditional_transitivity:
"⊢ (φ ↔ ψ) → (ψ ↔ χ) → (φ ↔ χ)"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ ↔ ❙⟨ψ❙⟩) → (❙⟨ψ❙⟩ ↔ ❙⟨χ❙⟩) → (❙⟨φ❙⟩ ↔ ❙⟨χ❙⟩)"
by simp
hence "⊢ ❙⦇ (❙⟨φ❙⟩ ↔ ❙⟨ψ❙⟩) → (❙⟨ψ❙⟩ ↔ ❙⟨χ❙⟩) → (❙⟨φ❙⟩ ↔ ❙⟨χ❙⟩) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) biconditional_transitivity_rule:
"⊢ φ ↔ ψ ⟹ ⊢ ψ ↔ χ ⟹ ⊢ φ ↔ χ"
using modus_ponens biconditional_transitivity by blast

subsection ‹ Biconditional Weakening ›

lemma (in classical_logic) biconditional_weaken:
assumes "Γ ⊩ φ ↔ ψ"
shows "Γ ⊩ φ = Γ ⊩ ψ"
by (metis assms
biconditional_left_elimination
biconditional_right_elimination
set_deduction_modus_ponens
set_deduction_weaken)

lemma (in classical_logic) list_biconditional_weaken:
assumes "Γ :⊢ φ ↔ ψ"
shows "Γ :⊢ φ = Γ :⊢ ψ"
by (metis assms
biconditional_left_elimination
biconditional_right_elimination
list_deduction_modus_ponens
list_deduction_weaken)

lemma (in classical_logic) weak_biconditional_weaken:
assumes "⊢ φ ↔ ψ"
shows "⊢ φ = ⊢ ψ"
by (metis assms
biconditional_left_elimination
biconditional_right_elimination
modus_ponens)

subsection ‹ Conjunction Identities ›

lemma (in classical_logic) conjunction_negation_identity:
"⊢ ∼ (φ ⊓ ψ) ↔ (φ → ψ → ⊥)"
by (metis Contraposition
double_negation_converse
modus_ponens
biconditional_introduction
conjunction_def
negation_def)

lemma (in classical_logic) conjunction_set_deduction_equivalence [simp]:
"Γ ⊩ φ ⊓ ψ = (Γ ⊩ φ ∧ Γ ⊩ ψ)"
by (metis set_deduction_weaken [where Γ="Γ"]
set_deduction_modus_ponens [where Γ="Γ"]
conjunction_introduction
conjunction_left_elimination
conjunction_right_elimination)

lemma (in classical_logic) conjunction_list_deduction_equivalence [simp]:
"Γ :⊢ φ ⊓ ψ = (Γ :⊢ φ ∧ Γ :⊢ ψ)"
by (metis list_deduction_weaken [where Γ="Γ"]
list_deduction_modus_ponens [where Γ="Γ"]
conjunction_introduction
conjunction_left_elimination
conjunction_right_elimination)

lemma (in classical_logic) weak_conjunction_deduction_equivalence [simp]:
"⊢ φ ⊓ ψ = (⊢ φ ∧ ⊢ ψ)"
by (metis conjunction_set_deduction_equivalence set_deduction_base_theory)

lemma (in classical_logic) conjunction_set_deduction_arbitrary_equivalence [simp]:
"Γ ⊩ ⨅ Φ = (∀ φ ∈ set Φ. Γ ⊩ φ)"
by (induct Φ, simp add: set_deduction_weaken, simp)

lemma (in classical_logic) conjunction_list_deduction_arbitrary_equivalence [simp]:
"Γ :⊢ ⨅ Φ = (∀ φ ∈ set Φ. Γ :⊢ φ)"
by (induct Φ, simp add: list_deduction_weaken, simp)

lemma (in classical_logic) weak_conjunction_deduction_arbitrary_equivalence [simp]:
"⊢ ⨅ Φ = (∀ φ ∈ set Φ. ⊢ φ)"
by (induct Φ, simp+)

lemma (in classical_logic) conjunction_commutativity:
"⊢ (ψ ⊓ φ) ↔ (φ ⊓ ψ)"
by (metis
(full_types)
modus_ponens
biconditional_introduction
conjunction_def
flip_hypothetical_syllogism
flip_implication)

lemma (in classical_logic) conjunction_associativity:
"⊢ ((φ ⊓ ψ) ⊓ χ) ↔ (φ ⊓ (ψ ⊓ χ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ((❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) ⊓ ❙⟨χ❙⟩) ↔ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩))"
by simp
hence "⊢ ❙⦇ ((❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) ⊓ ❙⟨χ❙⟩) ↔ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) arbitrary_conjunction_antitone:
"set Φ ⊆ set Ψ ⟹ ⊢ ⨅ Ψ → ⨅ Φ"
proof -
have "∀ Φ. set Φ ⊆ set Ψ ⟶ ⊢ ⨅ Ψ → ⨅ Φ"
proof (induct Ψ)
case Nil
then show ?case
next
case (Cons ψ Ψ)
{
fix Φ
assume "set Φ ⊆ set (ψ # Ψ)"
have "⊢ ⨅ (ψ # Ψ) → ⨅ Φ"
proof (cases "ψ ∈ set Φ")
assume "ψ ∈ set Φ"
have "∀ φ ∈ set Φ. ⊢ ⨅ Φ ↔ (φ ⊓ ⨅ (removeAll φ Φ))"
proof (induct Φ)
case Nil
then show ?case by simp
next
case (Cons χ Φ)
{
fix φ
assume "φ ∈ set (χ # Φ)"
have "⊢ ⨅ (χ # Φ) ↔ (φ ⊓ ⨅ (removeAll φ (χ # Φ)))"
proof cases
assume "φ ∈ set Φ"
hence "⊢ ⨅ Φ ↔ (φ ⊓ ⨅ (removeAll φ Φ))"
using Cons.hyps ‹φ ∈ set Φ›
by auto
moreover
have "⊢ (⨅ Φ ↔ (φ ⊓ ⨅ (removeAll φ Φ))) →
(χ ⊓ ⨅ Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p
(❙⟨⨅ Φ❙⟩ ↔ (❙⟨φ❙⟩ ⊓ ❙⟨⨅ (removeAll φ Φ)❙⟩))
→ (❙⟨χ❙⟩ ⊓ ❙⟨⨅ Φ❙⟩)
↔ (❙⟨φ❙⟩ ⊓ ❙⟨χ❙⟩ ⊓ ❙⟨⨅ (removeAll φ Φ)❙⟩)"
by auto
hence "⊢ ❙⦇ (❙⟨⨅ Φ❙⟩ ↔ (❙⟨φ❙⟩ ⊓ ❙⟨⨅ (removeAll φ Φ)❙⟩))
→ (❙⟨χ❙⟩ ⊓ ❙⟨⨅ Φ❙⟩)
↔ (❙⟨φ❙⟩ ⊓ ❙⟨χ❙⟩ ⊓ ❙⟨⨅ (removeAll φ Φ)❙⟩) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed
ultimately have "⊢ ⨅ (χ # Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))"
using modus_ponens by auto
show ?thesis
proof cases
assume "φ = χ"
moreover
{
fix φ
have "⊢ (χ ⊓ φ) → (χ ⊓ χ ⊓ φ)"
unfolding conjunction_def
by (meson
axiom_s
double_negation
modus_ponens
flip_hypothetical_syllogism
flip_implication)
} note tautology = this
from ‹⊢ ⨅ (χ # Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))›
‹φ = χ›
have "⊢ (χ ⊓ ⨅ (removeAll χ Φ)) → (χ ⊓ ⨅ Φ)"
unfolding biconditional_def
by (simp, metis tautology hypothetical_syllogism modus_ponens)
moreover
from ‹⊢ ⨅ (χ # Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))›
‹φ = χ›
have "⊢ (χ ⊓ ⨅ Φ) → (χ ⊓ ⨅ (removeAll χ Φ))"
unfolding biconditional_def
by (simp,
metis conjunction_right_elimination
hypothetical_syllogism
modus_ponens)
ultimately show ?thesis
unfolding biconditional_def
by simp
next
assume "φ ≠ χ"
then show ?thesis
using ‹⊢ ⨅ (χ # Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))›
by simp
qed
next
assume "φ ∉ set Φ"
hence "φ = χ" "χ ∉ set Φ"
using ‹φ ∈ set (χ # Φ)› by auto
then show ?thesis
using biconditional_reflection
by simp
qed
}
thus ?case by blast
qed
hence "⊢ (ψ ⊓ ⨅ (removeAll ψ Φ)) → ⨅ Φ"
using modus_ponens biconditional_right_elimination ‹ψ ∈ set Φ›
by blast
moreover
from ‹ψ ∈ set Φ› ‹set Φ ⊆ set (ψ # Ψ)› Cons.hyps
have "⊢ ⨅ Ψ → ⨅ (removeAll ψ Φ)"
hence "⊢ (ψ ⊓ ⨅ Ψ) → (ψ ⊓ ⨅ (removeAll ψ Φ))"
unfolding conjunction_def
using
modus_ponens
hypothetical_syllogism
flip_hypothetical_syllogism
by meson
ultimately have "⊢ (ψ ⊓ ⨅ Ψ) → ⨅ Φ"
using modus_ponens hypothetical_syllogism
by blast
thus ?thesis
by simp
next
assume "ψ ∉ set Φ"
hence "⊢ ⨅ Ψ → ⨅ Φ"
using Cons.hyps ‹set Φ ⊆ set (ψ # Ψ)›
by auto
hence "⊢ (ψ ⊓ ⨅ Ψ) → ⨅ Φ"
unfolding conjunction_def
by (metis
modus_ponens
conjunction_def
conjunction_right_elimination
hypothetical_syllogism)
thus ?thesis
by simp
qed
}
thus ?case by blast
qed
thus "set Φ ⊆ set Ψ ⟹ ⊢ ⨅ Ψ → ⨅ Φ" by blast
qed

lemma (in classical_logic) arbitrary_conjunction_remdups:
"⊢ (⨅ Φ) ↔ ⨅ (remdups Φ)"

lemma (in classical_logic) curry_uncurry:
"⊢ (φ → ψ → χ) ↔ ((φ ⊓ ψ) → χ)"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ → ❙⟨ψ❙⟩ → ❙⟨χ❙⟩) ↔ ((❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) → ❙⟨χ❙⟩)"
by auto
hence "⊢ ❙⦇ (❙⟨φ❙⟩ → ❙⟨ψ❙⟩ → ❙⟨χ❙⟩) ↔ ((❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) → ❙⟨χ❙⟩) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) list_curry_uncurry:
"⊢ (Φ :→ χ) ↔ (⨅ Φ → χ)"
proof (induct Φ)
case Nil
have "⊢ χ ↔ (⊤ → χ)"
unfolding biconditional_def
conjunction_def
verum_def
using
axiom_k
ex_falso_quodlibet
modus_ponens
conjunction_def
excluded_middle_elimination
set_deduction_base_theory
conjunction_set_deduction_equivalence
by metis
with Nil show ?case
by simp
next
case (Cons φ Φ)
have "⊢ ((φ # Φ) :→ χ) ↔ (φ → (Φ :→ χ))"
with Cons have "⊢ ((φ # Φ) :→ χ) ↔ (φ → ⨅ Φ → χ)"
by (metis modus_ponens
biconditional_def
hypothetical_syllogism
list_implication.simps(2)
weak_conjunction_deduction_equivalence)
with curry_uncurry [where ?φ="φ"  and ?ψ="⨅ Φ" and ?χ="χ"]
show ?case
unfolding biconditional_def
by (simp, metis modus_ponens hypothetical_syllogism)
qed

subsection ‹ Disjunction Identities ›

lemma (in classical_logic) bivalence:
"⊢ ∼ φ ⊔ φ"
by (simp add: double_negation disjunction_def negation_def)

lemma (in classical_logic) implication_equivalence:
"⊢ (∼ φ ⊔ ψ) ↔ (φ → ψ)"
by (metis double_negation_converse
modus_ponens
biconditional_introduction
bivalence
disjunction_def
flip_hypothetical_syllogism
negation_def)

lemma (in classical_logic) disjunction_commutativity:
"⊢ (ψ ⊔ φ) ↔ (φ ⊔ ψ)"
by (meson modus_ponens
biconditional_introduction
disjunction_elimination
disjunction_left_introduction
disjunction_right_introduction)

lemma (in classical_logic) disjunction_associativity:
"⊢ ((φ ⊔ ψ) ⊔ χ) ↔ (φ ⊔ (ψ ⊔ χ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ((❙⟨φ❙⟩ ⊔ ❙⟨ψ❙⟩) ⊔ ❙⟨χ❙⟩) ↔ (❙⟨φ❙⟩ ⊔ (❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩))"
by simp
hence "⊢ ❙⦇ ((❙⟨φ❙⟩ ⊔ ❙⟨ψ❙⟩) ⊔ ❙⟨χ❙⟩) ↔ (❙⟨φ❙⟩ ⊔ (❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) arbitrary_disjunction_monotone:
"set Φ ⊆ set Ψ ⟹ ⊢ ⨆ Φ → ⨆ Ψ"
proof -
have "∀ Φ. set Φ ⊆ set Ψ ⟶ ⊢ ⨆ Φ → ⨆ Ψ"
proof (induct Ψ)
case Nil
then show ?case using verum_def verum_tautology by auto
next
case (Cons ψ Ψ)
{
fix Φ
assume "set Φ ⊆ set (ψ # Ψ)"
have "⊢ ⨆ Φ → ⨆ (ψ # Ψ)"
proof cases
assume "ψ ∈ set Φ"
have "∀ φ ∈ set Φ. ⊢ ⨆ Φ ↔ (φ ⊔ ⨆ (removeAll φ Φ))"
proof (induct Φ)
case Nil
then show ?case by simp
next
case (Cons χ Φ)
{
fix φ
assume "φ ∈ set (χ # Φ)"
have "⊢ ⨆ (χ # Φ) ↔ (φ ⊔ ⨆ (removeAll φ (χ # Φ)))"
proof cases
assume "φ ∈ set Φ"
hence "⊢ ⨆ Φ ↔ (φ ⊔ ⨆ (removeAll φ Φ))"
using Cons.hyps ‹φ ∈ set Φ›
by auto
moreover
have "⊢ (⨆ Φ ↔ (φ ⊔ ⨆ (removeAll φ Φ))) →
(χ ⊔ ⨆ Φ) ↔ (φ ⊔ χ ⊔ ⨆ (removeAll φ Φ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p
(❙⟨⨆ Φ❙⟩ ↔ (❙⟨φ❙⟩ ⊔ ❙⟨⨆ (removeAll φ Φ)❙⟩))
→ (❙⟨χ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)
↔ (❙⟨φ❙⟩ ⊔ ❙⟨χ❙⟩ ⊔ ❙⟨⨆ (removeAll φ Φ)❙⟩)"
by auto
hence "⊢ ❙⦇ (❙⟨⨆ Φ❙⟩ ↔ (❙⟨φ❙⟩ ⊔ ❙⟨⨆ (removeAll φ Φ)❙⟩))
→ (❙⟨χ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)
↔ (❙⟨φ❙⟩ ⊔ ❙⟨χ❙⟩ ⊔ ❙⟨⨆ (removeAll φ Φ)❙⟩) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed
ultimately have "⊢ ⨆ (χ # Φ) ↔ (φ ⊔ χ ⊔ ⨆ (removeAll φ Φ))"
using modus_ponens by auto
show ?thesis
proof cases
assume "φ = χ"
then show ?thesis
using ‹⊢ ⨆ (χ # Φ) ↔ (φ ⊔ χ ⊔ ⨆ (removeAll φ Φ))›
unfolding biconditional_def
meson
axiom_k
modus_ponens
flip_hypothetical_syllogism
implication_absorption)
next
assume "φ ≠ χ"
then show ?thesis
using ‹⊢ ⨆ (χ # Φ) ↔ (φ ⊔ χ ⊔ ⨆ (removeAll φ Φ))›
by simp
qed
next
assume "φ ∉ set Φ"
hence "φ = χ" "χ ∉ set Φ"
using ‹φ ∈ set (χ # Φ)› by auto
then show ?thesis
using biconditional_reflection
by simp
qed
}
thus ?case by blast
qed
hence "⊢ ⨆ Φ → (ψ ⊔ ⨆ (removeAll ψ Φ))"
using modus_ponens biconditional_left_elimination ‹ψ ∈ set Φ›
by blast
moreover
from ‹ψ ∈ set Φ› ‹set Φ ⊆ set (ψ # Ψ)› Cons.hyps
have "⊢ ⨆ (removeAll ψ Φ) → ⨆ Ψ"
hence "⊢ (ψ ⊔ ⨆ (removeAll ψ Φ)) → ⨆ (ψ # Ψ)"
using
modus_ponens
disjunction_def
hypothetical_syllogism
by fastforce
ultimately show ?thesis
by (simp, metis modus_ponens hypothetical_syllogism)
next
assume "ψ ∉ set Φ"
hence "⊢ ⨆ Φ → ⨆ Ψ"
using Cons.hyps ‹set Φ ⊆ set (ψ # Ψ)›
by auto
then show ?thesis
by (metis
arbitrary_disjunction.simps(2)
disjunction_def
list_deduction_def
list_deduction_theorem
list_deduction_weaken
list_implication.simps(1)
list_implication.simps(2))
qed
}
then show ?case by blast
qed
thus "set Φ ⊆ set Ψ ⟹ ⊢ ⨆ Φ → ⨆ Ψ" by blast
qed

lemma (in classical_logic) arbitrary_disjunction_remdups:
"⊢ (⨆ Φ) ↔ ⨆ (remdups Φ)"

lemma (in classical_logic) arbitrary_disjunction_exclusion_MCS:
assumes "MCS Ω"
shows "⨆ Ψ ∉ Ω ≡ ∀ ψ ∈ set Ψ. ψ ∉ Ω"
proof (induct Ψ)
case Nil
then show ?case
using
assms
formula_consistent_def
formula_maximally_consistent_set_def_def
maximally_consistent_set_def
set_deduction_reflection
by (simp, blast)
next
case (Cons ψ Ψ)
have "⨆ (ψ # Ψ) ∉ Ω = (ψ ∉ Ω ∧ ⨆ Ψ ∉ Ω)"
meson
assms
formula_consistent_def
formula_maximally_consistent_set_def_def
formula_maximally_consistent_set_def_implication
maximally_consistent_set_def
set_deduction_reflection)
thus ?case using Cons.hyps by simp
qed

lemma (in classical_logic) contra_list_curry_uncurry:
"⊢ (Φ :→ χ) ↔ (∼ χ → ⨆ (❙∼ Φ))"
proof (induct Φ)
case Nil
then show ?case
by (simp,
metis
biconditional_introduction
bivalence
disjunction_def
double_negation_converse
modus_ponens
negation_def)
next
case (Cons φ Φ)
hence "⊢ (⨅ Φ → χ) ↔ (∼ χ → ⨆ (❙∼ Φ))"
by (metis
biconditional_symmetry_rule
biconditional_transitivity_rule
list_curry_uncurry)
have "⊢ (⨅ (φ # Φ) → χ) ↔ (∼ χ → ⨆ (❙∼ (φ # Φ)))"
proof -
have "⊢ (⨅ Φ → χ) ↔ (∼ χ → ⨆ (❙∼ Φ))
→ ((φ ⊓ ⨅ Φ) → χ) ↔ (∼ χ → (∼ φ ⊔ ⨆ (❙∼ Φ)))"
proof -
have
"∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p
(❙⟨⨅ Φ❙⟩ → ❙⟨χ❙⟩) ↔ (∼ ❙⟨χ❙⟩ → ❙⟨⨆ (❙∼ Φ)❙⟩)
→ ((❙⟨φ❙⟩ ⊓ ❙⟨⨅ Φ❙⟩) → ❙⟨χ❙⟩) ↔ (∼ ❙⟨χ❙⟩ → (∼ ❙⟨φ❙⟩ ⊔ ❙⟨⨆ (❙∼ Φ)❙⟩))"
by auto
hence
"⊢ ❙⦇ (❙⟨⨅ Φ❙⟩ → ❙⟨χ❙⟩) ↔ (∼ ❙⟨χ❙⟩ → ❙⟨⨆ (❙∼ Φ)❙⟩)
→ ((❙⟨φ❙⟩ ⊓ ❙⟨⨅ Φ❙⟩) → ❙⟨χ❙⟩) ↔ (∼ ❙⟨χ❙⟩ → (∼ ❙⟨φ❙⟩ ⊔ ❙⟨⨆ (❙∼ Φ)❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed
thus ?thesis
using ‹⊢ (⨅ Φ → χ) ↔ (∼ χ → ⨆ (❙∼ Φ))› modus_ponens by auto
qed
then show ?case
using biconditional_transitivity_rule list_curry_uncurry by blast
qed

subsection ‹ Monotony of Conjunction and Disjunction ›

lemma (in classical_logic) conjunction_monotonic_identity:
"⊢ (φ → ψ) → (φ ⊓ χ) → (ψ ⊓ χ)"
unfolding conjunction_def
using modus_ponens
flip_hypothetical_syllogism
by blast

lemma (in classical_logic) conjunction_monotonic:
assumes "⊢ φ → ψ"
shows "⊢ (φ ⊓ χ) → (ψ ⊓ χ)"
using assms
modus_ponens
conjunction_monotonic_identity
by blast

lemma (in classical_logic) disjunction_monotonic_identity:
"⊢ (φ → ψ) → (φ ⊔ χ) → (ψ ⊔ χ)"
unfolding disjunction_def
using modus_ponens
flip_hypothetical_syllogism
by blast

lemma (in classical_logic) disjunction_monotonic:
assumes "⊢ φ → ψ"
shows "⊢ (φ ⊔ χ) → (ψ ⊔ χ)"
using assms
modus_ponens
disjunction_monotonic_identity
by blast

subsection ‹ Distribution Identities ›

lemma (in classical_logic) conjunction_distribution:
"⊢ ((ψ ⊔ χ) ⊓ φ) ↔ ((ψ ⊓ φ) ⊔ (χ ⊓ φ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ((❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩) ⊓ ❙⟨φ❙⟩) ↔ ((❙⟨ψ❙⟩ ⊓ ❙⟨φ❙⟩) ⊔ (❙⟨χ❙⟩ ⊓ ❙⟨φ❙⟩))"
by auto
hence "⊢ ❙⦇ ((❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩) ⊓ ❙⟨φ❙⟩) ↔ ((❙⟨ψ❙⟩ ⊓ ❙⟨φ❙⟩) ⊔ (❙⟨χ❙⟩ ⊓ ❙⟨φ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) subtraction_distribution:
"⊢ ((ψ ⊔ χ) ∖ φ) ↔ ((ψ ∖ φ) ⊔ (χ ∖ φ))"

lemma (in classical_logic) conjunction_arbitrary_distribution:
"⊢ (⨆ Ψ ⊓ φ) ↔ ⨆ [ψ ⊓ φ. ψ ← Ψ]"
proof (induct Ψ)
case Nil
then show ?case
biconditional_def
conjunction_left_elimination)
next
case (Cons ψ Ψ)
have "⊢ (⨆ (ψ # Ψ) ⊓ φ) ↔ ((ψ ⊓ φ) ⊔ ((⨆ Ψ) ⊓ φ))"
using conjunction_distribution by auto
moreover
from Cons have
"⊢ ((ψ ⊓ φ) ⊔ ((⨆ Ψ) ⊓ φ)) ↔ ((ψ ⊓ φ) ⊔ (⨆ [ψ ⊓ φ. ψ ← Ψ]))"
unfolding disjunction_def biconditional_def
by (simp, meson modus_ponens hypothetical_syllogism)
ultimately show ?case
by (simp, metis biconditional_transitivity_rule)
qed

lemma (in classical_logic) subtraction_arbitrary_distribution:
"⊢ (⨆ Ψ ∖ φ) ↔ ⨆ [ψ ∖ φ. ψ ← Ψ]"

lemma (in classical_logic) disjunction_distribution:
"⊢ (φ ⊔ (ψ ⊓ χ)) ↔ ((φ ⊔ ψ) ⊓ (φ ⊔ χ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ ⊔ (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ↔ ((❙⟨φ❙⟩ ⊔ ❙⟨ψ❙⟩) ⊓ (❙⟨φ❙⟩ ⊔ ❙⟨χ❙⟩))"
by auto
hence "⊢ ❙⦇ (❙⟨φ❙⟩ ⊔ (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ↔ ((❙⟨φ❙⟩ ⊔ ❙⟨ψ❙⟩) ⊓ (❙⟨φ❙⟩ ⊔ ❙⟨χ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) implication_distribution:
"⊢ (φ → (ψ ⊓ χ)) ↔ ((φ → ψ) ⊓ (φ → χ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ → (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ↔ ((❙⟨φ❙⟩ → ❙⟨ψ❙⟩) ⊓ (❙⟨φ❙⟩ → ❙⟨χ❙⟩))"
by auto
hence "⊢ ❙⦇ (❙⟨φ❙⟩ → (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ↔ ((❙⟨φ❙⟩ → ❙⟨ψ❙⟩) ⊓ (❙⟨φ❙⟩ → ❙⟨χ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) list_implication_distribution:
"⊢ (Φ :→ (ψ ⊓ χ)) ↔ ((Φ :→ ψ) ⊓ (Φ :→ χ))"
proof (induct Φ)
case Nil
then show ?case
next
case (Cons φ Φ)
hence " ⊢ (φ # Φ) :→ (ψ ⊓ χ) ↔ (φ → (Φ :→ ψ ⊓ Φ :→ χ))"
by (metis
modus_ponens
biconditional_def
hypothetical_syllogism
list_implication.simps(2)
weak_conjunction_deduction_equivalence)
moreover
have "⊢ (φ → (Φ :→ ψ ⊓ Φ :→ χ)) ↔ (((φ # Φ) :→ ψ) ⊓ ((φ # Φ) :→ χ))"
using implication_distribution by auto
ultimately show ?case
by (simp, metis biconditional_transitivity_rule)
qed

lemma (in classical_logic) biconditional_conjunction_weaken:
"⊢ (α ↔ β) → ((γ ⊓ α) ↔ (γ ⊓ β))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨α❙⟩ ↔ ❙⟨β❙⟩) → ((❙⟨γ❙⟩ ⊓ ❙⟨α❙⟩) ↔ (❙⟨γ❙⟩ ⊓ ❙⟨β❙⟩))"
by auto
hence "⊢ ❙⦇ (❙⟨α❙⟩ ↔ ❙⟨β❙⟩) → ((❙⟨γ❙⟩ ⊓ ❙⟨α❙⟩) ↔ (❙⟨γ❙⟩ ⊓ ❙⟨β❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) biconditional_conjunction_weaken_rule:
"⊢ (α ↔ β) ⟹ ⊢ (γ ⊓ α) ↔ (γ ⊓ β)"
using modus_ponens biconditional_conjunction_weaken by blast

lemma (in classical_logic) disjunction_arbitrary_distribution:
"⊢ (φ ⊔ ⨅ Ψ) ↔ ⨅ [φ ⊔ ψ. ψ ← Ψ]"
proof (induct Ψ)
case Nil
then show ?case
unfolding disjunction_def biconditional_def
using axiom_k modus_ponens verum_tautology
by (simp, blast)
next
case (Cons ψ Ψ)
have "⊢ (φ ⊔ ⨅ (ψ # Ψ)) ↔ ((φ ⊔ ψ) ⊓ (φ ⊔ ⨅ Ψ))"
moreover
from biconditional_conjunction_weaken_rule
Cons
have " ⊢ ((φ ⊔ ψ) ⊓ φ ⊔ ⨅ Ψ) ↔ ⨅ (map (λ χ . φ ⊔ χ) (ψ # Ψ))"
by simp
ultimately show ?case
by (metis biconditional_transitivity_rule)
qed

lemma (in classical_logic) list_implication_arbitrary_distribution:
"⊢ (Φ :→ ⨅ Ψ) ↔ ⨅ [Φ :→ ψ. ψ ← Ψ]"
proof (induct Ψ)
case Nil
then show ?case
meson
axiom_k
modus_ponens
list_implication_axiom_k
verum_tautology)
next
case (Cons ψ Ψ)
have "⊢ Φ :→ ⨅ (ψ # Ψ) ↔ (Φ :→ ψ ⊓ Φ :→ ⨅ Ψ)"
using list_implication_distribution
by fastforce
moreover
from biconditional_conjunction_weaken_rule
Cons
have "⊢ (Φ :→ ψ ⊓ Φ :→ ⨅ Ψ) ↔ ⨅ [Φ :→ ψ. ψ ← (ψ # Ψ)]"
by simp
ultimately show ?case
by (metis biconditional_transitivity_rule)
qed

lemma (in classical_logic) implication_arbitrary_distribution:
"⊢ (φ → ⨅ Ψ) ↔ ⨅ [φ → ψ. ψ ← Ψ]"
using list_implication_arbitrary_distribution [where ?Φ="[φ]"]
by simp

subsection ‹ Negation ›

lemma (in classical_logic) double_negation_biconditional:
"⊢ ∼ (∼ φ) ↔ φ"
unfolding biconditional_def negation_def

lemma (in classical_logic) double_negation_elimination [simp]:
"Γ ⊩ ∼ (∼ φ) = Γ ⊩ φ"
using
set_deduction_weaken
biconditional_weaken
double_negation_biconditional
by metis

lemma (in classical_logic) alt_double_negation_elimination [simp]:
"Γ ⊩ (φ → ⊥) → ⊥ ≡ Γ ⊩ φ"
using double_negation_elimination
unfolding negation_def
by auto

lemma (in classical_logic) base_double_negation_elimination [simp]:
"⊢ ∼ (∼ φ) = ⊢ φ"
by (metis double_negation_elimination set_deduction_base_theory)

lemma (in classical_logic) alt_base_double_negation_elimination [simp]:
"⊢ (φ → ⊥) → ⊥ ≡ ⊢ φ"
using base_double_negation_elimination
unfolding negation_def
by auto

subsection ‹ Mutual Exclusion Identities ›

lemma (in classical_logic) exclusion_contrapositive_equivalence:
"⊢ (φ → γ) ↔ ∼ (φ ⊓ ∼ γ)"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ → ❙⟨γ❙⟩) ↔ ∼ (❙⟨φ❙⟩ ⊓ ∼ ❙⟨γ❙⟩)"
by auto
hence "⊢ ❙⦇ (❙⟨φ❙⟩ → ❙⟨γ❙⟩) ↔ ∼ (❙⟨φ❙⟩ ⊓ ∼ ❙⟨γ❙⟩) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed

lemma (in classical_logic) disjuction_exclusion_equivalence:
"Γ ⊩ ∼ (ψ ⊓ ⨆ Φ) ≡ ∀ φ ∈ set Φ. Γ ⊩ ∼ (ψ ⊓ φ)"
proof (induct Φ)
case Nil
then show ?case
conjunction_right_elimination
negation_def
set_deduction_weaken)
next
case (Cons φ Φ)
have "⊢ ∼ (ψ ⊓ ⨆ (φ # Φ)) ↔ ∼ (ψ ⊓ (φ ⊔ ⨆ Φ))"
moreover have "⊢ ∼ (ψ ⊓ (φ ⊔ ⨆ Φ)) ↔ (∼ (ψ ⊓ φ) ⊓ ∼ (ψ ⊓ ⨆ Φ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ∼ (❙⟨ψ❙⟩ ⊓ (❙⟨φ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))
↔ (∼ (❙⟨ψ❙⟩ ⊓ ❙⟨φ❙⟩) ⊓ ∼ (❙⟨ψ❙⟩ ⊓ ❙⟨⨆ Φ❙⟩))"
by auto
hence "⊢ ❙⦇ ∼ (❙⟨ψ❙⟩ ⊓ (❙⟨φ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))
↔ (∼ (❙⟨ψ❙⟩ ⊓ ❙⟨φ❙⟩) ⊓ ∼ (❙⟨ψ❙⟩ ⊓ ❙⟨⨆ Φ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed
ultimately
have "⊢ ∼ (ψ ⊓ ⨆ (φ # Φ)) ↔ (∼ (ψ ⊓ φ) ⊓ ∼ (ψ ⊓ ⨆ Φ))"
by simp
hence "Γ ⊩ ∼ (ψ ⊓ ⨆ (φ # Φ)) = (Γ ⊩ ∼ (ψ ⊓ φ)
∧ (∀φ∈set Φ. Γ ⊩ ∼ (ψ ⊓ φ)))"
using set_deduction_weaken [where Γ="Γ"]
conjunction_set_deduction_equivalence [where Γ="Γ"]
Cons.hyps
biconditional_def
set_deduction_modus_ponens
by metis
thus "Γ ⊩ ∼ (ψ ⊓ ⨆ (φ # Φ)) = (∀φ∈set (φ # Φ). Γ ⊩ ∼ (ψ ⊓ φ))"
by simp
qed

lemma (in classical_logic) exclusive_elimination1:
assumes "Γ ⊩ ∐ Φ"
shows "∀ φ ∈ set Φ. ∀ ψ ∈ set Φ. (φ ≠ ψ) ⟶ Γ ⊩ ∼ (φ ⊓ ψ)"
using assms
proof (induct Φ)
case Nil
thus ?case by auto
next
case (Cons χ Φ)
assume "Γ ⊩ ∐ (χ # Φ)"
hence "Γ ⊩ ∐ Φ" by simp
hence "∀φ∈set Φ. ∀ψ∈set Φ. φ ≠ ψ ⟶ Γ ⊩ ∼ (φ ⊓ ψ)"
using Cons.hyps by blast
moreover have "Γ ⊩ ∼ (χ ⊓ ⨆ Φ)"
using ‹Γ ⊩ ∐ (χ # Φ)› conjunction_set_deduction_equivalence by auto
hence "∀ φ ∈ set Φ. Γ ⊩ ∼ (χ ⊓ φ)"
using disjuction_exclusion_equivalence by auto
moreover {
fix φ
have "⊢ ∼ (χ ⊓ φ) → ∼ (φ ⊓ χ)"
unfolding negation_def
conjunction_def
using modus_ponens flip_hypothetical_syllogism flip_implication by blast
}
with ‹∀ φ ∈ set Φ. Γ ⊩ ∼ (χ ⊓ φ)› have "∀ φ ∈ set Φ. Γ ⊩ ∼ (φ ⊓ χ)"
using set_deduction_weaken [where Γ="Γ"]
set_deduction_modus_ponens [where Γ="Γ"]
by blast
ultimately
show "∀φ ∈ set (χ # Φ). ∀ψ ∈ set (χ # Φ). φ ≠ ψ ⟶ Γ ⊩ ∼ (φ ⊓ ψ)"
by simp
qed

lemma (in classical_logic) exclusive_elimination2:
assumes "Γ ⊩ ∐ Φ"
shows "∀ φ ∈ duplicates Φ. Γ ⊩ ∼ φ"
using assms
proof (induct Φ)
case Nil
then show ?case by simp
next
case (Cons φ Φ)
assume "Γ ⊩ ∐ (φ # Φ)"
hence "Γ ⊩ ∐ Φ" by simp
hence "∀φ∈duplicates Φ. Γ ⊩ ∼ φ" using Cons.hyps by auto
show ?case
proof cases
assume "φ ∈ set Φ"
moreover {
fix φ ψ χ
have "⊢ ∼ (φ ⊓ (ψ ⊔ χ)) ↔ (∼ (φ ⊓ ψ) ⊓ ∼ (φ ⊓ χ))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩))
↔ (∼ (❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) ⊓ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨χ❙⟩))"
by auto
hence "⊢ ❙⦇ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩)) ↔ (∼ (❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) ⊓ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨χ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed
hence "Γ ⊩ ∼ (φ ⊓ (ψ ⊔ χ)) ≡ Γ ⊩ ∼ (φ ⊓ ψ) ⊓ ∼ (φ ⊓ χ)"
using set_deduction_weaken
biconditional_weaken by presburger
}
moreover
have "⊢ ∼ (φ ⊓ φ) ↔ ∼ φ"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ∼ (❙⟨φ❙⟩ ⊓ ❙⟨φ❙⟩) ↔ ∼ ❙⟨φ❙⟩"
by auto
hence "⊢ ❙⦇ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨φ❙⟩) ↔ ∼ ❙⟨φ❙⟩ ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed
hence "Γ ⊩ ∼ (φ ⊓ φ) ≡ Γ ⊩ ∼ φ"
using set_deduction_weaken
biconditional_weaken by presburger
moreover have "Γ ⊩ ∼ (φ ⊓ ⨆ Φ)" using ‹Γ ⊩ ∐ (φ # Φ)› by simp
ultimately have "Γ ⊩ ∼ φ" by (induct Φ, simp, simp, blast)
thus ?thesis using ‹φ ∈ set Φ› ‹∀φ∈duplicates Φ. Γ ⊩ ∼ φ› by simp
next
assume "φ ∉ set Φ"
hence "duplicates (φ # Φ) = duplicates Φ" by simp
then show ?thesis using ‹∀φ∈duplicates Φ. Γ ⊩ ∼ φ›
by auto
qed
qed

lemma (in classical_logic) exclusive_equivalence:
"Γ ⊩ ∐ Φ =
((∀φ∈duplicates Φ. Γ ⊩ ∼ φ) ∧
(∀ φ ∈ set Φ. ∀ ψ ∈ set Φ. (φ ≠ ψ) ⟶ Γ ⊩ ∼ (φ ⊓ ψ)))"
proof -
{
assume "∀φ∈duplicates Φ. Γ ⊩ ∼ φ"
"∀ φ ∈ set Φ. ∀ ψ ∈ set Φ. (φ ≠ ψ) ⟶ Γ ⊩ ∼ (φ ⊓ ψ)"
hence "Γ ⊩ ∐ Φ"
proof (induct Φ)
case Nil
then show ?case
next
case (Cons φ Φ)
assume A: "∀φ∈duplicates (φ # Φ). Γ ⊩ ∼ φ"
and B: "∀χ∈set (φ # Φ). ∀ψ∈set (φ # Φ). χ ≠ ψ ⟶ Γ ⊩ ∼ (χ ⊓ ψ)"
hence C: "Γ ⊩ ∐ Φ" using Cons.hyps by simp
then show ?case
proof cases
assume "φ ∈ duplicates (φ # Φ)"
moreover from this have "Γ ⊩ ∼ φ" using A by auto
moreover have "duplicates Φ ⊆ set Φ" by (induct Φ, simp, auto)
ultimately have "φ ∈ set Φ" by (metis duplicates.simps(2) subsetCE)
hence "⊢ ∼ φ ↔ ∼(φ ⊓ ⨆ Φ)"
proof (induct Φ)
case Nil
then show ?case by simp
next
case (Cons ψ Φ)
assume "φ ∈ set (ψ # Φ)"
then show "⊢ ∼ φ ↔ ∼ (φ ⊓ ⨆ (ψ # Φ))"
proof -
{
assume "φ = ψ"
hence ?thesis
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))"
using ‹φ = ψ› by auto
hence "⊢ ❙⦇ ∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed
}
moreover
{
assume "φ ≠ ψ"
hence "φ ∈ set Φ" using ‹φ ∈ set (ψ # Φ)› by auto
hence "⊢ ∼ φ ↔ ∼ (φ ⊓ ⨆ Φ)" using Cons.hyps by auto
moreover have "⊢ (∼ φ ↔ ∼ (φ ⊓ ⨆ Φ))
→ (∼ φ ↔ ∼ (φ ⊓ (ψ ⊔ ⨆ Φ)))"
proof -
have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨⨆ Φ❙⟩)) →
(∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)))"
by auto
hence "⊢ ❙⦇ (∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨⨆ Φ❙⟩))
→ (∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))) ❙⦈"
using propositional_semantics by blast
thus ?thesis by simp
qed
ultimately have ?thesis using modus_ponens by simp
}
ultimately show ?thesis by auto
qed
qed
with ‹Γ ⊩ ∼ φ› have "Γ ⊩ ∼(φ ⊓ ⨆ Φ)"
using biconditional_weaken set_deduction_weaken by blast
with ‹Γ ⊩ ∐ Φ› show ?thesis by simp
next
assume "φ ∉ duplicates (φ # Φ)"
hence "φ ∉ set Φ" by auto
with B have "∀ψ∈set Φ. Γ ⊩ ∼ (φ ⊓ ψ)" by (simp, metis)
hence "Γ ⊩ ∼ (φ ⊓ ⨆ Φ)"
with ‹Γ ⊩ ∐ Φ› show ?thesis by simp
qed
qed
}
thus ?thesis
by (metis exclusive_elimination1 exclusive_elimination2)
qed

subsection ‹ Miscellaneous Disjunctive Normal Form Identities ›

lemma (in classical_logic) map_negation_list_implication:
"⊢ ((❙∼ Φ) :→ (∼ φ)) ↔ (φ → ⨆ Φ)"
proof (induct Φ)
case Nil
then show ?case
unfolding
biconditional_def
map_negation_def
negation_def
using
conjunction_introduction
modus_ponens
trivial_implication
by simp
next
case (Cons ψ Φ)
have "⊢ (❙∼ Φ :→ ∼ φ ↔ (φ → ⨆ Φ))
→ (∼ ψ → ❙∼ Φ :→ ∼ φ) ↔ (φ → (ψ ⊔ ⨆ Φ))"
proof -
have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨❙∼ Φ :→ ∼ φ❙⟩ ↔ (❙⟨φ❙⟩ → ❙⟨⨆ Φ❙⟩)) →
(∼ ❙⟨ψ❙⟩ → ❙⟨❙∼ Φ :→ ∼ φ❙⟩) ↔ (❙⟨φ❙⟩ → (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))"
by fastforce
hence "⊢ ❙⦇ (❙⟨❙∼ Φ :→ ∼ φ❙⟩ ↔ (❙⟨φ❙⟩ → ❙⟨⨆ Φ❙⟩)) →
(∼ ❙⟨ψ❙⟩ → ❙⟨❙∼ Φ :→ ∼ φ❙⟩) ↔ (❙⟨φ❙⟩ → (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)) ❙⦈"
using propositional_semantics by blast
thus ?thesis
by simp
qed
with Cons show ?case
by (metis
map_negation_def
list.simps(9)
arbitrary_disjunction.simps(2)
modus_ponens
list_implication.simps(2))
qed

lemma (in classical_logic) conj_dnf_distribute:
"⊢ ⨆ (map (⨅ ∘ (λ φs. φ # φs)) Λ) ↔ (φ ⊓ ⨆ (map ⨅ Λ))"
proof(induct Λ)
case Nil
have "⊢ ⊥ ↔ (φ ⊓ ⊥)"
proof -
let ?φ = "⊥ ↔ (❙⟨φ❙⟩ ⊓ ⊥)"
have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ?φ" by fastforce
hence "⊢ ❙⦇ ?φ ❙⦈" using propositional_semantics by blast
thus ?thesis by simp
qed
then show ?case by simp
next
case (Cons Ψ Λ)
assume "⊢ ⨆ (map (⨅ ∘ (λ φs. φ # φs)) Λ) ↔ (φ ⊓ ⨆ (map ⨅ Λ))"
(is "⊢ ?A ↔ (φ ⊓ ?B)")
moreover
have "⊢ (?A ↔ (φ ⊓ ?B)) → (((φ ⊓ ⨅ Ψ) ⊔ ?A) ↔ (φ ⊓ ⨅ Ψ ⊔ ?B))"
proof -
let ?φ = "(❙⟨?A❙⟩ ↔ (❙⟨φ❙⟩ ⊓ ❙⟨?B❙⟩)) →
(((❙⟨φ❙⟩ ⊓ ❙⟨⨅ Ψ❙⟩) ⊔ ❙⟨?A❙⟩) ↔ (❙⟨φ❙⟩ ⊓ ❙⟨⨅ Ψ❙⟩ ⊔ ❙⟨?B❙⟩))"
have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ?φ" by fastforce
hence "⊢ ❙⦇ ?φ ❙⦈" using propositional_semantics by blast
thus ?thesis
by simp
qed
ultimately have "⊢ ((φ ⊓ ⨅ Ψ) ⊔ ?A) ↔ (φ ⊓ ⨅ Ψ ⊔ ?B)"
using modus_ponens
by blast
moreover
have "map (⨅ ∘ (λ φs. φ # φs)) Λ = map (λΨ. φ ⊓ ⨅ Ψ) Λ" by simp
ultimately show ?case by simp
qed

lemma (in classical_logic) append_dnf_distribute:
"⊢ ⨆ (map (⨅ ∘ (λ Ψ. Φ @ Ψ)) Λ) ↔ (⨅ Φ ⊓ ⨆ (map ⨅ Λ))"
proof(induct Φ)
case Nil
have "⊢ ⨆ (map ⨅ Λ) ↔ (⊤ ⊓ ⨆ (map ⨅ Λ))"
(is "⊢ ?A ↔ (⊤ ⊓ ?A)")
proof -
let ?φ = "❙⟨?A❙⟩ ↔ ((⊥ → ⊥) ⊓ ❙⟨?A❙⟩)"
have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ?φ" by simp
hence "⊢ ❙⦇ ?φ ❙⦈" using propositional_semantics by blast
thus ?thesis
unfolding verum_def
by simp
qed
then show ?case by simp
next
case (Cons φ Φ)
have "⊢ ⨆ (map (⨅ ∘ (@) Φ) Λ) ↔ (⨅ Φ ⊓ ⨆ (map ⨅ Λ))
= ⊢ ⨆ (map ⨅ (map ((@) Φ) Λ)) ↔ (⨅ Φ ⊓ ⨆ (map ⨅ Λ))"
by simp
with Cons have
"⊢ ⨆ (map ⨅ (map (λ Ψ. Φ @ Ψ) Λ)) ↔ (⨅ Φ ⊓ ⨆ (map ⨅ Λ))"
(is "⊢ ⨆ (map ⨅ ?A) ↔ (?B ⊓ ?C)")
by meson
moreover have "⊢ ⨆ (map ⨅ ?A) ↔ (?B ⊓ ?C)
→ (⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A) ↔ (φ ⊓ ⨆ (map ⨅ ?A)))
→ ⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A) ↔ ((φ ⊓ ?B) ⊓ ?C)"
proof -
let ?φ = "❙⟨⨆ (map ⨅ ?A)❙⟩ ↔ (❙⟨?B❙⟩ ⊓ ❙⟨?C❙⟩)
→ (❙⟨⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A)❙⟩ ↔ (❙⟨φ❙⟩ ⊓ ❙⟨⨆ (map ⨅ ?A)❙⟩))
→ ❙⟨⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A)❙⟩ ↔ ((❙⟨φ❙⟩ ⊓ ❙⟨?B❙⟩) ⊓ ❙⟨?C❙⟩)"
have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ?φ" by simp
hence "⊢ ❙⦇ ?φ ❙⦈" using propositional_semantics by blast
thus ?thesis
by simp
qed
ultimately have "⊢ ⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A) ↔ ((φ ⊓ ?B) ⊓ ?C)"
using modus_ponens conj_dnf_distribute
by blast
moreover
have "⨅ ∘ (@) (φ # Φ) = ⨅ ∘ (#) φ ∘ (@) Φ" by auto
hence
"⊢ ⨆ (map (⨅ ∘ (@) (φ # Φ)) Λ) ↔ (⨅ (φ # Φ) ⊓ ?C)
= ⊢ ⨆ (map (⨅ ∘ (#) φ) ?A) ↔ ((φ ⊓ ?B) ⊓ ?C)"
by simp
ultimately show ?case by meson
qed

notation FuncSet.funcset (infixr "→" 60)

end