Theory TAO_9_PLM

(*<*)
theory TAO_9_PLM
imports
TAO_8_Definitions
"HOL-Eisbach.Eisbach_Tools"
begin
(*>*)

section‹The Deductive System PLM›
text‹\label{TAO_PLM}›

declare meta_defs[no_atp] meta_aux[no_atp]

locale PLM = Axioms
begin

subsection‹Automatic Solver›
text‹\label{TAO_PLM_Solver}›

named_theorems PLM
named_theorems PLM_intro
named_theorems PLM_elim
named_theorems PLM_dest
named_theorems PLM_subst

method PLM_solver declares PLM_intro PLM_elim PLM_subst PLM_dest PLM
= ((assumption | (match axiom in A: "[[φ]]" for φ ⇒ ‹fact A[axiom_instance]›)
| fact PLM | rule PLM_intro | subst PLM_subst | subst (asm) PLM_subst
| fastforce | safe | drule PLM_dest | erule PLM_elim); (PLM_solver)?)

subsection‹Modus Ponens›
text‹\label{TAO_PLM_ModusPonens}›

lemma modus_ponens[PLM]:
"⟦[φ in v]; [φ ❙→ ψ in v]⟧ ⟹ [ψ in v]"

subsection‹Axioms›
text‹\label{TAO_PLM_Axioms}›

interpretation Axioms .
declare axiom[PLM]
declare conn_defs[PLM]

subsection‹(Modally Strict) Proofs and Derivations›
text‹\label{TAO_PLM_ProofsAndDerivations}›

lemma vdash_properties_6[no_atp]:
"⟦[φ in v]; [φ ❙→ ψ in v]⟧ ⟹ [ψ in v]"
using modus_ponens .
lemma vdash_properties_9[PLM]:
"[φ in v] ⟹ [ψ ❙→ φ in v]"
using modus_ponens pl_1[axiom_instance] by blast
lemma vdash_properties_10[PLM]:
"[φ ❙→ ψ in v] ⟹ ([φ in v] ⟹ [ψ in v])"
using vdash_properties_6 .

attribute_setup deduction = ‹
Scan.succeed (Thm.rule_attribute []
(fn _ => fn thm => thm RS @{thm vdash_properties_10}))
›

subsection‹GEN and RN›
text‹\label{TAO_PLM_GEN_RN}›

lemma rule_gen[PLM]:
"⟦⋀α . [φ α in v]⟧ ⟹ [❙∀α . φ α in v]"

lemma RN_2[PLM]:
"(⋀ v . [ψ in v] ⟹ [φ in v]) ⟹ ([❙□ψ in v] ⟹ [❙□φ in v])"

lemma RN[PLM]:
"(⋀ v . [φ in v]) ⟹ [❙□φ in v]"
using qml_3[axiom_necessitation, axiom_instance] RN_2 by blast

subsection‹Negations and Conditionals›
text‹\label{TAO_PLM_NegationsAndConditionals}›

lemma if_p_then_p[PLM]:
"[φ ❙→ φ in v]"
using pl_1 pl_2 vdash_properties_10 axiom_instance by blast

lemma deduction_theorem[PLM,PLM_intro]:
"⟦[φ in v] ⟹ [ψ in v]⟧ ⟹ [φ ❙→ ψ in v]"
lemmas CP = deduction_theorem

lemma ded_thm_cor_3[PLM]:
"⟦[φ ❙→ ψ in v]; [ψ ❙→ χ in v]⟧ ⟹ [φ ❙→ χ in v]"
by (meson pl_2 vdash_properties_10 vdash_properties_9 axiom_instance)
lemma ded_thm_cor_4[PLM]:
"⟦[φ ❙→ (ψ ❙→ χ) in v]; [ψ in v]⟧ ⟹ [φ ❙→ χ in v]"
by (meson pl_2 vdash_properties_10 vdash_properties_9 axiom_instance)

lemma useful_tautologies_1[PLM]:
"[❙¬❙¬φ ❙→ φ in v]"
by (meson pl_1 pl_3 ded_thm_cor_3 ded_thm_cor_4 axiom_instance)
lemma useful_tautologies_2[PLM]:
"[φ ❙→ ❙¬❙¬φ in v]"
by (meson pl_1 pl_3 ded_thm_cor_3 useful_tautologies_1
vdash_properties_10 axiom_instance)
lemma useful_tautologies_3[PLM]:
"[❙¬φ ❙→ (φ ❙→ ψ) in v]"
by (meson pl_1 pl_2 pl_3 ded_thm_cor_3 ded_thm_cor_4 axiom_instance)
lemma useful_tautologies_4[PLM]:
"[(❙¬ψ ❙→ ❙¬φ) ❙→ (φ ❙→ ψ) in v]"
by (meson pl_1 pl_2 pl_3 ded_thm_cor_3 ded_thm_cor_4 axiom_instance)
lemma useful_tautologies_5[PLM]:
"[(φ ❙→ ψ) ❙→ (❙¬ψ ❙→ ❙¬φ) in v]"
by (metis CP useful_tautologies_4 vdash_properties_10)
lemma useful_tautologies_6[PLM]:
"[(φ ❙→ ❙¬ψ) ❙→ (ψ ❙→ ❙¬φ) in v]"
by (metis CP useful_tautologies_4 vdash_properties_10)
lemma useful_tautologies_7[PLM]:
"[(❙¬φ ❙→ ψ) ❙→ (❙¬ψ ❙→ φ) in v]"
using ded_thm_cor_3 useful_tautologies_4 useful_tautologies_5
useful_tautologies_6 by blast
lemma useful_tautologies_8[PLM]:
"[φ ❙→ (❙¬ψ ❙→ ❙¬(φ ❙→ ψ)) in v]"
by (meson ded_thm_cor_3 CP useful_tautologies_5)
lemma useful_tautologies_9[PLM]:
"[(φ ❙→ ψ) ❙→ ((❙¬φ ❙→ ψ) ❙→ ψ) in v]"
by (metis CP useful_tautologies_4 vdash_properties_10)
lemma useful_tautologies_10[PLM]:
"[(φ ❙→ ❙¬ψ) ❙→ ((φ ❙→ ψ) ❙→ ❙¬φ) in v]"
by (metis ded_thm_cor_3 CP useful_tautologies_6)

lemma modus_tollens_1[PLM]:
"⟦[φ ❙→ ψ in v]; [❙¬ψ in v]⟧ ⟹ [❙¬φ in v]"
by (metis ded_thm_cor_3 ded_thm_cor_4 useful_tautologies_3
useful_tautologies_7 vdash_properties_10)
lemma modus_tollens_2[PLM]:
"⟦[φ ❙→ ❙¬ψ in v]; [ψ in v]⟧ ⟹ [❙¬φ in v]"
using modus_tollens_1 useful_tautologies_2
vdash_properties_10 by blast

lemma contraposition_1[PLM]:
"[φ ❙→ ψ in v] = [❙¬ψ ❙→ ❙¬φ in v]"
using useful_tautologies_4 useful_tautologies_5
vdash_properties_10 by blast
lemma contraposition_2[PLM]:
"[φ ❙→ ❙¬ψ in v] = [ψ ❙→ ❙¬φ in v]"
using contraposition_1 ded_thm_cor_3
useful_tautologies_1 by blast

lemma reductio_aa_1[PLM]:
"⟦[❙¬φ in v] ⟹ [❙¬ψ in v]; [❙¬φ in v] ⟹ [ψ in v]⟧ ⟹ [φ in v]"
using CP modus_tollens_2 useful_tautologies_1
vdash_properties_10 by blast
lemma reductio_aa_2[PLM]:
"⟦[φ in v] ⟹ [❙¬ψ in v]; [φ in v] ⟹ [ψ in v]⟧ ⟹ [❙¬φ in v]"
by (meson contraposition_1 reductio_aa_1)
lemma reductio_aa_3[PLM]:
"⟦[❙¬φ ❙→ ❙¬ψ in v]; [❙¬φ ❙→ ψ in v]⟧ ⟹ [φ in v]"
using reductio_aa_1 vdash_properties_10 by blast
lemma reductio_aa_4[PLM]:
"⟦[φ ❙→ ❙¬ψ in v]; [φ ❙→ ψ in v]⟧ ⟹ [❙¬φ in v]"
using reductio_aa_2 vdash_properties_10 by blast

