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]"
    by (simp add: Semantics.T5)

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]"
    by (simp add: Semantics.T8)

  lemma RN_2[PLM]:
    "(⋀ v . [ψ in v] ⟹ [φ in v]) ⟹ ([❙□ψ in v] ⟹ [❙□φ in v])"
    by (simp add: Semantics.T6)

  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]"
    by (simp add: Semantics.T5)
  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]"
      by (simp add: "❙¬❙¬I")
    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
      by (simp add: identity_ν_def)
  next
    fix x y::ν and v
    show "[x ❙= y ❙→ y ❙= x in v]"
      using PLM.id_eq_obj_2
      by (simp add: identity_ν_def)
  next
    fix x y z::ν and v
    show "[((x ❙= y) ❙& (y ❙= z)) ❙→ x ❙= z in v]"
      using PLM.id_eq_obj_3
      by (simp add: identity_ν_def)
  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]"
            using 1 "❙&E"(2) qml_2[axiom_instance]
              ded_thm_cor_3 "❙∀E" by fastforce
        }
        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]:
    "[❙𝒜(φ ❙≡ ψ) ❙≡ (❙𝒜φ