lemma raa_cor_1[PLM]:
"⟦[φ in v]; [❙¬ψ in v] ⟹ [❙¬φ in v]⟧ ⟹ ([φ in v] ⟹ [ψ in v])"
using reductio_aa_1 vdash_properties_9 by blast
lemma raa_cor_2[PLM]:
"⟦[❙¬φ in v]; [❙¬ψ in v] ⟹ [φ in v]⟧ ⟹ ([❙¬φ in v] ⟹ [ψ in v])"
using reductio_aa_1 vdash_properties_9 by blast
lemma raa_cor_3[PLM]:
"⟦[φ in v]; [❙¬ψ ❙→ ❙¬φ in v]⟧ ⟹ ([φ in v] ⟹ [ψ in v])"
using raa_cor_1 vdash_properties_10 by blast
lemma raa_cor_4[PLM]:
"⟦[❙¬φ in v]; [❙¬ψ ❙→ φ in v]⟧ ⟹ ([❙¬φ in v] ⟹ [ψ in v])"
using raa_cor_2 vdash_properties_10 by blast

text‹
\begin{remark}
In contrast to PLM the classical introduction and elimination rules are proven
before the tautologies. The statements proven so far are sufficient
for the proofs and using the derived rules the tautologies can be derived
automatically.
\end{remark}
›

lemma intro_elim_1[PLM]:
"⟦[φ in v]; [ψ in v]⟧ ⟹ [φ ❙& ψ in v]"
unfolding conj_def using ded_thm_cor_4 if_p_then_p modus_tollens_2 by blast
lemmas "❙&I" = intro_elim_1
lemma intro_elim_2_a[PLM]:
"[φ ❙& ψ in v] ⟹ [φ in v]"
unfolding conj_def using CP reductio_aa_1 by blast
lemma intro_elim_2_b[PLM]:
"[φ ❙& ψ in v] ⟹ [ψ in v]"
unfolding conj_def using pl_1 CP reductio_aa_1 axiom_instance by blast
lemmas "❙&E" = intro_elim_2_a intro_elim_2_b
lemma intro_elim_3_a[PLM]:
"[φ in v] ⟹ [φ ❙∨ ψ in v]"
unfolding disj_def using ded_thm_cor_4 useful_tautologies_3 by blast
lemma intro_elim_3_b[PLM]:
"[ψ in v] ⟹ [φ ❙∨ ψ in v]"
by (simp only: disj_def vdash_properties_9)
lemmas "❙∨I" = intro_elim_3_a intro_elim_3_b
lemma intro_elim_4_a[PLM]:
"⟦[φ ❙∨ ψ in v]; [φ ❙→ χ in v]; [ψ ❙→ χ in v]⟧ ⟹ [χ in v]"
unfolding disj_def by (meson reductio_aa_2 vdash_properties_10)
lemma intro_elim_4_b[PLM]:
"⟦[φ ❙∨ ψ in v]; [❙¬φ in v]⟧ ⟹ [ψ in v]"
unfolding disj_def using vdash_properties_10 by blast
lemma intro_elim_4_c[PLM]:
"⟦[φ ❙∨ ψ in v]; [❙¬ψ in v]⟧ ⟹ [φ in v]"
unfolding disj_def using raa_cor_2 vdash_properties_10 by blast
lemma intro_elim_4_d[PLM]:
"⟦[φ ❙∨ ψ in v]; [φ ❙→ χ in v]; [ψ ❙→ Θ in v]⟧ ⟹ [χ ❙∨ Θ in v]"
unfolding disj_def using contraposition_1 ded_thm_cor_3 by blast
lemma intro_elim_4_e[PLM]:
"⟦[φ ❙∨ ψ in v]; [φ ❙≡ χ in v]; [ψ ❙≡ Θ in v]⟧ ⟹ [χ ❙∨ Θ in v]"
unfolding equiv_def using "❙&E"(1) intro_elim_4_d by blast
lemmas "❙∨E" = intro_elim_4_a intro_elim_4_b intro_elim_4_c intro_elim_4_d
lemma intro_elim_5[PLM]:
"⟦[φ ❙→ ψ in v]; [ψ ❙→ φ in v]⟧ ⟹ [φ ❙≡ ψ in v]"
by (simp only: equiv_def "❙&I")
lemmas "❙≡I" = intro_elim_5
lemma intro_elim_6_a[PLM]:
"⟦[φ ❙≡ ψ in v]; [φ in v]⟧ ⟹ [ψ in v]"
unfolding equiv_def using "❙&E"(1) vdash_properties_10 by blast
lemma intro_elim_6_b[PLM]:
"⟦[φ ❙≡ ψ in v]; [ψ in v]⟧ ⟹ [φ in v]"
unfolding equiv_def using "❙&E"(2) vdash_properties_10 by blast
lemma intro_elim_6_c[PLM]:
"⟦[φ ❙≡ ψ in v]; [❙¬φ in v]⟧ ⟹ [❙¬ψ in v]"
unfolding equiv_def using "❙&E"(2) modus_tollens_1 by blast
lemma intro_elim_6_d[PLM]:
"⟦[φ ❙≡ ψ in v]; [❙¬ψ in v]⟧ ⟹ [❙¬φ in v]"
unfolding equiv_def using "❙&E"(1) modus_tollens_1 by blast
lemma intro_elim_6_e[PLM]:
"⟦[φ ❙≡ ψ in v]; [ψ ❙≡ χ in v]⟧ ⟹ [φ ❙≡ χ in v]"
by (metis equiv_def ded_thm_cor_3 "❙&E" "❙≡I")
lemma intro_elim_6_f[PLM]:
"⟦[φ ❙≡ ψ in v]; [φ ❙≡ χ in v]⟧ ⟹ [χ ❙≡ ψ in v]"
by (metis equiv_def ded_thm_cor_3 "❙&E" "❙≡I")
lemmas "❙≡E" = intro_elim_6_a intro_elim_6_b intro_elim_6_c
intro_elim_6_d intro_elim_6_e intro_elim_6_f
lemma intro_elim_7[PLM]:
"[φ in v] ⟹ [❙¬❙¬φ in v]"
using if_p_then_p modus_tollens_2 by blast
lemmas "❙¬❙¬I" = intro_elim_7
lemma intro_elim_8[PLM]:
"[❙¬❙¬φ in v] ⟹ [φ in v]"
using if_p_then_p raa_cor_2 by blast
lemmas "❙¬❙¬E" = intro_elim_8

context
begin
private lemma NotNotI[PLM_intro]:
"[φ in v] ⟹ [❙¬(❙¬φ) in v]"
private lemma NotNotD[PLM_dest]:
"[❙¬(❙¬φ) in v] ⟹ [φ in v]"
using "❙¬❙¬E" by blast

private lemma ImplI[PLM_intro]:
"([φ in v] ⟹ [ψ in v]) ⟹ [φ ❙→ ψ in v]"
using CP .
private lemma ImplE[PLM_elim, PLM_dest]:
"[φ ❙→ ψ in v] ⟹ ([φ in v] ⟹ [ψ in v])"
using modus_ponens .
private lemma ImplS[PLM_subst]:
"[φ ❙→ ψ in v] = ([φ in v] ⟶ [ψ in v])"
using ImplI ImplE by blast

private lemma NotI[PLM_intro]:
"([φ in v] ⟹ (⋀ψ .[ψ in v])) ⟹ [❙¬φ in v]"
using CP modus_tollens_2 by blast
private lemma NotE[PLM_elim,PLM_dest]:
"[❙¬φ in v] ⟹ ([φ in v] ⟶ (∀ψ .[ψ in v]))"
using "❙∨I"(2) "❙∨E"(3) by blast
private lemma NotS[PLM_subst]:
"[❙¬φ in v] = ([φ in v] ⟶ (∀ψ .[ψ in v]))"
using NotI NotE by blast

private lemma ConjI[PLM_intro]:
"⟦[φ in v]; [ψ in v]⟧ ⟹ [φ ❙& ψ in v]"
using "❙&I" by blast
private lemma ConjE[PLM_elim,PLM_dest]:
"[φ ❙& ψ in v] ⟹ (([φ in v] ∧ [ψ in v]))"
using CP "❙&E" by blast
private lemma ConjS[PLM_subst]:
"[φ ❙& ψ in v] = (([φ in v] ∧ [ψ in v]))"
using ConjI ConjE by blast

private lemma DisjI[PLM_intro]:
"[φ in v] ∨ [ψ in v] ⟹ [φ ❙∨ ψ in v]"
using "❙∨I" by blast
private lemma DisjE[PLM_elim,PLM_dest]:
"[φ ❙∨ ψ in v] ⟹ [φ in v] ∨ [ψ in v]"
using CP "❙∨E"(1) by blast
private lemma DisjS[PLM_subst]:
"[φ ❙∨ ψ in v] = ([φ in v] ∨ [ψ in v])"
using DisjI DisjE by blast

private lemma EquivI[PLM_intro]:
"⟦[φ in v] ⟹ [ψ in v];[ψ in v] ⟹ [φ in v]⟧ ⟹ [φ ❙≡ ψ in v]"
using CP "❙≡I" by blast
private lemma EquivE[PLM_elim,PLM_dest]:
"[φ ❙≡ ψ in v] ⟹ (([φ in v] ⟶ [ψ in v]) ∧ ([ψ in v] ⟶ [φ in v]))"
using "❙≡E"(1) "❙≡E"(2) by blast
private lemma EquivS[PLM_subst]:
"[φ ❙≡ ψ in v] = ([φ in v] ⟷ [ψ in v])"
using EquivI EquivE by blast

private lemma NotOrD[PLM_dest]:
"¬[φ ❙∨ ψ in v] ⟹ ¬[φ in v] ∧ ¬[ψ in v]"
using "❙∨I" by blast
private lemma NotAndD[PLM_dest]:
"¬[φ ❙& ψ in v] ⟹ ¬[φ in v] ∨ ¬[ψ in v]"
using "❙&I" by blast
private lemma NotEquivD[PLM_dest]:
"¬[φ ❙≡ ψ in v] ⟹ [φ in v] ≠ [ψ in v]"
by (meson NotI contraposition_1 "❙≡I" vdash_properties_9)

private lemma BoxI[PLM_intro]:
"(⋀ v . [φ in v]) ⟹ [❙□φ in v]"
using RN by blast
private lemma NotBoxD[PLM_dest]:
"¬[❙□φ in v] ⟹ (∃ v . ¬[φ in v])"
using BoxI by blast

private lemma AllI[PLM_intro]:
"(⋀ x . [φ x in v]) ⟹ [❙∀ x . φ x in v]"
using rule_gen by blast
lemma NotAllD[PLM_dest]:
"¬[❙∀ x . φ x in v] ⟹ (∃ x . ¬[φ x in v])"
using AllI by fastforce
end

lemma oth_class_taut_1_a[PLM]:
"[❙¬(φ ❙& ❙¬φ) in v]"
by PLM_solver
lemma oth_class_taut_1_b[PLM]:
"[❙¬(φ ❙≡ ❙¬φ) in v]"
by PLM_solver
lemma oth_class_taut_2[PLM]:
"[φ ❙∨ ❙¬φ in v]"
by PLM_solver
lemma oth_class_taut_3_a[PLM]:
"[(φ ❙& φ) ❙≡ φ in v]"
by PLM_solver
lemma oth_class_taut_3_b[PLM]:
"[(φ ❙& ψ) ❙≡ (ψ ❙& φ) in v]"
by PLM_solver
lemma oth_class_taut_3_c[PLM]:
"[(φ ❙& (ψ ❙& χ)) ❙≡ ((φ ❙& ψ) ❙& χ) in v]"
by PLM_solver
lemma oth_class_taut_3_d[PLM]:
"[(φ ❙∨ φ) ❙≡ φ in v]"
by PLM_solver
lemma oth_class_taut_3_e[PLM]:
"[(φ ❙∨ ψ) ❙≡ (ψ ❙∨ φ) in v]"
by PLM_solver
lemma oth_class_taut_3_f[PLM]:
"[(φ ❙∨ (ψ ❙∨ χ)) ❙≡ ((φ ❙∨ ψ) ❙∨ χ) in v]"
by PLM_solver
lemma oth_class_taut_3_g[PLM]:
"[(φ ❙≡ ψ) ❙≡ (ψ ❙≡ φ) in v]"
by PLM_solver
lemma oth_class_taut_3_i[PLM]:
"[(φ ❙≡ (ψ ❙≡ χ)) ❙≡ ((φ ❙≡ ψ) ❙≡ χ) in v]"
by PLM_solver
lemma oth_class_taut_4_a[PLM]:
"[φ ❙≡ φ in v]"
by PLM_solver
lemma oth_class_taut_4_b[PLM]:
"[φ ❙≡ ❙¬❙¬φ in v]"
by PLM_solver
lemma oth_class_taut_5_a[PLM]:
"[(φ ❙→ ψ) ❙≡ ❙¬(φ ❙& ❙¬ψ) in v]"
by PLM_solver
lemma oth_class_taut_5_b[PLM]:
"[❙¬(φ ❙→ ψ) ❙≡ (φ ❙& ❙¬ψ) in v]"
by PLM_solver
lemma oth_class_taut_5_c[PLM]:
"[(φ ❙→ ψ) ❙→ ((ψ ❙→ χ) ❙→ (φ ❙→ χ)) in v]"
by PLM_solver
lemma oth_class_taut_5_d[PLM]:
"[(φ ❙≡ ψ) ❙≡ (❙¬φ ❙≡ ❙¬ψ) in v]"
by PLM_solver
lemma oth_class_taut_5_e[PLM]:
"[(φ ❙≡ ψ) ❙→ ((φ ❙→ χ) ❙≡ (ψ ❙→ χ)) in v]"
by PLM_solver
lemma oth_class_taut_5_f[PLM]:
"[(φ ❙≡ ψ) ❙→ ((χ ❙→ φ) ❙≡ (χ ❙→ ψ)) in v]"
by PLM_solver
lemma oth_class_taut_5_g[PLM]:
"[(φ ❙≡ ψ) ❙→ ((φ ❙≡ χ) ❙≡ (ψ ❙≡ χ)) in v]"
by PLM_solver
lemma oth_class_taut_5_h[PLM]:
"[(φ ❙≡ ψ) ❙→ ((χ ❙≡ φ) ❙≡ (χ ❙≡ ψ)) in v]"
by PLM_solver
lemma oth_class_taut_5_i[PLM]:
"[(φ ❙≡ ψ) ❙≡ ((φ ❙& ψ) ❙∨ (❙¬φ ❙& ❙¬ψ)) in v]"
by PLM_solver
lemma oth_class_taut_5_j[PLM]:
"[(❙¬(φ ❙≡ ψ)) ❙≡ ((φ ❙& ❙¬ψ) ❙∨ (❙¬φ ❙& ψ)) in v]"
by PLM_solver
lemma oth_class_taut_5_k[PLM]:
"[(φ ❙→ ψ) ❙≡ (❙¬φ ❙∨ ψ) in v]"
by PLM_solver

lemma oth_class_taut_6_a[PLM]:
"[(φ ❙& ψ) ❙≡ ❙¬(❙¬φ ❙∨ ❙¬ψ) in v]"
by PLM_solver
lemma oth_class_taut_6_b[PLM]:
"[(φ ❙∨ ψ) ❙≡ ❙¬(❙¬φ ❙& ❙¬ψ) in v]"
by PLM_solver
lemma oth_class_taut_6_c[PLM]:
"[❙¬(φ ❙& ψ) ❙≡ (❙¬φ ❙∨ ❙¬ψ) in v]"
by PLM_solver
lemma oth_class_taut_6_d[PLM]:
"[❙¬(φ ❙∨ ψ) ❙≡ (❙¬φ ❙& ❙¬ψ) in v]"
by PLM_solver

lemma oth_class_taut_7_a[PLM]:
"[(φ ❙& (ψ ❙∨ χ)) ❙≡ ((φ ❙& ψ) ❙∨ (φ ❙& χ)) in v]"
by PLM_solver
lemma oth_class_taut_7_b[PLM]:
"[(φ ❙∨ (ψ ❙& χ)) ❙≡ ((φ ❙∨ ψ) ❙& (φ ❙∨ χ)) in v]"
by PLM_solver

lemma oth_class_taut_8_a[PLM]:
"[((φ ❙& ψ) ❙→ χ) ❙→ (φ ❙→ (ψ ❙→ χ)) in v]"
by PLM_solver
lemma oth_class_taut_8_b[PLM]:
"[(φ ❙→ (ψ ❙→ χ)) ❙→ ((φ ❙& ψ) ❙→ χ) in v]"
by PLM_solver

lemma oth_class_taut_9_a[PLM]:
"[(φ ❙& ψ) ❙→ φ in v]"
by PLM_solver
lemma oth_class_taut_9_b[PLM]:
"[(φ ❙& ψ) ❙→ ψ in v]"
by PLM_solver

lemma oth_class_taut_10_a[PLM]:
"[φ ❙→ (ψ ❙→ (φ ❙& ψ)) in v]"
by PLM_solver
lemma oth_class_taut_10_b[PLM]:
"[(φ ❙→ (ψ ❙→ χ)) ❙≡ (ψ ❙→ (φ ❙→ χ)) in v]"
by PLM_solver
lemma oth_class_taut_10_c[PLM]:
"[(φ ❙→ ψ) ❙→ ((φ ❙→ χ) ❙→ (φ ❙→ (ψ ❙& χ))) in v]"
by PLM_solver
lemma oth_class_taut_10_d[PLM]:
"[(φ ❙→ χ) ❙→ ((ψ ❙→ χ) ❙→ ((φ ❙∨ ψ) ❙→ χ)) in v]"
by PLM_solver
lemma oth_class_taut_10_e[PLM]:
"[(φ ❙→ ψ) ❙→ ((χ ❙→ Θ) ❙→ ((φ ❙& χ) ❙→ (ψ ❙& Θ))) in v]"
by PLM_solver
lemma oth_class_taut_10_f[PLM]:
"[((φ ❙& ψ) ❙≡ (φ ❙& χ)) ❙≡ (φ ❙→ (ψ ❙≡ χ)) in v]"
by PLM_solver
lemma oth_class_taut_10_g[PLM]:
"[((φ ❙& ψ) ❙≡ (χ ❙& ψ)) ❙≡ (ψ ❙→ (φ ❙≡ χ)) in v]"
by PLM_solver

attribute_setup equiv_lr = ‹
Scan.succeed (Thm.rule_attribute []
(fn _ => fn thm => thm RS @{thm "❙≡E"(1)}))
›

attribute_setup equiv_rl = ‹
Scan.succeed (Thm.rule_attribute []
(fn _ => fn thm => thm RS @{thm "❙≡E"(2)}))
›

attribute_setup equiv_sym = ‹
Scan.succeed (Thm.rule_attribute []
(fn _ => fn thm => thm RS @{thm oth_class_taut_3_g[equiv_lr]}))
›

attribute_setup conj1 = ‹
Scan.succeed (Thm.rule_attribute []
(fn _ => fn thm => thm RS @{thm "❙&E"(1)}))
›

attribute_setup conj2 = ‹
Scan.succeed (Thm.rule_attribute []
(fn _ => fn thm => thm RS @{thm "❙&E"(2)}))
›

attribute_setup conj_sym = ‹
Scan.succeed (Thm.rule_attribute []
(fn _ => fn thm => thm RS @{thm oth_class_taut_3_b[equiv_lr]}))
›

subsection‹Identity›
text‹\label{TAO_PLM_Identity}›

lemma id_eq_prop_prop_1[PLM]:
"[(F::Π⇩1) ❙= F in v]"
unfolding identity_defs by PLM_solver
lemma id_eq_prop_prop_2[PLM]:
"[((F::Π⇩1) ❙= G) ❙→ (G ❙= F) in v]"
by (meson id_eq_prop_prop_1 CP ded_thm_cor_3 l_identity[axiom_instance])
lemma id_eq_prop_prop_3[PLM]:
"[(((F::Π⇩1) ❙= G) ❙& (G ❙= H)) ❙→ (F ❙= H) in v]"
by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "❙&E")
lemma id_eq_prop_prop_4_a[PLM]:
"[(F::Π⇩2) ❙= F in v]"
unfolding identity_defs by PLM_solver
lemma id_eq_prop_prop_4_b[PLM]:
"[(F::Π⇩3) ❙= F in v]"
unfolding identity_defs by PLM_solver
lemma id_eq_prop_prop_5_a[PLM]:
"[((F::Π⇩2) ❙= G) ❙→ (G ❙= F) in v]"
by (meson id_eq_prop_prop_4_a CP ded_thm_cor_3 l_identity[axiom_instance])
lemma id_eq_prop_prop_5_b[PLM]:
"[((F::Π⇩3) ❙= G) ❙→ (G ❙= F) in v]"
by (meson id_eq_prop_prop_4_b CP ded_thm_cor_3 l_identity[axiom_instance])
lemma id_eq_prop_prop_6_a[PLM]:
"[(((F::Π⇩2) ❙= G) ❙& (G ❙= H)) ❙→ (F ❙= H) in v]"
by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "❙&E")
lemma id_eq_prop_prop_6_b[PLM]:
"[(((F::Π⇩3) ❙= G) ❙& (G ❙= H)) ❙→ (F ❙= H) in v]"
by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "❙&E")
lemma id_eq_prop_prop_7[PLM]:
"[(p::Π⇩0) ❙= p in v]"
unfolding identity_defs by PLM_solver
lemma id_eq_prop_prop_7_b[PLM]:
"[(p::𝗈) ❙= p in v]"
unfolding identity_defs by PLM_solver
lemma id_eq_prop_prop_8[PLM]:
"[((p::Π⇩0) ❙= q) ❙→ (q ❙= p) in v]"
by (meson id_eq_prop_prop_7 CP ded_thm_cor_3 l_identity[axiom_instance])
lemma id_eq_prop_prop_8_b[PLM]:
"[((p::𝗈) ❙= q) ❙→ (q ❙= p) in v]"
by (meson id_eq_prop_prop_7_b CP ded_thm_cor_3 l_identity[axiom_instance])
lemma id_eq_prop_prop_9[PLM]:
"[(((p::Π⇩0) ❙= q) ❙& (q ❙= r)) ❙→ (p ❙= r) in v]"
by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "❙&E")
lemma id_eq_prop_prop_9_b[PLM]:
"[(((p::𝗈) ❙= q) ❙& (q ❙= r)) ❙→ (p ❙= r) in v]"
by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "❙&E")

lemma eq_E_simple_1[PLM]:
"[(x ❙=⇩E y) ❙≡ (⦇O!,x⦈ ❙& ⦇O!,y⦈ ❙& ❙□(❙∀F . ⦇F,x⦈ ❙≡ ⦇F,y⦈)) in v]"
proof (rule "❙≡I"; rule CP)
assume 1: "[x ❙=⇩E y in v]"
have "[❙∀ x y . ((x⇧P) ❙=⇩E (y⇧P)) ❙≡ (⦇O!,x⇧P⦈ ❙& ⦇O!,y⇧P⦈
❙& ❙□(❙∀F . ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈)) in v]"
unfolding identity⇩E_infix_def identity⇩E_def
apply (rule lambda_predicates_2_2[axiom_universal, axiom_universal, axiom_instance])
by show_proper
moreover have "[❙∃ α . (α⇧P) ❙= x in v]"
apply (rule cqt_5_mod[where ψ="λ x . x ❙=⇩E y", axiom_instance,deduction])
unfolding identity⇩E_infix_def
apply (rule SimpleExOrEnc.intros)
using 1 unfolding identity⇩E_infix_def by auto
moreover have "[❙∃ β . (β⇧P) ❙= y in v]"
apply (rule cqt_5_mod[where ψ="λ y . x ❙=⇩E y",axiom_instance,deduction])
unfolding identity⇩E_infix_def
apply (rule SimpleExOrEnc.intros) using 1
unfolding identity⇩E_infix_def by auto
ultimately have "[(x ❙=⇩E y) ❙≡ (⦇O!,x⦈ ❙& ⦇O!,y⦈
❙& ❙□(❙∀F . ⦇F,x⦈ ❙≡ ⦇F,y⦈)) in v]"
using cqt_1_κ[axiom_instance,deduction, deduction] by meson
thus "[(⦇O!,x⦈ ❙& ⦇O!,y⦈ ❙& ❙□(❙∀F . ⦇F,x⦈ ❙≡ ⦇F,y⦈)) in v]"
using 1 "❙≡E"(1) by blast
next
assume 1: "[⦇O!,x⦈ ❙& ⦇O!,y⦈ ❙& ❙□(❙∀F. ⦇F,x⦈ ❙≡ ⦇F,y⦈) in v]"
have "[❙∀ x y . ((x⇧P) ❙=⇩E (y⇧P)) ❙≡ (⦇O!,x⇧P⦈ ❙& ⦇O!,y⇧P⦈
❙& ❙□(❙∀F . ⦇F,x⇧P⦈ ❙≡ ⦇F,y⇧P⦈)) in v]"
unfolding identity⇩E_def identity⇩E_infix_def
apply (rule lambda_predicates_2_2[axiom_universal, axiom_universal, axiom_instance])
by show_proper
moreover have "[❙∃ α . (α⇧P) ❙= x in v]"
apply (rule cqt_5_mod[where ψ="λ x . ⦇O!,x⦈",axiom_instance,deduction])
apply (rule SimpleExOrEnc.intros)
using 1[conj1,conj1] by auto
moreover have "[❙∃ β . (β⇧P) ❙= y in v]"
apply (rule cqt_5_mod[where ψ="λ y . ⦇O!,y⦈",axiom_instance,deduction])
apply (rule SimpleExOrEnc.intros)
using 1[conj1,conj2] by auto
ultimately have "[(x ❙=⇩E y) ❙≡ (⦇O!,x⦈ ❙& ⦇O!,y⦈
❙& ❙□(❙∀F . ⦇F,x⦈ ❙≡ ⦇F,y⦈)) in v]"
using cqt_1_κ[axiom_instance,deduction, deduction] by meson
thus "[(x ❙=⇩E y) in v]" using 1 "❙≡E"(2) by blast
qed
lemma eq_E_simple_2[PLM]:
"[(x ❙=⇩E y) ❙→ (x ❙= y) in v]"
unfolding identity_defs by PLM_solver
lemma eq_E_simple_3[PLM]:
"[(x ❙= y) ❙≡ ((⦇O!,x⦈ ❙& ⦇O!,y⦈ ❙& ❙□(❙∀F . ⦇F,x⦈ ❙≡ ⦇F,y⦈))
❙∨ (⦇A!,x⦈ ❙& ⦇A!,y⦈ ❙& ❙□(❙∀F. ⦃x,F⦄ ❙≡ ⦃y,F⦄))) in v]"
using eq_E_simple_1
apply - unfolding identity_defs
by PLM_solver

lemma id_eq_obj_1[PLM]: "[(x⇧P) ❙= (x⇧P) in v]"
proof -
have "[(❙◇⦇E!, x⇧P⦈) ❙∨ (❙¬❙◇⦇E!, x⇧P⦈) in v]"
using PLM.oth_class_taut_2 by simp
hence "[(❙◇⦇E!, x⇧P⦈) in v] ∨ [(❙¬❙◇⦇E!, x⇧P⦈) in v]"
using CP "❙∨E"(1) by blast
moreover {
assume "[(❙◇⦇E!, x⇧P⦈) in v]"
hence "[⦇❙λx. ❙◇⦇E!,x⇧P⦈,x⇧P⦈ in v]"
apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl, rotated])
by show_proper
hence "[⦇❙λx. ❙◇⦇E!,x⇧P⦈,x⇧P⦈ ❙& ⦇❙λx. ❙◇⦇E!,x⇧P⦈,x⇧P⦈
❙& ❙□(❙∀F. ⦇F,x⇧P⦈ ❙≡ ⦇F,x⇧P⦈) in v]"
apply - by PLM_solver
hence "[(x⇧P) ❙=⇩E (x⇧P) in v]"
using eq_E_simple_1[equiv_rl] unfolding Ordinary_def by fast
}
moreover {
assume "[(❙¬❙◇⦇E!, x⇧P⦈) in v]"
hence "[⦇❙λx. ❙¬❙◇⦇E!,x⇧P⦈,x⇧P⦈ in v]"
apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl, rotated])
by show_proper
hence "[⦇❙λx. ❙¬❙◇⦇E!,x⇧P⦈,x⇧P⦈ ❙& ⦇❙λx. ❙¬❙◇⦇E!,x⇧P⦈,x⇧P⦈
❙& ❙□(❙∀F. ⦃x⇧P,F⦄ ❙≡ ⦃x⇧P,F⦄) in v]"
apply - by PLM_solver
}
ultimately show ?thesis unfolding identity_defs Ordinary_def Abstract_def
using "❙∨I" by blast
qed
lemma id_eq_obj_2[PLM]:
"[((x⇧P) ❙= (y⇧P)) ❙→ ((y⇧P) ❙= (x⇧P)) in v]"
by (meson l_identity[axiom_instance] id_eq_obj_1 CP ded_thm_cor_3)
lemma id_eq_obj_3[PLM]:
"[((x⇧P) ❙= (y⇧P)) ❙& ((y⇧P) ❙= (z⇧P)) ❙→ ((x⇧P) ❙= (z⇧P)) in v]"
by (metis l_identity[axiom_instance] ded_thm_cor_4 CP "❙&E")
end

text‹
\begin{remark}
To unify the statements of the properties of equality a type class is introduced.
\end{remark}
›

class id_eq = quantifiable_and_identifiable +
assumes id_eq_1: "[(x :: 'a) ❙= x in v]"
assumes id_eq_2: "[((x :: 'a) ❙= y) ❙→ (y ❙= x) in v]"
assumes id_eq_3: "[((x :: 'a) ❙= y) ❙& (y ❙= z) ❙→ (x ❙= z) in v]"

instantiation ν :: id_eq
begin
instance proof
fix x :: ν and v
show "[x ❙= x in v]"
using PLM.id_eq_obj_1
next
fix x y::ν and v
show "[x ❙= y ❙→ y ❙= x in v]"
using PLM.id_eq_obj_2
next
fix x y z::ν and v
show "[((x ❙= y) ❙& (y ❙= z)) ❙→ x ❙= z in v]"
using PLM.id_eq_obj_3
qed
end

instantiation 𝗈 :: id_eq
begin
instance proof
fix x :: 𝗈 and v
show "[x ❙= x in v]"
using PLM.id_eq_prop_prop_7 .
next
fix x y :: 𝗈 and v
show "[x ❙= y ❙→ y ❙= x in v]"
using PLM.id_eq_prop_prop_8 .
next
fix x y z :: 𝗈 and v
show "[((x ❙= y) ❙& (y ❙= z)) ❙→ x ❙= z in v]"
using PLM.id_eq_prop_prop_9 .
qed
end

instantiation Π⇩1 :: id_eq
begin
instance proof
fix x :: Π⇩1 and v
show "[x ❙= x in v]"
using PLM.id_eq_prop_prop_1 .
next
fix x y :: Π⇩1 and v
show "[x ❙= y ❙→ y ❙= x in v]"
using PLM.id_eq_prop_prop_2 .
next
fix x y z :: Π⇩1 and v
show "[((x ❙= y) ❙& (y ❙= z)) ❙→ x ❙= z in v]"
using PLM.id_eq_prop_prop_3 .
qed
end

instantiation Π⇩2 :: id_eq
begin
instance proof
fix x :: Π⇩2 and v
show "[x ❙= x in v]"
using PLM.id_eq_prop_prop_4_a .
next
fix x y :: Π⇩2 and v
show "[x ❙= y ❙→ y ❙= x in v]"
using PLM.id_eq_prop_prop_5_a .
next
fix x y z :: Π⇩2 and v
show "[((x ❙= y) ❙& (y ❙= z)) ❙→ x ❙= z in v]"
using PLM.id_eq_prop_prop_6_a .
qed
end

instantiation Π⇩3 :: id_eq
begin
instance proof
fix x :: Π⇩3 and v
show "[x ❙= x in v]"
using PLM.id_eq_prop_prop_4_b .
next
fix x y :: Π⇩3 and v
show "[x ❙= y ❙→ y ❙= x in v]"
using PLM.id_eq_prop_prop_5_b .
next
fix x y z :: Π⇩3 and v
show "[((x ❙= y) ❙& (y ❙= z)) ❙→ x ❙= z in v]"
using PLM.id_eq_prop_prop_6_b .
qed
end

context PLM
begin
lemma id_eq_1[PLM]:
"[(x::'a::id_eq) ❙= x in v]"
using id_eq_1 .
lemma id_eq_2[PLM]:
"[((x::'a::id_eq) ❙= y) ❙→ (y ❙= x) in v]"
using id_eq_2 .
lemma id_eq_3[PLM]:
"[((x::'a::id_eq) ❙= y) ❙& (y ❙= z) ❙→ (x ❙= z) in v]"
using id_eq_3 .

attribute_setup eq_sym = ‹
Scan.succeed (Thm.rule_attribute []
(fn _ => fn thm => thm RS @{thm id_eq_2[deduction]}))
›

lemma all_self_eq_1[PLM]:
"[❙□(❙∀ α :: 'a::id_eq . α ❙= α) in v]"
by PLM_solver
lemma all_self_eq_2[PLM]:
"[❙∀α :: 'a::id_eq . ❙□(α ❙= α) in v]"
by PLM_solver

lemma t_id_t_proper_1[PLM]:
"[τ ❙= τ' ❙→ (❙∃ β . (β⇧P) ❙= τ) in v]"
proof (rule CP)
assume "[τ ❙= τ' in v]"
moreover {
assume "[τ ❙=⇩E τ' in v]"
hence "[❙∃ β . (β⇧P) ❙= τ in v]"
apply -
apply (rule cqt_5_mod[where ψ="λ τ . τ ❙=⇩E τ'", axiom_instance, deduction])
subgoal unfolding identity_defs by (rule SimpleExOrEnc.intros)
by simp
}
moreover {
assume "[⦇A!,τ⦈ ❙& ⦇A!,τ'⦈ ❙& ❙□(❙∀F. ⦃τ,F⦄ ❙≡ ⦃τ',F⦄) in v]"
hence "[❙∃ β . (β⇧P) ❙= τ in v]"
apply -
apply (rule cqt_5_mod[where ψ="λ τ . ⦇A!,τ⦈", axiom_instance, deduction])
subgoal unfolding identity_defs by (rule SimpleExOrEnc.intros)
by PLM_solver
}
ultimately show "[❙∃ β . (β⇧P) ❙= τ in v]" unfolding identity⇩κ_def
using intro_elim_4_b reductio_aa_1 by blast
qed

lemma t_id_t_proper_2[PLM]: "[τ ❙= τ' ❙→ (❙∃ β . (β⇧P) ❙= τ') in v]"
proof (rule CP)
assume "[τ ❙= τ' in v]"
moreover {
assume "[τ ❙=⇩E τ' in v]"
hence "[❙∃ β . (β⇧P) ❙= τ' in v]"
apply -
apply (rule cqt_5_mod[where ψ="λ τ' . τ ❙=⇩E τ'", axiom_instance, deduction])
subgoal unfolding identity_defs by (rule SimpleExOrEnc.intros)
by simp
}
moreover {
assume "[⦇A!,τ⦈ ❙& ⦇A!,τ'⦈ ❙& ❙□(❙∀F. ⦃τ,F⦄ ❙≡ ⦃τ',F⦄) in v]"
hence "[❙∃ β . (β⇧P) ❙= τ' in v]"
apply -
apply (rule cqt_5_mod[where ψ="λ τ . ⦇A!,τ⦈", axiom_instance, deduction])
subgoal unfolding identity_defs by (rule SimpleExOrEnc.intros)
by PLM_solver
}
ultimately show "[❙∃ β . (β⇧P) ❙= τ' in v]" unfolding identity⇩κ_def
using intro_elim_4_b reductio_aa_1 by blast
qed

lemma id_nec[PLM]: "[((α::'a::id_eq) ❙= (β)) ❙≡ ❙□((α) ❙= (β)) in v]"
apply (rule "❙≡I")
using l_identity[where φ = "(λ β .  ❙□((α) ❙= (β)))", axiom_instance]
id_eq_1 RN ded_thm_cor_4 unfolding identity_ν_def
apply blast
using qml_2[axiom_instance] by blast

lemma id_nec_desc[PLM]:
"[((❙ιx. φ x) ❙= (❙ιx. ψ x)) ❙≡ ❙□((❙ιx. φ x) ❙= (❙ιx. ψ x)) in v]"
proof (cases "[(❙∃ α. (α⇧P) ❙= (❙ιx . φ x)) in v] ∧ [(❙∃ β. (β⇧P) ❙= (❙ιx . ψ x)) in v]")
assume "[(❙∃ α. (α⇧P) ❙= (❙ιx . φ x)) in v] ∧ [(❙∃ β. (β⇧P) ❙= (❙ιx . ψ x)) in v]"
then obtain α and β where
"[(α⇧P) ❙= (❙ιx . φ x) in v] ∧ [(β⇧P) ❙= (❙ιx . ψ x) in v]"
apply - unfolding conn_defs by PLM_solver
moreover {
moreover have "[(α) ❙= (β) ❙≡ ❙□((α) ❙= (β)) in v]" by PLM_solver
ultimately have "[((❙ιx. φ x) ❙= (β⇧P) ❙≡ ❙□((❙ιx. φ x) ❙= (β⇧P))) in v]"
using l_identity[where φ="λ α . (α) ❙= (β⇧P) ❙≡ ❙□((α) ❙= (β⇧P))", axiom_instance]
modus_ponens unfolding identity_ν_def by metis
}
ultimately show ?thesis
using l_identity[where φ="λ α . (❙ιx . φ x) ❙= (α)
❙≡ ❙□((❙ιx . φ x) ❙= (α))", axiom_instance]
modus_ponens by metis
next
assume "¬([(❙∃ α. (α⇧P) ❙= (❙ιx . φ x)) in v] ∧ [(❙∃ β. (β⇧P) ❙= (❙ιx . ψ x)) in v])"
hence "¬[⦇A!,(❙ιx . φ x)⦈ in v] ∧ ¬[(❙ιx . φ x) ❙=⇩E (❙ιx . ψ x) in v]
∨ ¬[⦇A!,(❙ιx . ψ x)⦈ in v] ∧ ¬[(❙ιx . φ x) ❙=⇩E (❙ιx . ψ x) in v]"
unfolding identity⇩E_infix_def
using cqt_5[axiom_instance] PLM.contraposition_1 SimpleExOrEnc.intros
vdash_properties_10 by meson
hence "¬[(❙ιx . φ x) ❙= (❙ιx . ψ x) in v]"
apply - unfolding identity_defs by PLM_solver
thus ?thesis apply - apply PLM_solver
using qml_2[axiom_instance, deduction] by auto
qed

subsection‹Quantification›
text‹\label{TAO_PLM_Quantification}›

lemma rule_ui[PLM,PLM_elim,PLM_dest]:
"[❙∀α . φ α in v] ⟹ [φ β in v]"
by (meson cqt_1[axiom_instance, deduction])
lemmas "❙∀E" = rule_ui

lemma rule_ui_2[PLM,PLM_elim,PLM_dest]:
"⟦[❙∀α . φ (α⇧P) in v]; [❙∃ α . (α)⇧P ❙= β in v]⟧ ⟹ [φ β in v]"
using cqt_1_κ[axiom_instance, deduction, deduction] by blast

lemma cqt_orig_1[PLM]:
"[(❙∀α. φ α) ❙→ φ β in v]"
by PLM_solver
lemma cqt_orig_2[PLM]:
"[(❙∀α. φ ❙→ ψ α) ❙→ (φ ❙→ (❙∀α. ψ α)) in v]"
by PLM_solver

lemma universal[PLM]:
"(⋀α . [φ α in v]) ⟹ [❙∀ α . φ α in v]"
using rule_gen .
lemmas "❙∀I" = universal

lemma cqt_basic_1[PLM]:
"[(❙∀α. (❙∀β . φ α β)) ❙≡ (❙∀β. (❙∀α. φ α β)) in v]"
by PLM_solver
lemma cqt_basic_2[PLM]:
"[(❙∀α. φ α ❙≡ ψ α) ❙≡ ((❙∀α. φ α ❙→ ψ α) ❙& (❙∀α. ψ α ❙→ φ α)) in v]"
by PLM_solver
lemma cqt_basic_3[PLM]:
"[(❙∀α. φ α ❙≡ ψ α) ❙→ ((❙∀α. φ α) ❙≡ (❙∀α. ψ α)) in v]"
by PLM_solver
lemma cqt_basic_4[PLM]:
"[(❙∀α. φ α ❙& ψ α) ❙≡ ((❙∀α. φ α) ❙& (❙∀α. ψ α)) in v]"
by PLM_solver
lemma cqt_basic_6[PLM]:
"[(❙∀α. (❙∀α. φ α)) ❙≡ (❙∀α. φ α) in v]"
by PLM_solver
lemma cqt_basic_7[PLM]:
"[(φ ❙→ (❙∀α . ψ α)) ❙≡ (❙∀α.(φ ❙→ ψ α)) in v]"
by PLM_solver
lemma cqt_basic_8[PLM]:
"[((❙∀α. φ α) ❙∨ (❙∀α. ψ α)) ❙→ (❙∀α. (φ α ❙∨ ψ α)) in v]"
by PLM_solver
lemma cqt_basic_9[PLM]:
"[((❙∀α. φ α ❙→ ψ α) ❙& (❙∀α. ψ α ❙→ χ α)) ❙→ (❙∀α. φ α ❙→ χ α) in v]"
by PLM_solver
lemma cqt_basic_10[PLM]:
"[((❙∀α. φ α ❙≡ ψ α) ❙& (❙∀α. ψ α ❙≡ χ α)) ❙→ (❙∀α. φ α ❙≡ χ α) in v]"
by PLM_solver
lemma cqt_basic_11[PLM]:
"[(❙∀α. φ α ❙≡ ψ α) ❙≡ (❙∀α. ψ α ❙≡ φ α) in v]"
by PLM_solver
lemma cqt_basic_12[PLM]:
"[(❙∀α. φ α) ❙≡ (❙∀β. φ β) in v]"
by PLM_solver

lemma existential[PLM,PLM_intro]:
"[φ α in v] ⟹ [❙∃ α. φ α in v]"
unfolding exists_def by PLM_solver
lemmas "❙∃I" = existential
lemma instantiation_[PLM,PLM_elim,PLM_dest]:
"⟦[❙∃α . φ α in v]; (⋀α.[φ α in v] ⟹ [ψ in v])⟧ ⟹ [ψ in v]"
unfolding exists_def by PLM_solver

lemma Instantiate:
assumes "[❙∃ x . φ x  in v]"
obtains x where "[φ x in v]"
apply (insert assms) unfolding exists_def by PLM_solver
lemmas "❙∃E" = Instantiate

lemma cqt_further_1[PLM]:
"[(❙∀α. φ α) ❙→ (❙∃α. φ α) in v]"
by PLM_solver
lemma cqt_further_2[PLM]:
"[(❙¬(❙∀α. φ α)) ❙≡ (❙∃α. ❙¬φ α) in v]"
unfolding exists_def by PLM_solver
lemma cqt_further_3[PLM]:
"[(❙∀α. φ α) ❙≡ ❙¬(❙∃α. ❙¬φ α) in v]"
unfolding exists_def by PLM_solver
lemma cqt_further_4[PLM]:
"[(❙¬(❙∃α. φ α)) ❙≡ (❙∀α. ❙¬φ α) in v]"
unfolding exists_def by PLM_solver
lemma cqt_further_5[PLM]:
"[(❙∃α. φ α ❙& ψ α) ❙→ ((❙∃α. φ α) ❙& (❙∃α. ψ α)) in v]"
unfolding exists_def by PLM_solver
lemma cqt_further_6[PLM]:
"[(❙∃α. φ α ❙∨ ψ α) ❙≡ ((❙∃α. φ α) ❙∨ (❙∃α. ψ α)) in v]"
unfolding exists_def by PLM_solver
lemma cqt_further_10[PLM]:
"[(φ (α::'a::id_eq) ❙& (❙∀ β . φ β ❙→ β ❙= α)) ❙≡ (❙∀ β . φ β ❙≡ β ❙= α) in v]"
apply PLM_solver
using l_identity[axiom_instance, deduction, deduction] id_eq_2[deduction]
apply blast
using id_eq_1 by auto
lemma cqt_further_11[PLM]:
"[((❙∀α. φ α) ❙& (❙∀α. ψ α)) ❙→ (❙∀α. φ α ❙≡ ψ α) in v]"
by PLM_solver
lemma cqt_further_12[PLM]:
"[((❙¬(❙∃α. φ α)) ❙& (❙¬(❙∃α. ψ α))) ❙→ (❙∀α. φ α ❙≡ ψ α) in v]"
unfolding exists_def by PLM_solver
lemma cqt_further_13[PLM]:
"[((❙∃α. φ α) ❙& (❙¬(❙∃α. ψ α))) ❙→ (❙¬(❙∀α. φ α ❙≡ ψ α)) in v]"
unfolding exists_def by PLM_solver
lemma cqt_further_14[PLM]:
"[(❙∃α. ❙∃β. φ α β) ❙≡ (❙∃β. ❙∃α. φ α β) in v]"
unfolding exists_def by PLM_solver

lemma nec_exist_unique[PLM]:
"[(❙∀ x. φ x ❙→ ❙□(φ x)) ❙→ ((❙∃!x. φ x) ❙→ (❙∃!x. ❙□(φ x))) in v]"
proof (rule CP)
assume a: "[❙∀x. φ x ❙→ ❙□φ x in v]"
show "[(❙∃!x. φ x) ❙→ (❙∃!x. ❙□φ x) in v]"
proof (rule CP)
assume "[(❙∃!x. φ x) in v]"
hence "[❙∃α. φ α ❙& (❙∀β. φ β ❙→ β ❙= α) in v]"
by (simp only: exists_unique_def)
then obtain α where 1:
"[φ α ❙& (❙∀β. φ β ❙→ β ❙= α) in v]"
by (rule "❙∃E")
{
fix β
have "[❙□φ β ❙→ β ❙= α in v]"
by (metis "1" Semantics.T5 Semantics.T6 cqt_orig_1 oth_class_taut_9_b)
}
hence "[❙∀β. ❙□φ β ❙→ β ❙= α in v]" by (rule "❙∀I")
moreover have "[❙□(φ α) in v]"
using 1 "❙&E"(1) a vdash_properties_10 cqt_orig_1[deduction]
by fast
ultimately have "[❙∃α. ❙□(φ α) ❙& (❙∀β. ❙□φ β ❙→ β ❙= α) in v]"
using "❙&I" "❙∃I" by fast
thus "[(❙∃!x. ❙□φ x) in v]"
unfolding exists_unique_def by assumption
qed
qed

subsection‹Actuality and Descriptions›
text‹\label{TAO_PLM_ActualityAndDescriptions}›

lemma nec_imp_act[PLM]: "[❙□φ ❙→ ❙𝒜φ in v]"
apply (rule CP)
using qml_act_2[axiom_instance, equiv_lr]
qml_2[axiom_actualization, axiom_instance]
logic_actual_nec_2[axiom_instance, equiv_lr, deduction]
by blast
lemma act_conj_act_1[PLM]:
"[❙𝒜(❙𝒜φ ❙→ φ) in v]"
using equiv_def logic_actual_nec_2[axiom_instance]
logic_actual_nec_4[axiom_instance] "❙&E"(2) "❙≡E"(2)
by metis
lemma act_conj_act_2[PLM]:
"[❙𝒜(φ ❙→ ❙𝒜φ) in v]"
using logic_actual_nec_2[axiom_instance] qml_act_1[axiom_instance]
ded_thm_cor_3 "❙≡E"(2) nec_imp_act
by blast
lemma act_conj_act_3[PLM]:
"[(❙𝒜φ ❙& ❙𝒜ψ) ❙→ ❙𝒜(φ ❙& ψ) in v]"
unfolding conn_defs
by (metis logic_actual_nec_2[axiom_instance]
logic_actual_nec_1[axiom_instance]
"❙≡E"(2) CP "❙≡E"(4) reductio_aa_2
vdash_properties_10)
lemma act_conj_act_4[PLM]:
"[❙𝒜(❙𝒜φ ❙≡ φ) in v]"
unfolding equiv_def
by (PLM_solver PLM_intro: act_conj_act_3[where φ="❙𝒜φ ❙→ φ"
and ψ="φ ❙→ ❙𝒜φ", deduction])
lemma closure_act_1a[PLM]:
"[❙𝒜❙𝒜(❙𝒜φ ❙≡ φ) in v]"
using logic_actual_nec_4[axiom_instance]
act_conj_act_4 "❙≡E"(1)
by blast
lemma closure_act_1b[PLM]:
"[❙𝒜❙𝒜❙𝒜(❙𝒜φ ❙≡ φ) in v]"
using logic_actual_nec_4[axiom_instance]
act_conj_act_4 "❙≡E"(1)
by blast
lemma closure_act_1c[PLM]:
"[❙𝒜❙𝒜❙𝒜❙𝒜(❙𝒜φ ❙≡ φ) in v]"
using logic_actual_nec_4[axiom_instance]
act_conj_act_4 "❙≡E"(1)
by blast
lemma closure_act_2[PLM]:
"[❙∀α. ❙𝒜(❙𝒜(φ α) ❙≡ φ α) in v]"
by PLM_solver

lemma closure_act_3[PLM]:
"[❙𝒜(❙∀α. ❙𝒜(φ α) ❙≡ φ α) in v]"
by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl])
lemma closure_act_4[PLM]:
"[❙𝒜(❙∀α⇩1 α⇩2. ❙𝒜(φ α⇩1 α⇩2) ❙≡ φ α⇩1 α⇩2) in v]"
by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl])
lemma closure_act_4_b[PLM]:
"[❙𝒜(❙∀α⇩1 α⇩2 α⇩3. ❙𝒜(φ α⇩1 α⇩2 α⇩3) ❙≡ φ α⇩1 α⇩2 α⇩3) in v]"
by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl])
lemma closure_act_4_c[PLM]:
"[❙𝒜(❙∀α⇩1 α⇩2 α⇩3 α⇩4. ❙𝒜(φ α⇩1 α⇩2 α⇩3 α⇩4) ❙≡ φ α⇩1 α⇩2 α⇩3 α⇩4) in v]"
by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl])

lemma RA[PLM,PLM_intro]:
"([φ in dw]) ⟹ [❙𝒜φ in dw]"
using logic_actual[necessitation_averse_axiom_instance, equiv_rl] .

lemma RA_2[PLM,PLM_intro]:
"([ψ in dw] ⟹ [φ in dw]) ⟹ ([❙𝒜ψ in dw] ⟹ [❙𝒜φ in dw])"
using RA logic_actual[necessitation_averse_axiom_instance] intro_elim_6_a by blast

context
begin
private lemma ActualE[PLM,PLM_elim,PLM_dest]:
"[❙𝒜φ in dw] ⟹ [φ in dw]"
using logic_actual[necessitation_averse_axiom_instance, equiv_lr] .

private lemma NotActualD[PLM_dest]:
"¬[❙𝒜φ in dw] ⟹ ¬[φ in dw]"
using RA by metis

private lemma ActualImplI[PLM_intro]:
"[❙𝒜φ ❙→ ❙𝒜ψ in v] ⟹ [❙𝒜(φ ❙→ ψ) in v]"
using logic_actual_nec_2[axiom_instance, equiv_rl] .
private lemma ActualImplE[PLM_dest, PLM_elim]:
"[❙𝒜(φ ❙→ ψ) in v] ⟹ [❙𝒜φ ❙→ ❙𝒜ψ in v]"
using logic_actual_nec_2[axiom_instance, equiv_lr] .
private lemma NotActualImplD[PLM_dest]:
"¬[❙𝒜(φ ❙→ ψ) in v] ⟹ ¬[❙𝒜φ ❙→ ❙𝒜ψ in v]"
using ActualImplI by blast

private lemma ActualNotI[PLM_intro]:
"[❙¬❙𝒜φ in v] ⟹ [❙𝒜❙¬φ in v]"
using logic_actual_nec_1[axiom_instance, equiv_rl] .
lemma ActualNotE[PLM_elim,PLM_dest]:
"[❙𝒜❙¬φ in v] ⟹ [❙¬❙𝒜φ in v]"
using logic_actual_nec_1[axiom_instance, equiv_lr] .
lemma NotActualNotD[PLM_dest]:
"¬[❙𝒜❙¬φ in v] ⟹ ¬[❙¬❙𝒜φ in v]"
using ActualNotI by blast

private  lemma ActualConjI[PLM_intro]:
"[❙𝒜φ ❙& ❙𝒜ψ in v] ⟹ [❙𝒜(φ ❙& ψ) in v]"
unfolding equiv_def
by (PLM_solver PLM_intro: act_conj_act_3[deduction])
private lemma ActualConjE[PLM_elim,PLM_dest]:
"[❙𝒜(φ ❙& ψ) in v] ⟹ [❙𝒜φ ❙& ❙𝒜ψ in v]"
unfolding conj_def by PLM_solver

private lemma ActualEquivI[PLM_intro]:
"[❙𝒜φ ❙≡ ❙𝒜ψ in v] ⟹ [❙𝒜(φ ❙≡ ψ) in v]"
unfolding equiv_def
by (PLM_solver PLM_intro: act_conj_act_3[deduction])
private lemma ActualEquivE[PLM_elim, PLM_dest]:
"[❙𝒜(φ ❙≡ ψ) in v] ⟹ [❙𝒜φ ❙≡ ❙𝒜ψ in v]"
unfolding equiv_def by PLM_solver

private lemma ActualBoxI[PLM_intro]:
"[❙□φ in v] ⟹ [❙𝒜(❙□φ) in v]"
using qml_act_2[axiom_instance, equiv_lr] .
private lemma ActualBoxE[PLM_elim, PLM_dest]:
"[❙𝒜(❙□φ) in v] ⟹ [❙□φ in v]"
using qml_act_2[axiom_instance, equiv_rl] .
private lemma NotActualBoxD[PLM_dest]:
"¬[❙𝒜(❙□φ) in v] ⟹ ¬[❙□φ in v]"
using ActualBoxI by blast

private lemma ActualDisjI[PLM_intro]:
"[❙𝒜φ ❙∨ ❙𝒜ψ in v] ⟹ [❙𝒜(φ ❙∨ ψ) in v]"
unfolding disj_def by PLM_solver
private lemma ActualDisjE[PLM_elim,PLM_dest]:
"[❙𝒜(φ ❙∨ ψ) in v] ⟹ [❙𝒜φ ❙∨ ❙𝒜ψ in v]"
unfolding disj_def by PLM_solver
private lemma NotActualDisjD[PLM_dest]:
"¬[❙𝒜(φ ❙∨ ψ) in v] ⟹ ¬[❙𝒜φ ❙∨ ❙𝒜ψ in v]"
using ActualDisjI by blast

private lemma ActualForallI[PLM_intro]:
"[❙∀ x . ❙𝒜(φ x) in v] ⟹ [❙𝒜(❙∀ x . φ x) in v]"
using logic_actual_nec_3[axiom_instance, equiv_rl] .
lemma ActualForallE[PLM_elim,PLM_dest]:
"[❙𝒜(❙∀ x . φ x) in v] ⟹ [❙∀ x . ❙𝒜(φ x) in v]"
using logic_actual_nec_3[axiom_instance, equiv_lr] .
lemma NotActualForallD[PLM_dest]:
"¬[❙𝒜(❙∀ x . φ x) in v] ⟹ ¬[❙∀ x . ❙𝒜(φ x) in v]"
using ActualForallI by blast

lemma ActualActualI[PLM_intro]:
"[❙𝒜φ in v] ⟹ [❙𝒜❙𝒜φ in v]"
using logic_actual_nec_4[axiom_instance, equiv_lr] .
lemma ActualActualE[PLM_elim,PLM_dest]:
"[❙𝒜❙𝒜φ in v] ⟹ [❙𝒜φ in v]"
using logic_actual_nec_4[axiom_instance, equiv_rl] .
lemma NotActualActualD[PLM_dest]:
"¬[❙𝒜❙𝒜φ in v] ⟹ ¬[❙𝒜φ in v]"
using ActualActualI by blast
end

lemma ANeg_1[PLM]:
"[❙¬❙𝒜φ ❙≡ ❙¬φ in dw]"
by PLM_solver
lemma ANeg_2[PLM]:
"[❙¬❙𝒜❙¬φ ❙≡ φ in dw]"
by PLM_solver
lemma Act_Basic_1[PLM]:
"[❙𝒜φ ❙∨ ❙𝒜❙¬φ in v]"
by PLM_solver
lemma Act_Basic_2[PLM]:
"[❙𝒜(φ ❙& ψ) ❙≡ (❙𝒜φ ❙& ❙𝒜ψ) in v]"
by PLM_solver
lemma Act_Basic_3[PLM]:
"[❙𝒜(φ ❙≡ ψ) ❙≡ ((❙𝒜(φ ❙→ ψ)) ❙& (❙𝒜(ψ ❙→ φ))) in v]"
by PLM_solver
lemma Act_Basic_4[PLM]:
"[(❙𝒜(φ ❙→ ψ) ❙& ❙𝒜(ψ ❙→ φ)) ❙≡ (❙𝒜φ ❙≡ ❙𝒜ψ) in v]"
by PLM_solver
lemma Act_Basic_5[PLM]:
"[❙𝒜(φ ❙≡ ψ) ❙≡ (❙𝒜φ ❙≡ ❙𝒜ψ