subsection‹(Modally Strict) Proofs and Derivations› text‹\label{TAO_PLM_ProofsAndDerivations}›
lemma vdash_properties_6[no_atp]: "[[φ in v]; [φ \<rightarrow> ψ in v]]==> [ψ in v]" using modus_ponens . lemma vdash_properties_9[PLM]: "[φ in v] ==> [ψ \<rightarrow> φ in v]" using modus_ponens pl_1[axiom_instance] by blast lemma vdash_properties_10[PLM]: "[φ \<rightarrow> ψ in v] ==> ([φ in v] ==> [ψ in v])" using vdash_properties_6 .
subsection‹GEN and RN› text‹\label{TAO_PLM_GEN_RN}›
lemma rule_gen[PLM]: "[∧α . [φ α in v]]==> [\<forall>α . φ α in v]" by (simp add: Semantics.T8)
lemma RN_2[PLM]: "(∧ v . [ψ in v] ==> [φ in v]) ==> ([\<box>ψ in v] ==> [\<box>φ in v])" by (simp add: Semantics.T6)
lemma RN[PLM]: "(∧ v . [φ in v]) ==> [\<box>φ 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]: "[φ \<rightarrow> φ in v]" using pl_1 pl_2 vdash_properties_10 axiom_instance by blast
lemma deduction_theorem[PLM,PLM_intro]: "[[φ in v] ==> [ψ in v]]==> [φ \<rightarrow> ψ in v]" by (simp add: Semantics.T5) lemmas CP = deduction_theorem
lemma ded_thm_cor_3[PLM]: "[[φ \<rightarrow> ψ in v]; [ψ \<rightarrow> χ in v]]==> [φ \<rightarrow> χ in v]" by (meson pl_2 vdash_properties_10 vdash_properties_9 axiom_instance) lemma ded_thm_cor_4[PLM]: "[[φ \<rightarrow> (ψ \<rightarrow> χ) in v]; [ψ in v]]==> [φ \<rightarrow> χ in v]" by (meson pl_2 vdash_properties_10 vdash_properties_9 axiom_instance)
lemma useful_tautologies_1[PLM]: "[\<not>\<not>φ \<rightarrow> φ in v]" by (meson pl_1 pl_3 ded_thm_cor_3 ded_thm_cor_4 axiom_instance) lemma useful_tautologies_2[PLM]: "[φ \<rightarrow> \<not>\<not>φ 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]: "[\<not>φ \<rightarrow> (φ \<rightarrow> ψ) 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]: "[(\<not>ψ \<rightarrow> \<not>φ) \<rightarrow> (φ \<rightarrow> ψ) 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]: "[(φ \<rightarrow> ψ) \<rightarrow> (\<not>ψ \<rightarrow> \<not>φ) in v]" by (metis CP useful_tautologies_4 vdash_properties_10) lemma useful_tautologies_6[PLM]: "[(φ \<rightarrow> \<not>ψ) \<rightarrow> (ψ \<rightarrow> \<not>φ) in v]" by (metis CP useful_tautologies_4 vdash_properties_10) lemma useful_tautologies_7[PLM]: "[(\<not>φ \<rightarrow> ψ) \<rightarrow> (\<not>ψ \<rightarrow> φ) in v]" using ded_thm_cor_3 useful_tautologies_4 useful_tautologies_5
useful_tautologies_6 by blast lemma useful_tautologies_8[PLM]: "[φ \<rightarrow> (\<not>ψ \<rightarrow> \<not>(φ \<rightarrow> ψ)) in v]" by (meson ded_thm_cor_3 CP useful_tautologies_5) lemma useful_tautologies_9[PLM]: "[(φ \<rightarrow> ψ) \<rightarrow> ((\<not>φ \<rightarrow> ψ) \<rightarrow> ψ) in v]" by (metis CP useful_tautologies_4 vdash_properties_10) lemma useful_tautologies_10[PLM]: "[(φ \<rightarrow> \<not>ψ) \<rightarrow> ((φ \<rightarrow> ψ) \<rightarrow> \<not>φ) in v]" by (metis ded_thm_cor_3 CP useful_tautologies_6)
lemma modus_tollens_1[PLM]: "[[φ \<rightarrow> ψ in v]; [\<not>ψ in v]]==> [\<not>φ 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]: "[[φ \<rightarrow> \<not>ψ in v]; [ψ in v]]==> [\<not>φ in v]" using modus_tollens_1 useful_tautologies_2
vdash_properties_10 by blast
lemma contraposition_1[PLM]: "[φ \<rightarrow> ψ in v] = [\<not>ψ \<rightarrow> \<not>φ in v]" using useful_tautologies_4 useful_tautologies_5
vdash_properties_10 by blast lemma contraposition_2[PLM]: "[φ \<rightarrow> \<not>ψ in v] = [ψ \<rightarrow> \<not>φ in v]" using contraposition_1 ded_thm_cor_3
useful_tautologies_1 by blast
lemma reductio_aa_1[PLM]: "[[\<not>φ in v] ==> [\<not>ψ in v]; [\<not>φ 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] ==> [\<not>ψ in v]; [φ in v] ==> [ψ in v]]==> [\<not>φ in v]" by (meson contraposition_1 reductio_aa_1) lemma reductio_aa_3[PLM]: "[[\<not>φ \<rightarrow> \<not>ψ in v]; [\<not>φ \<rightarrow> ψ in v]]==> [φ in v]" using reductio_aa_1 vdash_properties_10 by blast lemma reductio_aa_4[PLM]: "[[φ \<rightarrow> \<not>ψ in v]; [φ \<rightarrow> ψ in v]]==> [\<not>φ in v]" using reductio_aa_2 vdash_properties_10 by blast
lemma raa_cor_1[PLM]: "[[φ in v]; [\<not>ψ in v] ==> [\<not>φ in v]]==> ([φ in v] ==> [ψ in v])" using reductio_aa_1 vdash_properties_9 by blast lemma raa_cor_2[PLM]: "[[\<not>φ in v]; [\<not>ψ in v] ==> [φ in v]]==> ([\<not>φ in v] ==> [ψ in v])" using reductio_aa_1 vdash_properties_9 by blast lemma raa_cor_3[PLM]: "[[φ in v]; [\<not>ψ \<rightarrow> \<not>φ in v]]==> ([φ in v] ==> [ψ in v])" using raa_cor_1 vdash_properties_10 by blast lemma raa_cor_4[PLM]: "[[\<not>φ in v]; [\<not>ψ \<rightarrow> φ in v]]==> ([\<not>φ 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] ==> [φ \<or> ψ in v]" unfolding disj_def using ded_thm_cor_4 useful_tautologies_3 by blast lemma intro_elim_3_b[PLM]: "[ψ in v] ==> [φ \<or> ψ in v]" by (simp only: disj_def vdash_properties_9) lemmas"\<or>I" = intro_elim_3_a intro_elim_3_b lemma intro_elim_4_a[PLM]: "[[φ \<or> ψ in v]; [φ \<rightarrow> χ in v]; [ψ \<rightarrow> χ in v]]==> [χ in v]" unfolding disj_def by (meson reductio_aa_2 vdash_properties_10) lemma intro_elim_4_b[PLM]: "[[φ \<or> ψ in v]; [\<not>φ in v]]==> [ψ in v]" unfolding disj_def using vdash_properties_10 by blast lemma intro_elim_4_c[PLM]: "[[φ \<or> ψ in v]; [\<not>ψ in v]]==> [φ in v]" unfolding disj_def using raa_cor_2 vdash_properties_10 by blast lemma intro_elim_4_d[PLM]: "[[φ \<or> ψ in v]; [φ \<rightarrow> χ in v]; [ψ \<rightarrow> Θ in v]]==> [χ \<or> Θ in v]" unfolding disj_def using contraposition_1 ded_thm_cor_3 by blast lemma intro_elim_4_e[PLM]: "[[φ \<or> ψ in v]; [φ \<equiv> χ in v]; [ψ \<equiv> Θ in v]]==> [χ \<or> Θ in v]" unfolding equiv_def using"&E"(1) intro_elim_4_d by blast lemmas"\<or>E" = intro_elim_4_a intro_elim_4_b intro_elim_4_c intro_elim_4_d lemma intro_elim_5[PLM]: "[[φ \<rightarrow> ψ in v]; [ψ \<rightarrow> φ in v]]==> [φ \<equiv> ψ in v]" by (simp only: equiv_def "&I") lemmas"\<equiv>I" = intro_elim_5 lemma intro_elim_6_a[PLM]: "[[φ \<equiv> ψ in v]; [φ in v]]==> [ψ in v]" unfolding equiv_def using"&E"(1) vdash_properties_10 by blast lemma intro_elim_6_b[PLM]: "[[φ \<equiv> ψ in v]; [ψ in v]]==> [φ in v]" unfolding equiv_def using"&E"(2) vdash_properties_10 by blast lemma intro_elim_6_c[PLM]: "[[φ \<equiv> ψ in v]; [\<not>φ in v]]==> [\<not>ψ in v]" unfolding equiv_def using"&E"(2) modus_tollens_1 by blast lemma intro_elim_6_d[PLM]: "[[φ \<equiv> ψ in v]; [\<not>ψ in v]]==> [\<not>φ in v]" unfolding equiv_def using"&E"(1) modus_tollens_1 by blast lemma intro_elim_6_e[PLM]: "[[φ \<equiv> ψ in v]; [ψ \<equiv> χ in v]]==> [φ \<equiv> χ in v]" by (metis equiv_def ded_thm_cor_3 "&E""\<equiv>I") lemma intro_elim_6_f[PLM]: "[[φ \<equiv> ψ in v]; [φ \<equiv> χ in v]]==> [χ \<equiv> ψ in v]" by (metis equiv_def ded_thm_cor_3 "&E""\<equiv>I") lemmas"\<equiv>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] ==> [\<not>\<not>φ in v]" using if_p_then_p modus_tollens_2 by blast lemmas"\<not>\<not>I" = intro_elim_7 lemma intro_elim_8[PLM]: "[\<not>\<not>φ in v] ==> [φ in v]" using if_p_then_p raa_cor_2 by blast lemmas"\<not>\<not>E" = intro_elim_8
context begin privatelemma NotNotI[PLM_intro]: "[φ in v] ==> [\<not>(\<not>φ) in v]" by (simp add: "\<not>\<not>I") privatelemma NotNotD[PLM_dest]: "[\<not>(\<not>φ) in v] ==> [φ in v]" using"\<not>\<not>E"by blast
privatelemma ImplI[PLM_intro]: "([φ in v] ==> [ψ in v]) ==> [φ \<rightarrow> ψ in v]" using CP . privatelemma ImplE[PLM_elim, PLM_dest]: "[φ \<rightarrow> ψ in v] ==> ([φ in v] ==> [ψ in v])" using modus_ponens . privatelemma ImplS[PLM_subst]: "[φ \<rightarrow> ψ in v] = ([φ in v] ⟶ [ψ in v])" using ImplI ImplE by blast
privatelemma NotI[PLM_intro]: "([φ in v] ==> (∧ψ .[ψ in v])) ==> [\<not>φ in v]" using CP modus_tollens_2 by blast privatelemmaNotE[PLM_elim,PLM_dest]: "[\<not>φ in v] ==> ([φ in v] ⟶ (∀ψ .[ψ in v]))" using"\<or>I"(2) "\<or>E"(3) by blast privatelemma NotS[PLM_subst]: "[\<not>φ in v] = ([φ in v] ⟶ (∀ψ .[ψ in v]))" using NotI NotEby blast
privatelemma ConjI[PLM_intro]: "[[φ in v]; [ψ in v]]==> [φ & ψ in v]" using"&I"by blast privatelemma ConjE[PLM_elim,PLM_dest]: "[φ & ψ in v] ==> (([φ in v] ∧ [ψ in v]))" using CP "&E"by blast privatelemma ConjS[PLM_subst]: "[φ & ψ in v] = (([φ in v] ∧ [ψ in v]))" using ConjI ConjE by blast
privatelemma DisjI[PLM_intro]: "[φ in v] ∨ [ψ in v] ==> [φ \<or> ψ in v]" using"\<or>I"by blast privatelemma DisjE[PLM_elim,PLM_dest]: "[φ \<or> ψ in v] ==> [φ in v] ∨ [ψ in v]" using CP "\<or>E"(1) by blast privatelemma DisjS[PLM_subst]: "[φ \<or> ψ in v] = ([φ in v] ∨ [ψ in v])" using DisjI DisjE by blast
privatelemma EquivI[PLM_intro]: "[[φ in v] ==> [ψ in v];[ψ in v] ==> [φ in v]]==> [φ \<equiv> ψ in v]" using CP "\<equiv>I"by blast privatelemma EquivE[PLM_elim,PLM_dest]: "[φ \<equiv> ψ in v] ==> (([φ in v] ⟶ [ψ in v]) ∧ ([ψ in v] ⟶ [φ in v]))" using"\<equiv>E"(1) "\<equiv>E"(2) by blast privatelemma EquivS[PLM_subst]: "[φ \<equiv> ψ in v] = ([φ in v] ⟷ [ψ in v])" using EquivI EquivE by blast
privatelemma NotOrD[PLM_dest]: "¬[φ \<or> ψ in v] ==>¬[φ in v] ∧¬[ψ in v]" using"\<or>I"by blast privatelemma NotAndD[PLM_dest]: "¬[φ & ψ in v] ==>¬[φ in v] ∨¬[ψ in v]" using"&I"by blast privatelemma NotEquivD[PLM_dest]: "¬[φ \<equiv> ψ in v] ==> [φ in v] ≠ [ψ in v]" by (meson NotI contraposition_1 "\<equiv>I" vdash_properties_9)
privatelemma BoxI[PLM_intro]: "(∧ v . [φ in v]) ==> [\<box>φ in v]" using RN by blast privatelemma NotBoxD[PLM_dest]: "¬[\<box>φ in v] ==> (∃ v . ¬[φ in v])" using BoxI by blast
privatelemma AllI[PLM_intro]: "(∧ x . [φ x in v]) ==> [\<forall> x . φ x in v]" using rule_gen by blast lemma NotAllD[PLM_dest]: "¬[\<forall> x . φ x in v] ==> (∃ x . ¬[φ x in v])" using AllI by fastforce end
lemma oth_class_taut_1_a[PLM]: "[\<not>(φ &\<not>φ) in v]" by PLM_solver lemma oth_class_taut_1_b[PLM]: "[\<not>(φ \<equiv> \<not>φ) in v]" by PLM_solver lemma oth_class_taut_2[PLM]: "[φ \<or> \<not>φ in v]" by PLM_solver lemma oth_class_taut_3_a[PLM]: "[(φ & φ) \<equiv> φ in v]" by PLM_solver lemma oth_class_taut_3_b[PLM]: "[(φ & ψ) \<equiv> (ψ & φ) in v]" by PLM_solver lemma oth_class_taut_3_c[PLM]: "[(φ & (ψ & χ)) \<equiv> ((φ & ψ) & χ) in v]" by PLM_solver lemma oth_class_taut_3_d[PLM]: "[(φ \<or> φ) \<equiv> φ in v]" by PLM_solver lemma oth_class_taut_3_e[PLM]: "[(φ \<or> ψ) \<equiv> (ψ \<or> φ) in v]" by PLM_solver lemma oth_class_taut_3_f[PLM]: "[(φ \<or> (ψ \<or> χ)) \<equiv> ((φ \<or> ψ) \<or> χ) in v]" by PLM_solver lemma oth_class_taut_3_g[PLM]: "[(φ \<equiv> ψ) \<equiv> (ψ \<equiv> φ) in v]" by PLM_solver lemma oth_class_taut_3_i[PLM]: "[(φ \<equiv> (ψ \<equiv> χ)) \<equiv> ((φ \<equiv> ψ) \<equiv> χ) in v]" by PLM_solver lemma oth_class_taut_4_a[PLM]: "[φ \<equiv> φ in v]" by PLM_solver lemma oth_class_taut_4_b[PLM]: "[φ \<equiv> \<not>\<not>φ in v]" by PLM_solver lemma oth_class_taut_5_a[PLM]: "[(φ \<rightarrow> ψ) \<equiv> \<not>(φ &\<not>ψ) in v]" by PLM_solver lemma oth_class_taut_5_b[PLM]: "[\<not>(φ \<rightarrow> ψ) \<equiv> (φ &\<not>ψ) in v]" by PLM_solver lemma oth_class_taut_5_c[PLM]: "[(φ \<rightarrow> ψ) \<rightarrow> ((ψ \<rightarrow> χ) \<rightarrow> (φ \<rightarrow> χ)) in v]" by PLM_solver lemma oth_class_taut_5_d[PLM]: "[(φ \<equiv> ψ) \<equiv> (\<not>φ \<equiv> \<not>ψ) in v]" by PLM_solver lemma oth_class_taut_5_e[PLM]: "[(φ \<equiv> ψ) \<rightarrow> ((φ \<rightarrow> χ) \<equiv> (ψ \<rightarrow> χ)) in v]" by PLM_solver lemma oth_class_taut_5_f[PLM]: "[(φ \<equiv> ψ) \<rightarrow> ((χ \<rightarrow> φ) \<equiv> (χ \<rightarrow> ψ)) in v]" by PLM_solver lemma oth_class_taut_5_g[PLM]: "[(φ \<equiv> ψ) \<rightarrow> ((φ \<equiv> χ) \<equiv> (ψ \<equiv> χ)) in v]" by PLM_solver lemma oth_class_taut_5_h[PLM]: "[(φ \<equiv> ψ) \<rightarrow> ((χ \<equiv> φ) \<equiv> (χ \<equiv> ψ)) in v]" by PLM_solver lemma oth_class_taut_5_i[PLM]: "[(φ \<equiv> ψ) \<equiv> ((φ & ψ) \<or> (\<not>φ &\<not>ψ)) in v]" by PLM_solver lemma oth_class_taut_5_j[PLM]: "[(\<not>(φ \<equiv> ψ)) \<equiv> ((φ &\<not>ψ) \<or> (\<not>φ & ψ)) in v]" by PLM_solver lemma oth_class_taut_5_k[PLM]: "[(φ \<rightarrow> ψ) \<equiv> (\<not>φ \<or> ψ) in v]" by PLM_solver
lemma oth_class_taut_6_a[PLM]: "[(φ & ψ) \<equiv> \<not>(\<not>φ \<or> \<not>ψ) in v]" by PLM_solver lemma oth_class_taut_6_b[PLM]: "[(φ \<or> ψ) \<equiv> \<not>(\<not>φ &\<not>ψ) in v]" by PLM_solver lemma oth_class_taut_6_c[PLM]: "[\<not>(φ & ψ) \<equiv> (\<not>φ \<or> \<not>ψ) in v]" by PLM_solver lemma oth_class_taut_6_d[PLM]: "[\<not>(φ \<or> ψ) \<equiv> (\<not>φ &\<not>ψ) in v]" by PLM_solver
lemma oth_class_taut_7_a[PLM]: "[(φ & (ψ \<or> χ)) \<equiv> ((φ & ψ) \<or> (φ & χ)) in v]" by PLM_solver lemma oth_class_taut_7_b[PLM]: "[(φ \<or> (ψ & χ)) \<equiv> ((φ \<or> ψ) & (φ \<or> χ)) in v]" by PLM_solver
lemma oth_class_taut_8_a[PLM]: "[((φ & ψ) \<rightarrow> χ) \<rightarrow> (φ \<rightarrow> (ψ \<rightarrow> χ)) in v]" by PLM_solver lemma oth_class_taut_8_b[PLM]: "[(φ \<rightarrow> (ψ \<rightarrow> χ)) \<rightarrow> ((φ & ψ) \<rightarrow> χ) in v]" by PLM_solver
lemma oth_class_taut_9_a[PLM]: "[(φ & ψ) \<rightarrow> φ in v]" by PLM_solver lemma oth_class_taut_9_b[PLM]: "[(φ & ψ) \<rightarrow> ψ in v]" by PLM_solver
lemma oth_class_taut_10_a[PLM]: "[φ \<rightarrow> (ψ \<rightarrow> (φ & ψ)) in v]" by PLM_solver lemma oth_class_taut_10_b[PLM]: "[(φ \<rightarrow> (ψ \<rightarrow> χ)) \<equiv> (ψ \<rightarrow> (φ \<rightarrow> χ)) in v]" by PLM_solver lemma oth_class_taut_10_c[PLM]: "[(φ \<rightarrow> ψ) \<rightarrow> ((φ \<rightarrow> χ) \<rightarrow> (φ \<rightarrow> (ψ &</b> χ))) in v]" by PLM_solver lemma oth_class_taut_10_d[PLM]: "[(φ \<rightarrow> χ) \<rightarrow> ((ψ \<rightarrow> χ) \<rightarrow> ((φ \<or> ψ) \<rightarrow> χ)) in v]" by PLM_solver lemma oth_class_taut_10_e[PLM]: "[(φ \<rightarrow> ψ) \<rightarrow> ((χ \<rightarrow> Θ) \<rightarrow> ((φ & χ) \<rightarrow> (ψ & Θ))) in v]" by PLM_solver lemma oth_class_taut_10_f[PLM]: "[((φ & ψ) \<equiv> (φ & χ)) \<equiv> (φ \<rightarrow> (ψ \<equiv> χ)) in v]" by PLM_solver lemma oth_class_taut_10_g[PLM]: "[((φ & ψ) \<equiv> (χ & ψ)) \<equiv> (ψ \<rightarrow> (φ \<equiv> χ)) in v]" by PLM_solver
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) \<rightarrow> (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)) \<rightarrow> (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) \<rightarrow> (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) \<rightarrow> (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)) \<rightarrow> (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)) \<rightarrow> (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::o) = p in v]" unfolding identity_defs by PLM_solver lemma id_eq_prop_prop_8[PLM]: "[((p::Π0) = q) \<rightarrow> (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::o) = q) \<rightarrow> (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)) \<rightarrow> (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::o) = q) & (q = r)) \<rightarrow> (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) \<equiv> ((O!,x)&(O!,y)&\<box>(\<forall>F . (F,x)\<equiv> (F,y))) in v]" proof (rule "\<equiv>I"; rule CP) assume1: "[x =E y in v]" have"[\<forall> x y . ((xP) =E (yP)) \<equiv> ((O!,xP)&(O!,yP) &\<box>(\<forall>F . (F,xP)\<equiv> (F,yP))) in v]" unfolding identityE_infix_def identityE_def apply (rule lambda_predicates_2_2[axiom_universal, axiom_universal, axiom_instance]) by show_proper moreoverhave"[\<exists> α . (αP) = x in v]" apply (rule cqt_5_mod[where ψ="λ x . x =E y", axiom_instance,deduction]) unfolding identityE_infix_def apply (rule SimpleExOrEnc.intros) using1unfolding identityE_infix_defby auto moreoverhave"[\<exists> β . (βP) = y in v]" apply (rule cqt_5_mod[where ψ="λ y . x =E y",axiom_instance,deduction]) unfolding identityE_infix_def apply (rule SimpleExOrEnc.intros) using1 unfolding identityE_infix_defby auto ultimatelyhave"[(x =E y) \<equiv> ((O!,x)&(O!,y) &\<box>(\<forall>F . (F,x)\<equiv> (F,y))) in v]" using cqt_1_κ[axiom_instance,deduction, deduction] by meson thus"[((O!,x)&(O!,y)&\<box>(\<forall>F . (F,x)\<equiv> (F,y))) in v]" using1"\<equiv>E"(1) by blast next assume1: "[(O!,x)&(O!,y)&\<box>(\<forall>F. (F,x)\<equiv> (F,y)) in v]" have"[\<forall> x y . ((xP) =E (yP)) \<equiv> ((O!,xP)&(O!,yP) &\<box>(\<forall>F . (F,xP)\<equiv> (F,yP))) in v]" unfolding identityE_def identityE_infix_def apply (rule lambda_predicates_2_2[axiom_universal, axiom_universal, axiom_instance]) by show_proper moreoverhave"[\<exists> α . (αP) = x in v]" apply (rule cqt_5_mod[where ψ="λ x . (O!,x)",axiom_instance,deduction]) apply (rule SimpleExOrEnc.intros) using1[conj1,conj1] by auto moreoverhave"[\<exists> β . (βP) = y in v]" apply (rule cqt_5_mod[where ψ="λ y . (O!,y)",axiom_instance,deduction]) apply (rule SimpleExOrEnc.intros) using1[conj1,conj2] by auto ultimatelyhave"[(x =E y) \<equiv> ((O!,x)&(O!,y) &\<box>(\<forall>F . (F,x)\<equiv> (F,y))) in v]" using cqt_1_κ[axiom_instance,deduction, deduction] by meson thus"[(x =E y) in v]"using1"\<equiv>E"(2) by blast qed lemma eq_E_simple_2[PLM]: "[(x =E y) \<rightarrow> (x = y) in v]" unfolding identity_defs by PLM_solver lemma eq_E_simple_3[PLM]: "[(x = y) \<equiv> (((O!,x)&(O!,y)&\<box>(\<forall>F . (F,x)\<equiv> (F,y))) \<or> ((A!,x)&(A!,y)&\<box>(\<forall>F. {x,F}\<equiv> {y,F}))) in v]" using eq_E_simple_1 apply - unfolding identity_defs by PLM_solver
lemma id_eq_obj_1[PLM]: "[(xP) = (xP) in v]" proof - have"[(\<diamond>(E!, xP)) \<or> (\<not>\<diamond>(E!, xP)) in v]" using PLM.oth_class_taut_2 by simp hence"[(\<diamond>(E!, xP)) in v] ∨ [(\<not>\<diamond>(E!, xP)) in v]" using CP "\<or>E"(1) by blast moreover { assume"[(\<diamond>(E!, xP)) in v]" hence"[(\<lambda>x. \<diamond>(E!,xP),xP) in v]" apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl, rotated]) by show_proper hence"[(\<lambda>x. \<diamond>(E!,xP),xP)&(\<lambda>x. \<diamond>(E!,xP),xP) &\<box>(\<forall>F. (F,xP)\<equiv> (F,xP)) in v]" apply - by PLM_solver hence"[(xP) =E (xP) in v]" using eq_E_simple_1[equiv_rl] unfolding Ordinary_def by fast
} moreover { assume"[(\<not>\<diamond>(E!, xP)) in v]" hence"[(\<lambda>x. \<not>\<diamond>(E!,xP),xP) in v]" apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl, rotated]) by show_proper hence"[(\<lambda>x. \<not>\<diamond>(E!,xP),xP)&(\<lambda>x. \<not>\<diamond>(E!,xP),xP) &\<box>(\<forall>F. {xP,F}\<equiv> {xP,F}) in v]" apply - by PLM_solver
} ultimatelyshow ?thesis unfolding identity_defs Ordinary_def Abstract_def using"\<or>I"by blast qed lemma id_eq_obj_2[PLM]: "[((xP) = (yP)) \<rightarrow> ((yP) = (xP)) in v]" by (meson l_identity[axiom_instance] id_eq_obj_1 CP ded_thm_cor_3) lemma id_eq_obj_3[PLM]: "[((xP) = (yP)) & ((yP) = (zP)) \<rightarrow> ((xP) = (zP)) 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) \<rightarrow> (y = x) in v]" assumes id_eq_3: "[((x :: 'a) = y) & (y = z) \<rightarrow> (x = z) in v]"
instantiation ν :: id_eq begin instanceproof 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 \<rightarrow> 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)) \<rightarrow> x = z in v]" using PLM.id_eq_obj_3 by (simp add: identity_ν_def) qed end
instantiationo :: id_eq begin instanceproof fix x :: oand v show"[x = x in v]" using PLM.id_eq_prop_prop_7 . next fix x y :: oand v show"[x = y \<rightarrow> y = x in v]" using PLM.id_eq_prop_prop_8 . next fix x y z :: oand v show"[((x = y) & (y = z)) \<rightarrow> x = z in v]" using PLM.id_eq_prop_prop_9 . qed end
instantiation Π1 :: id_eq begin instanceproof fix x :: Π1and v show"[x = x in v]" using PLM.id_eq_prop_prop_1 . next fix x y :: Π1and v show"[x = y \<rightarrow> y = x in v]" using PLM.id_eq_prop_prop_2 . next fix x y z :: Π1and v show"[((x = y) & (y = z)) \<rightarrow> x = z in v]" using PLM.id_eq_prop_prop_3 . qed end
instantiation Π2 :: id_eq begin instanceproof fix x :: Π2and v show"[x = x in v]" using PLM.id_eq_prop_prop_4_a . next fix x y :: Π2and v show"[x = y \<rightarrow> y = x in v]" using PLM.id_eq_prop_prop_5_a . next fix x y z :: Π2and v show"[((x = y) & (y = z)) \<rightarrow> x = z in v]" using PLM.id_eq_prop_prop_6_a . qed end
instantiation Π3 :: id_eq begin instanceproof fix x :: Π3and v show"[x = x in v]" using PLM.id_eq_prop_prop_4_b . next fix x y :: Π3and v show"[x = y \<rightarrow> y = x in v]" using PLM.id_eq_prop_prop_5_b . next fix x y z :: Π3and v show"[((x = y) & (y = z)) \<rightarrow> 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) \<rightarrow> (y = x) in v]" using id_eq_2 . lemma id_eq_3[PLM]: "[((x::'a::id_eq) = y) & (y = z) \<rightarrow> (x = z) in v]" using id_eq_3 .
lemma rule_ui[PLM,PLM_elim,PLM_dest]: "[\<forall>α . φ α in v] ==> [φ β in v]" by (meson cqt_1[axiom_instance, deduction]) lemmas"\<forall>E" = rule_ui
lemma rule_ui_2[PLM,PLM_elim,PLM_dest]: "[[\<forall>α . φ (αP) in v]; [\<exists> α . (α)P= β in v]]==> [φ β in v]" using cqt_1_κ[axiom_instance, deduction, deduction] by blast
lemma cqt_orig_1[PLM]: "[(\<forall>α. φ α) \<rightarrow> φ β in v]" by PLM_solver lemma cqt_orig_2[PLM]: "[(\<forall>α. φ \<rightarrow> ψ α) \<rightarrow> (φ \<rightarrow> (\<forall>α. ψ α)) in v]" by PLM_solver
lemma universal[PLM]: "(∧α . [φ α in v]) ==> [\<forall> α . φ α in v]" using rule_gen . lemmas"\<forall>I" = universal
lemma cqt_basic_1[PLM]: "[(\<forall>α. (\<forall>β . φ α β)) \<equiv> (\<forall>β. (\<forall>α. φ α β)) in v]" by PLM_solver lemma cqt_basic_2[PLM]: "[(\<forall>α. φ α \<equiv> ψ α) \<equiv> ((\<forall>α. φ α \<rightarrow> ψ α) & (\<forall>α. ψ α\<rightarrow> φ α)) in v]" by PLM_solver lemma cqt_basic_3[PLM]: "[(\<forall>α. φ α \<equiv> ψ α) \<rightarrow> ((\<forall>α. φ α) \<equiv> (\<forall>α. ψ α)) in v]" by PLM_solver lemma cqt_basic_4[PLM]: "[(\<forall>α. φ α & ψ α) \<equiv> ((\<forall>α. φ α) & (\<forall>α. ψ α)) in v]" by PLM_solver lemma cqt_basic_6[PLM]: "[(\<forall>α. (\<forall>α. φ α)) \<equiv> (\<forall>α. φ α) in v]" by PLM_solver lemma cqt_basic_7[PLM]: "[(φ \<rightarrow> (\<forall>α . ψ α)) \<equiv> (\<forall>α.(φ \<rightarrow> ψ α)) in v]" by PLM_solver lemma cqt_basic_8[PLM]: "[((\<forall>α. φ α) \<or> (\<forall>α. ψ α)) \<rightarrow> (\<forall>α. (φ α \<or> ψ α)) in v]" by PLM_solver lemma cqt_basic_9[PLM]: "[((\<forall>α. φ α \<rightarrow> ψ α) & (\<forall>α. ψ α \<rightarrow> χ α)) \<rightarrow> (\<forall>α. φ α \<rightarrow> χ α) in v]" by PLM_solver lemma cqt_basic_10[PLM]: "[((\<forall>α. φ α \<equiv> ψ α) & (\<forall>α. ψ α \<equiv> χ α)) \<rightarrow> (\<forall>α. φ α \<equiv> χ α) in v]" by PLM_solver lemma cqt_basic_11[PLM]: "[(\<forall>α. φ α \<equiv> ψ α) \<equiv> (\<forall>α. ψ α \<equiv> φ α) in v]" by PLM_solver lemma cqt_basic_12[PLM]: "[(\<forall>α. φ α) \<equiv> (\<forall>β. φ β) in v]" by PLM_solver
lemma existential[PLM,PLM_intro]: "[φ α in v] ==> [\<exists> α. φ α in v]" unfolding exists_def by PLM_solver lemmas"\<exists>I" = existential lemma instantiation_[PLM,PLM_elim,PLM_dest]: "[[\<exists>α . φ α in v]; (∧α.[φ α in v] ==> [ψ in v])]==> [ψ in v]" unfolding exists_def by PLM_solver
lemma Instantiate: assumes"[\<exists> x . φ x in v]" obtains x where"[φ x in v]" apply (insert assms) unfolding exists_def by PLM_solver lemmas"\<exists>E" = Instantiate
lemma cqt_further_1[PLM]: "[(\<forall>α. φ α) \<rightarrow> (\<exists>α. φ α) in v]" by PLM_solver lemma cqt_further_2[PLM]: "[(\<not>(\<forall>α. φ α)) \<equiv> (\<exists>α. \<not>φ α) in v]" unfolding exists_def by PLM_solver lemma cqt_further_3[PLM]: "[(\<forall>α. φ α) \<equiv> \<not>(\<exists>α. \<not>φ α) in v]" unfolding exists_def by PLM_solver lemma cqt_further_4[PLM]: "[(\<not>(\<exists>α. φ α)) \<equiv> (\<forall>α. \<not>φ α) in v]" unfolding exists_def by PLM_solver lemma cqt_further_5[PLM]: "[(\<exists>α. φ α & ψ α) \<rightarrow> ((\<exists>α. φ α) & (\<exists>α. ψ α)) in v]" unfolding exists_def by PLM_solver lemma cqt_further_6[PLM]: "[(\<exists>α. φ α \<or> ψ α) \<equiv> ((\<exists>α. φ α) \<or> (\<exists>α. ψ α)) in v]" unfolding exists_def by PLM_solver lemma cqt_further_10[PLM]: "[(φ (α::'a::id_eq) & (\<forall> β . φ β \<rightarrow> β = α)) \<equiv> (\<forall> β . φ β \<equiv> β = α) 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]: "[((\<forall>α. φ α) & (\<forall>α. ψ α)) \<rightarrow> (\<forall>α. φ α \<equiv> ψ α) in v]" by PLM_solver lemma cqt_further_12[PLM]: "[((\<not>(\<exists>α. φ α)) & (\<not>(\<exists>α. ψ α))) \<rightarrow> (\<forall>α. φ α \<equiv> ψ α) in v]" unfolding exists_def by PLM_solver lemma cqt_further_13[PLM]: "[((\<exists>α. φ α) & (\<not>(\<exists>α. ψ α))) \<rightarrow> (\<not>(\<forall>α. φ α \<equiv> ψ α)) in v]" unfolding exists_def by PLM_solver lemma cqt_further_14[PLM]: "[(\<exists>α. \<exists>β. φ α β) \<equiv> (\<exists>β. \<exists>α. φ α β) in v]" unfolding exists_def by PLM_solver
lemma nec_exist_unique[PLM]: "[(\<forall> x. φ x \<rightarrow> \<box>(φ x)) \<rightarrow> ((\<exists>!x. φ x) \<rightarrow> (\<exists>!x. \<box>(φ x))) in v]" proof (rule CP) assume a: "[\<forall>x. φ x \<rightarrow> \<box>φ x in v]" show"[(\<exists>!x. φ x) \<rightarrow> (\<exists>!x. \<box>φ x) in v]" proof (rule CP) assume"[(\<exists>!x. φ x) in v]" hence"[\<exists>α. φ α & (\<forall>β. φ β \<rightarrow> β = α) in v]" by (simp only: exists_unique_def) thenobtain α where1: "[φ α & (\<forall>β. φ β \<rightarrow> β = α) in v]" by (rule "\<exists>E")
{ fix β have"[\<box>φ β \<rightarrow> β = α in v]" by (metis "1" Semantics.T5 Semantics.T6 cqt_orig_1 oth_class_taut_9_b)
} hence"[\<forall>β. \<box>φ β \<rightarrow> β = α in v]"by (rule "\<forall>I") moreoverhave"[\<box>(φ α) in v]" using1"&E"(1) a vdash_properties_10 cqt_orig_1[deduction] by fast ultimatelyhave"[\<exists>α. \<box>(φ α) & (\<forall>β. \<box>φ β \<rightarrow> β = α) in v]" using"&I""\<exists>I"by fast thus"[(\<exists>!x. \<box>φ 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]: "[\<box>φ \<rightarrow> \<A>φ 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]: "[\<A>(\<A>φ \<rightarrow> φ) in v]" using equiv_def logic_actual_nec_2[axiom_instance]
logic_actual_nec_4[axiom_instance] "&E"(2) "\<equiv>E"(2) by metis lemma act_conj_act_2[PLM]: "[\<A>(φ \<rightarrow> \<A>φ) in v]" using logic_actual_nec_2[axiom_instance] qml_act_1[axiom_instance]
ded_thm_cor_3 "\<equiv>E"(2) nec_imp_act by blast lemma act_conj_act_3[PLM]: "[(\<A>φ &\<A>ψ) \<rightarrow> \<A>(φ & ψ) in v]" unfolding conn_defs by (metis logic_actual_nec_2[axiom_instance]
logic_actual_nec_1[axiom_instance] "\<equiv>E"(2) CP "\<equiv>E"(4) reductio_aa_2
vdash_properties_10) lemma act_conj_act_4[PLM]: "[\<A>(\<A>φ \<equiv> φ) in v]" unfolding equiv_def by (PLM_solver PLM_intro: act_conj_act_3[where φ="\<A>φ \<rightarrow> φ" and ψ="φ \<rightarrow> \<A>φ", deduction]) lemma closure_act_1a[PLM]: "[\<A>\<A>(\<A>φ \<equiv> φ) in v]" using logic_actual_nec_4[axiom_instance]
act_conj_act_4 "\<equiv>E"(1) by blast lemma closure_act_1b[PLM]: "[\<A>\<A>\<A>(\<A>φ \<equiv> φ) in v]" using logic_actual_nec_4[axiom_instance]
act_conj_act_4 "\<equiv>E"(1) by blast lemma closure_act_1c[PLM]: "[\<A>\<A>\<A>\<A>(\<A>φ \<equiv> φ) in v]" using logic_actual_nec_4[axiom_instance]
act_conj_act_4 "\<equiv>E"(1) by blast lemma closure_act_2[PLM]: "[\<forall>α. \<A>(\<A>(φ α) \<equiv> φ α) in v]" by PLM_solver
lemma closure_act_3[PLM]: "[\<A>(\<forall>α. \<A>(φ α) \<equiv> φ α) in v]" by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl]) lemma closure_act_4[PLM]: "[\<A>(\<forall>α1 α2. \<A>(φ α1 α2) \<equiv> φ α1 α2) in v]" by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl]) lemma closure_act_4_b[PLM]: "[\<A>(\<forall>α1 α2 α3. \<A>(φ α1 α2 α3) \<equiv> φ α1 α2 α3) in v]" by (PLM_solver PLM_intro: logic_actual_nec_3[axiom_instance, equiv_rl]) lemma closure_act_4_c[PLM]: "[\<A>(\<forall>α1 α2 α3 α4. \<A>(φ α1 α2 α3 α4) \<equiv> φ α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]) ==> [\<A>φ in dw]" using logic_actual[necessitation_averse_axiom_instance, equiv_rl] .
lemma RA_2[PLM,PLM_intro]: "([ψ in dw] ==> [φ in dw]) ==> ([\<A>ψ in dw] ==> [\<A>φ in dw])" using RA logic_actual[necessitation_averse_axiom_instance] intro_elim_6_a by blast
context begin privatelemma ActualE[PLM,PLM_elim,PLM_dest]: "[\<A>φ in dw] ==> [φ in dw]" using logic_actual[necessitation_averse_axiom_instance, equiv_lr] .
privatelemma NotActualD[PLM_dest]: "¬[\<A>φ in dw] ==>¬[φ in dw]" using RA by metis
privatelemma ActualImplI[PLM_intro]: "[\<A>φ \<rightarrow> \<A>ψ in v] ==> [\<A>(φ \<rightarrow> ψ) in v]" using logic_actual_nec_2[axiom_instance, equiv_rl] . privatelemma ActualImplE[PLM_dest, PLM_elim]: "[\<A>(φ \<rightarrow> ψ) in v] ==> [\<A>φ \<rightarrow> \<A>ψ in v]" using logic_actual_nec_2[axiom_instance, equiv_lr] . privatelemma NotActualImplD[PLM_dest]: "¬[\<A>(φ \<rightarrow> ψ) in v] ==>¬[\<A>φ \<rightarrow> \<A>ψ in v]" using ActualImplI by blast
privatelemma ActualNotI[PLM_intro]: "[\<not>\<A>φ in v] ==> [\<A>\<not>φ in v]" using logic_actual_nec_1[axiom_instance, equiv_rl] . lemma ActualNotE[PLM_elim,PLM_dest]: "[\<A>\<not>φ in v] ==> [\<not>\<A>φ in v]" using logic_actual_nec_1[axiom_instance, equiv_lr] . lemma NotActualNotD[PLM_dest]: "¬[\<A>\<not>φ in v] ==>¬[\<not>\<A>φ in v]" using ActualNotI by blast
privatelemma ActualConjI[PLM_intro]: "[\<A>φ &\<A>ψ in v] ==> [\<A>(φ & ψ) in v]" unfolding equiv_def by (PLM_solver PLM_intro: act_conj_act_3[deduction]) privatelemma ActualConjE[PLM_elim,PLM_dest]: "[\<A>(φ & ψ) in v] ==> [\<A>φ &\<A>ψ in v]" unfolding conj_def by PLM_solver
privatelemma ActualEquivI[PLM_intro]: "[\<A>φ \<equiv> \<A>ψ in v] ==> [\<A>(φ \<equiv> ψ) in v]" unfolding equiv_def by (PLM_solver PLM_intro: act_conj_act_3[deduction]) privatelemma ActualEquivE[PLM_elim, PLM_dest]: "[\<A>(φ \<equiv> ψ) in v] ==> [\<A>φ \<equiv> \<A>ψ in v]" unfolding equiv_def by PLM_solver
privatelemma ActualBoxI[PLM_intro]: "[\<box>φ in v] ==> [\<A>(\<box>φ) in v]" using qml_act_2[axiom_instance, equiv_lr] . privatelemma ActualBoxE[PLM_elim, PLM_dest]: "[\<A>(\<box>φ) in v] ==> [\<box>φ in v]" using qml_act_2[axiom_instance, equiv_rl] . privatelemma NotActualBoxD[PLM_dest]: "¬[\<A>(\<box>φ) in v] ==>¬[\<box>φ in v]" using ActualBoxI by blast
privatelemma ActualDisjI[PLM_intro]: "[\<A>φ \<or> \<A>ψ in v] ==> [\<A>(φ \<or> ψ) in v]" unfolding disj_def by PLM_solver privatelemma ActualDisjE[PLM_elim,PLM_dest]: "[\<A>(φ \<or> ψ) in v] ==> [\<A>φ \<or> \<A>ψ in v]" unfolding disj_def by PLM_solver privatelemma NotActualDisjD[PLM_dest]: "¬[\<A>(φ \<or> ψ) in v] ==>¬[\<A>φ \<or> \<A>ψ in v]" using ActualDisjI by blast
privatelemma ActualForallI[PLM_intro]: "[\<forall> x . \<A>(φ x) in v] ==> [\<A>(\<forall> x . φ x) in v]" using logic_actual_nec_3[axiom_instance, equiv_rl] . lemma ActualForallE[PLM_elim,PLM_dest]: "[\<A>(\<forall> x . φ x) in v] ==> [\<forall> x . \<A>(φ x) in v]" using logic_actual_nec_3[axiom_instance, equiv_lr] . lemma NotActualForallD[PLM_dest]: "¬[\<A>(\<forall> x . φ x) in v] ==>¬[\<forall> x . \<A>(φ x) in v]" using ActualForallI by blast
lemma ActualActualI[PLM_intro]: "[\<A>φ in v] ==> [\<A>\<A>φ in v]" using logic_actual_nec_4[axiom_instance, equiv_lr] . lemma ActualActualE[PLM_elim,PLM_dest]: "[\<A>\<A>φ in v] ==> [\<A>φ in v]" using logic_actual_nec_4[axiom_instance, equiv_rl] . lemma NotActualActualD[PLM_dest]: "¬[\<A>\<A>φ in v] ==>¬[\<A>φ in v]" using ActualActualI by blast end
lemma ANeg_1[PLM]: "[\<not>\<A>φ \<equiv> \<not>φ in dw]" by PLM_solver lemma ANeg_2[PLM]: "[\<not>\<A>\<not>φ \<equiv> φ in dw]" by PLM_solver lemma Act_Basic_1[PLM]: "[\<A>φ \<or> \<A>\<not>φ in v]" by PLM_solver lemma Act_Basic_2[PLM]: "[\<A>(φ & ψ) \<equiv> (\<A>φ &\<A>ψ) in v]" by PLM_solver lemma Act_Basic_3[PLM]: "[\<A>(φ \<equiv> ψ) \<equiv> ((\<A>(φ \<rightarrow> ψ)) & (\<A>(ψ \<rightarrow> φ))) in v]" by PLM_solver lemma Act_Basic_4[PLM]: "[(\<A>(φ \<rightarrow> ψ) &\<A>(ψ \<rightarrow> φ)) \<equiv> (\<A>φ \<equiv> \<A>ψ) in v]" by PLM_solver lemma Act_Basic_5[PLM]: "[\<A>(φ \<equiv> ψ) \<equiv> (\<A>φ \<equiv> \<A>ψ) in v]" by PLM_solver lemma Act_Basic_6[PLM]: "[\<diamond>φ \<equiv> \<A>(\<diamond>φ) in v]" unfolding diamond_def by PLM_solver lemma Act_Basic_7[PLM]: "[\<A>φ \<equiv> \<box>\<A>φ in v]" by (simp add: qml_2[axiom_instance] qml_act_1[axiom_instance] "\<equiv>I") lemma Act_Basic_8[PLM]: "[\<A>(\<box>φ) \<rightarrow> \<box>\<A>φ in v]" by (metis qml_act_2[axiom_instance] CP Act_Basic_7 "\<equiv>E"(1) "\<equiv>E"(2) nec_imp_act vdash_properties_10) lemma Act_Basic_9[PLM]: "[\<box>φ \<rightarrow> \<box>\<A>φ in v]" using qml_act_1[axiom_instance] ded_thm_cor_3 nec_imp_act by blast lemma Act_Basic_10[PLM]: "[\<A>(φ \<or> ψ) \<equiv> \<A>φ \<or> \<A>ψ in v]" by PLM_solver
lemma Act_Basic_11[PLM]: "[\<A>(\<exists>α. φ α) \<equiv> (\<exists>α.\<A>(φ α)) in v]" proof - have"[\<A>(\<forall> α . \<not>φ α) \<equiv> (\<forall> α . \<A>\<not>φ α) in v]" using logic_actual_nec_3[axiom_instance] by blast hence"[\<not>\<A>(\<forall> α . \<not>φ α) \<equiv> \<not>(\<forall> α . \<A>\<not>φ α) in v]" using oth_class_taut_5_d[equiv_lr] by blast moreoverhave"[\<A>\<not>(\<forall> α . \<not>φ α) \<equiv> \<not>\<A>(\<forall> α . \<not>φ α) in v]" using logic_actual_nec_1[axiom_instance] by blast ultimatelyhave"[\<A>\<not>(\<forall> α . \<not>φ α) \<equiv> \<not>(\<forall> α . \<A>\<not>φ α) in v]" using"\<equiv>E"(5) by blast moreover { have"[\<forall> α . \<A>\<not>φ α \<equiv> \<not>\<A>φ α in v]" using logic_actual_nec_1[axiom_universal, axiom_instance] by blast hence"[(\<forall> α . \<A>\<not>φ α) \<equiv> (\<forall> α . \<not>\<A>φ α) in v]" using cqt_basic_3[deduction] by fast hence"[(\<not>(\<forall> α . \<A>\<not>φ α)) \<equiv> \<not>(\<forall> α . \<not>\<A>φ α) in v]" using oth_class_taut_5_d[equiv_lr] by blast
} ultimatelyshow ?thesis by (metis "\<exists>E" MetaSolver.EquivI Semantics.T7 existential) qed
lemma act_quant_uniq[PLM]: "[(\<forall> z . \<A>φ z \<equiv> z = x) \<equiv> (\<forall> z . φ z \<equiv> z = x) in dw]" by PLM_solver
lemma fund_cont_desc[PLM]: "[(xP= (\<iota>x. φ x)) \<equiv> (\<forall> z . φ z \<equiv> (z = x)) in dw]" using descriptions[axiom_instance] act_quant_uniq "\<equiv>E"(5) by fast
lemma hintikka[PLM]: "[(xP= (\<iota>x. φ x)) \<equiv> (φ x & (\<forall> z . φ z \<rightarrow> z = x)) in dw]" proof - have"[(\<forall> z . φ z \<equiv> z = x) \<equiv> (φ x & (\<forall> z . φ z \<rightarrow> z = x)) in dw]" unfolding identity_ν_defapply PLM_solver using id_eq_obj_1 apply simp using l_identity[where φ="λ x . φ x", axiom_instance,
deduction, deduction] using id_eq_obj_2[deduction] unfolding identity_ν_defby fastforce thus ?thesis using"\<equiv>E"(5) fund_cont_desc by blast qed
lemma russell_axiom_a[PLM]: "[((F, \<iota>x. φ x)) \<equiv> (\<exists> x . φ x & (\<forall> z . φ z \<rightarrow> z = x) &(F, xP)) in dw]"
(is"[?lhs \<equiv> ?rhs in dw]") proof -
{ assume1: "[?lhs in dw]" hence"[\<exists>α. αP= (\<iota>x. φ x) in dw]" using cqt_5[axiom_instance, deduction]
SimpleExOrEnc.intros by blast thenobtain α where2: "[αP= (\<iota>x. φ x) in dw]" using"\<exists>E"by auto hence3: "[φ α & (\<forall> z . φ z \<rightarrow> z = α) in dw]" using hintikka[equiv_lr] by simp from2have"[(\<iota>x. φ x) = (αP) in dw]" using l_identity[where α="αP"and β="\<iota>x. φ x"and φ="λ x . x = αP",
axiom_instance, deduction, deduction]
id_eq_obj_1[where x=α] by auto hence"[(F, αP) in dw]" using1 l_identity[where β="αP"and α="\<iota>x. φ x"and φ="λ x . (F,x)",
axiom_instance, deduction, deduction] by auto with3have"[φ α & (\<forall> z . φ z \<rightarrow> z = α) &(F, αP) in dw]"by (rule "&I") hence"[?rhs in dw]"using"\<exists>I"[where α=α] by simp
} moreover { assume"[?rhs in dw]" thenobtain α where4: "[φ α & (\<forall> z . φ z \<rightarrow> z = α) &(F, αP) in dw]" using"\<exists>E"by auto hence"[αP= (\<iota>x . φ x) in dw] ∧ [(F, αP) in dw]" using hintikka[equiv_rl] "&E"by blast hence"[?lhs in dw]" using l_identity[axiom_instance, deduction, deduction] by blast
} ultimatelyshow ?thesis by PLM_solver qed
lemma russell_axiom_g[PLM]: "[{\<iota>x. φ x,F}\<equiv> (\<exists> x . φ x & (\<forall> z . φ z \<rightarrow> z = x) &{xP, F}) in dw]"
(is"[?lhs \<equiv> ?rhs in dw]") proof -
{ assume1: "[?lhs in dw]" hence"[\<exists>α. αP= (\<iota>x. φ x) in dw]" using cqt_5[axiom_instance, deduction] SimpleExOrEnc.introsby blast thenobtain α where2: "[αP= (\<iota>x. φ x) in dw]"by (rule "\<exists>E") hence3: "[(φ α & (\<forall> z . φ z \<rightarrow> z = α)) in dw]" using hintikka[equiv_lr] by simp from2have"[(\<iota>x. φ x) = αP in dw]" using l_identity[where α="αP"and β="\<iota>x. φ x"and φ="λ x . x = αP",
axiom_instance, deduction, deduction]
id_eq_obj_1[where x=α] by auto hence"[{αP, F} in dw]" using1 l_identity[where β="αP"and α="\<iota>x. φ x"and φ="λ x . {x,F}",
axiom_instance, deduction, deduction] by auto with3have"[(φ α & (\<forall> z . φ z \<rightarrow> z = α)) &{αP, F} in dw]" using"&I"by auto hence"[?rhs in dw]"using"\<exists>I"[where α=α] by (simp add: identity_defs)
} moreover { assume"[?rhs in dw]" thenobtain α where4: "[φ α & (\<forall> z . φ z \<rightarrow> z = α) &{αP, F} in dw]" using"\<exists>E"by auto hence"[αP= (\<iota>x . φ x) in dw] ∧ [{αP, F} in dw]" using hintikka[equiv_rl] "&E"by blast hence"[?lhs in dw]" using l_identity[axiom_instance, deduction, deduction] by fast
} ultimatelyshow ?thesis by PLM_solver qed
lemma russell_axiom[PLM]: assumes"SimpleExOrEnc ψ" shows"[ψ (\<iota>x. φ x) \<equiv> (\<exists> x . φ x & (\<forall> z . φ z \<rightarrow> z = x) & ψ (xP)) in dw]"
(is"[?lhs \<equiv> ?rhs in dw]") proof -
{ assume1: "[?lhs in dw]" hence"[\<exists>α. αP= (\<iota>x. φ x) in dw]" using cqt_5[axiom_instance, deduction] assms by blast thenobtain α where2: "[αP= (\<iota>x. φ x) in dw]"by (rule "\<exists>E") hence3: "[(φ α & (\<forall> z . φ z \<rightarrow> z = α)) in dw]" using hintikka[equiv_lr] by simp from2have"[(\<iota>x. φ x) = (αP) in dw]" using l_identity[where α="αP"and β="\<iota>x. φ x"and φ="λ x . x = αP",
axiom_instance, deduction, deduction]
id_eq_obj_1[where x=α] by auto hence"[ψ (αP) in dw]" using1 l_identity[where β="αP"and α="\<iota>x. φ x"and φ="λ x . ψ x",
axiom_instance, deduction, deduction] by auto with3have"[φ α & (\<forall> z . φ z \<rightarrow> z = α) & ψ (αP) in dw]" using"&I"by auto hence"[?rhs in dw]"using"\<exists>I"[where α=α] by (simp add: identity_defs)
} moreover { assume"[?rhs in dw]" thenobtain α where4: "[φ α & (\<forall> z . φ z \<rightarrow> z = α) & ψ (αP) in dw]" using"\<exists>E"by auto hence"[αP= (\<iota>x . φ x) in dw] ∧ [ψ (αP) in dw]" using hintikka[equiv_rl] "&E"by blast hence"[?lhs in dw]" using l_identity[axiom_instance, deduction, deduction] by fast
} ultimatelyshow ?thesis by PLM_solver qed
lemma unique_exists[PLM]: "[(\<exists> y . yP= (\<iota>x. φ x)) \<equiv> (\<exists>!x . φ x) in dw]" proof((rule "\<equiv>I", rule CP, rule_tac[2] CP)) assume"[\<exists>y. yP= (\<iota>x. φ x) in dw]" thenobtain α where "[αP= (\<iota>x. φ x) in dw]" by (rule "\<exists>E") hence"[φ α & (\<forall>β. φ β \<rightarrow> β = α) in dw]" using hintikka[equiv_lr] by auto thus"[\<exists>!x . φ x in dw]" unfolding exists_unique_def using"\<exists>I"by fast next assume"[\<exists>!x . φ x in dw]" thenobtain α where "[φ α & (\<forall>β. φ β \<rightarrow> β = α) in dw]" unfolding exists_unique_def by (rule "\<exists>E") hence"[αP= (\<iota>x. φ x) in dw]" using hintikka[equiv_rl] by auto thus"[\<exists>y. yP= (\<iota>x. φ x) in dw]" using"\<exists>I"by fast qed
lemma y_in_1[PLM]: "[xP= (\<iota>x . φ) \<rightarrow> φ in dw]" using hintikka[equiv_lr, conj1] by (rule CP)
lemma y_in_2[PLM]: "[zP= (\<iota>x . φ x) \<rightarrow> φ z in dw]" using hintikka[equiv_lr, conj1] by (rule CP)
lemma y_in_3[PLM]: "[(\<exists> y . yP= (\<iota>x . φ (xP))) \<rightarrow> φ (\<iota>x . φ (xP)) in dw]" proof (rule CP) assume"[(\<exists> y . yP= (\<iota>x . φ (xP))) in dw]" thenobtain y where1: "[yP= (\<iota>x. φ (xP)) in dw]" by (rule "\<exists>E") hence"[φ (yP) in dw]" using y_in_2[deduction] unfolding identity_ν_defby blast thus"[φ (\<iota>x. φ (xP)) in dw]" using l_identity[axiom_instance, deduction,
deduction] 1by fast qed
lemma act_quant_nec[PLM]: "[(\<forall>z . (\<A>φ z \<equiv> z = x)) \<equiv> (\<forall>z. \<A>\<A>φ z \<equiv> z = x) in v]" by PLM_solver
lemma equi_desc_descA_1[PLM]: "[(xP= (\<iota>x . φ x)) \<equiv> (xP= (\<iota>x . \<A>φ x)) in v]" using descriptions[axiom_instance] apply (rule "\<equiv>E"(5)) using act_quant_nec apply (rule "\<equiv>E"(5)) using descriptions[axiom_instance] by (meson "\<equiv>E"(6) oth_class_taut_4_a)
lemma equi_desc_descA_2[PLM]: "[(\<exists> y . yP= (\<iota>x. φ x)) \<rightarrow> ((\<iota>x . φ x) = (\<iota>x . \<A>φ x)) in v]" proof (rule CP) assume"[\<exists>y. yP= (\<iota>x. φ x) in v]" thenobtain y where "[yP= (\<iota>x. φ x) in v]" by (rule "\<exists>E") moreoverhence"[yP= (\<iota>x. \<A>φ x) in v]" using equi_desc_descA_1[equiv_lr] by auto ultimatelyshow"[(\<iota>x. φ x) = (\<iota>x. \<A>φ x) in v]" using l_identity[axiom_instance, deduction, deduction] by fast qed
lemma equi_desc_descA_3[PLM]: assumes"SimpleExOrEnc ψ" shows"[ψ (\<iota>x. φ x) \<rightarrow> (\<exists> y . yP= (\<iota>x. \<A>φ x)) in v]" proof (rule CP) assume"[ψ (\<iota>x. φ x) in v]" hence"[\<exists>α. αP= (\<iota>x. φ x) in v]" using cqt_5[OF assms, axiom_instance, deduction] by auto thenobtain α where"[αP= (\<iota>x. φ x) in v]"by (rule "\<exists>E") hence"[αP= (\<iota>x . \<A>φ x) in v]" using equi_desc_descA_1[equiv_lr] by auto thus"[\<exists>y. yP= (\<iota>x. \<A>φ x) in v]" using"\<exists>I"by fast qed
lemma equi_desc_descA_4[PLM]: assumes"SimpleExOrEnc ψ" shows"[ψ (\<iota>x. φ x) \<rightarrow> ((\<iota>x. φ x) = (\<iota>x. \<A>φ x)) in v]" proof (rule CP) assume"[ψ (\<iota>x. φ x) in v]" hence"[\<exists>α. αP= (\<iota>x. φ x) in v]" using cqt_5[OF assms, axiom_instance, deduction] by auto thenobtain α where"[αP= (\<iota>x. φ x) in v]"by (rule "\<exists>E") moreoverhence"[αP= (\<iota>x . \<A>φ x) in v]" using equi_desc_descA_1[equiv_lr] by auto ultimatelyshow"[(\<iota>x. φ x) = (\<iota>x . \<A>φ x) in v]" using l_identity[axiom_instance, deduction, deduction] by fast qed
lemma nec_hintikka_scheme[PLM]: "[(xP= (\<iota>x. φ x)) \<equiv> (\<A>φ x & (\<forall> z . \<A>φ z \<rightarrow> z = x)) in v]" using descriptions[axiom_instance] apply (rule "\<equiv>E"(5)) apply PLM_solver using id_eq_obj_1 apply simp using id_eq_obj_2[deduction]
l_identity[where α="x", axiom_instance, deduction, deduction] unfolding identity_ν_def apply blast using l_identity[where α="x", axiom_instance, deduction, deduction]
id_eq_2[where 'a=ν, deduction] unfolding identity_ν_defby meson
lemma equiv_desc_eq[PLM]: assumes"∧x.[\<A>(φ x \<equiv> ψ x) in v]" shows"[(\<forall> x . ((xP= (\<iota>x . φ x)) \<equiv> (xP= (\<iota>x . ψ x)))) in v]" proof(rule "\<forall>I") fix x
{ assume"[xP= (\<iota>x . φ x) in v]" hence1: "[\<A>φ x & (\<forall>z. \<A>φ z \<rightarrow> z = x) in v]" using nec_hintikka_scheme[equiv_lr] by auto hence2: "[\<A>φ x in v] ∧ [(\<forall>z. \<A>φ z \<rightarrow> z = x) in v]" using"&E"by blast
{ fix z
{ assume"[\<A>ψ z in v]" hence"[\<A>φ z in v]" using assms[where x=z] apply - by PLM_solver moreoverhave"[\<A>φ z \<rightarrow> z = x in v]" using2 cqt_1[axiom_instance,deduction] by auto ultimatelyhave"[z = x in v]" using vdash_properties_10 by auto
} hence"[\<A>ψ z \<rightarrow> z = x in v]"by (rule CP)
} hence"[(\<forall> z . \<A>ψ z \<rightarrow> z = x) in v]"by (rule "\<forall>I") moreoverhave"[\<A>ψ x in v]" using1[conj1] assms[where x=x] apply - by PLM_solver ultimatelyhave"[\<A>ψ x & (\<forall>z. \<A>ψ z \<rightarrow> z = x) in v]" by PLM_solver hence"[xP= (\<iota>x. ψ x) in v]" using nec_hintikka_scheme[where φ="ψ", equiv_rl] by auto
} moreover { assume"[xP= (\<iota>x . ψ x) in v]" hence1: "[\<A>ψ x & (\<forall>z. \<A>ψ z \<rightarrow> z = x) in v]" using nec_hintikka_scheme[equiv_lr] by auto hence2: "[\<A>ψ x in v] ∧ [(\<forall>z. \<A>ψ z \<rightarrow> z = x) in v]" using"&E"by blast
{ fix z
{ assume"[\<A>φ z in v]" hence"[\<A>ψ z in v]" using assms[where x=z] apply - by PLM_solver moreoverhave"[\<A>ψ z \<rightarrow> z = x in v]" using2 cqt_1[axiom_instance,deduction] by auto ultimatelyhave"[z = x in v]" using vdash_properties_10 by auto
} hence"[\<A>φ z \<rightarrow> z = x in v]"by (rule CP)
} hence"[(\<forall>z. \<A>φ z \<rightarrow> z = x) in v]"by (rule "\<forall>I") moreoverhave"[\<A>φ x in v]" using1[conj1] assms[where x=x] apply - by PLM_solver ultimatelyhave"[\<A>φ x & (\<forall>z. \<A>φ z \<rightarrow> z = x) in v]" by PLM_solver hence"[xP= (\<iota>x. φ x) in v]" using nec_hintikka_scheme[where φ="φ",equiv_rl] by auto
} ultimatelyshow"[xP= (\<iota>x. φ x) \<equiv> (xP) = (\<iota>x. ψ x) in v]" using"\<equiv>I" CP by auto qed
lemma UniqueAux: assumes"[(\<A>φ (α::ν) & (\<forall> z . \<A>(φ z) \<rightarrow> z = α)) in v]" shows"[(\<forall> z . (\<A>(φ z) \<equiv> (z = α))) in v]" proof -
{ fix z
{ assume"[\<A>(φ z) in v]" hence"[z = α in v]" using assms[conj2, THEN cqt_1[where α=z,
axiom_instance, deduction],
deduction] by auto
} moreover { assume"[z = α in v]" hence"[α = z in v]" unfolding identity_ν_def using id_eq_obj_2[deduction] by fast hence"[\<A>(φ z) in v]"using assms[conj1] using l_identity[axiom_instance, deduction,
deduction] by fast
} ultimatelyhave"[(\<A>(φ z) \<equiv> (z = α)) in v]" using"\<equiv>I" CP by auto
} thus"[(\<forall> z . (\<A>(φ z) \<equiv> (z = α))) in v]" by (rule "\<forall>I") qed
lemma nec_russell_axiom[PLM]: assumes"SimpleExOrEnc ψ" shows"[(ψ (\<iota>x. φ x)) \<equiv> (\<exists> x . (\<A>φ x & (\<forall> z . \<A>(φ z) \<rightarrow> z = x)) & ψ (xP)) in v]"
(is"[?lhs \<equiv> ?rhs in v]") proof -
{ assume1: "[?lhs in v]" hence"[\<exists>α. (αP) = (\<iota>x. φ x) in v]" using cqt_5[axiom_instance, deduction] assms by blast thenobtain α where2: "[(αP) = (\<iota>x. φ x) in v]"by (rule "\<exists>E") hence"[(\<forall> z . (\<A>(φ z) \<equiv> (z = α))) in v]" using descriptions[axiom_instance, equiv_lr] by auto hence3: "[(\<A>φ α) & (\<forall> z . (\<A>(φ z) \<rightarrow> (z = α))) in v]" using cqt_1[where α=α and φ="λ z . (\<A>(φ z) \<equiv> (z = α))",
axiom_instance, deduction, equiv_rl] using id_eq_obj_1[where x=α] unfolding identity_ν_def using hintikka[equiv_lr] cqt_basic_2[equiv_lr,conj1] "&I"by fast from2have"[(\<iota>x. φ x) = (αP) in v]" using l_identity[where β="(\<iota>x. φ x)"and φ="λ x . x = (αP)",
axiom_instance, deduction, deduction]
id_eq_obj_1[where x=α] by auto hence"[ψ (αP) in v]" using1 l_identity[where α="(\<iota>x. φ x)"and φ="λ x . ψ x",
axiom_instance, deduction,
deduction] by auto with3have"[(\<A>φ α & (\<forall> z . \<A>(φ z) \<rightarrow> (z = α))) & ψ (αP) in v]" using"&I"by simp hence"[?rhs in v]" using"\<exists>I"[where α=α] by (simp add: identity_defs)
} moreover { assume"[?rhs in v]" thenobtain α where4: "[(\<A>φ α & (\<forall> z . \<A>(φ z) \<rightarrow> z = α)) & ψ (αP) in v]" using"\<exists>E"by auto hence"[(\<forall> z . (\<A>(φ z) \<equiv> (z = α))) in v]" using UniqueAux "&E"(1) by auto hence"[(αP) = (\<iota>x . φ x) in v] ∧ [ψ (αP) in v]" using descriptions[axiom_instance, equiv_rl] 4[conj2] by blast hence"[?lhs in v]" using l_identity[axiom_instance, deduction,
deduction] by fast
} ultimatelyshow ?thesis by PLM_solver qed
lemma actual_desc_1[PLM]: "[(\<exists> y . (yP) = (\<iota>x. φ x)) \<equiv> (\<exists>! x . \<A>(φ x)) in v]" (is"[?lhs \<equiv> ?rhs in v]") proof -
{ assume"[?lhs in v]" thenobtain α where "[((αP) = (\<iota>x. φ x)) in v]" by (rule "\<exists>E") hence"[(A!,(\<iota>x. φ x)) in v] ∨ [(αP) =E (\<iota>x. φ x) in v]" apply - unfolding identity_defs by PLM_solver thenobtain x where "[((\<A>φ x & (\<forall> z . \<A>(φ z) \<rightarrow> z = x))) in v]" using nec_russell_axiom[where ψ="λx . (A!,x)", equiv_lr, THEN"\<exists>E"] using nec_russell_axiom[where ψ="λx . (αP) =E x", equiv_lr, THEN"\<exists>E"] using SimpleExOrEnc.introsunfolding identityE_infix_def by (meson "&E") hence"[?rhs in v]"unfolding exists_unique_def by (rule "\<exists>I")
} moreover { assume"[?rhs in v]" thenobtain x where "[((\<A>φ x & (\<forall> z . \<A>(φ z) \<rightarrow> z = x))) in v]" unfolding exists_unique_def by (rule "\<exists>E") hence"[\<forall>z. \<A>φ z \<equiv> z = x in v]" using UniqueAux by auto hence"[(xP) = (\<iota>x. φ x) in v]" using descriptions[axiom_instance, equiv_rl] by auto hence"[?lhs in v]"by (rule "\<exists>I")
} ultimatelyshow ?thesis using"\<equiv>I" CP by auto qed
lemma actual_desc_2[PLM]: "[(xP) = (\<iota>x. φ) \<rightarrow> \<A>φ in v]" using nec_hintikka_scheme[equiv_lr, conj1] by (rule CP)
lemma actual_desc_3[PLM]: "[(zP) = (\<iota>x. φ x) \<rightarrow> \<A>(φ z) in v]" using nec_hintikka_scheme[equiv_lr, conj1] by (rule CP)
lemma actual_desc_4[PLM]: "[(\<exists> y . ((yP) = (\<iota>x. φ (xP)))) \<rightarrow> \<A>(φ (\<iota>x. φ (xP))) in v]" proof (rule CP) assume"[(\<exists> y . (yP) = (\<iota>x . φ (xP))) in v]" thenobtain y where1: "[yP= (\<iota>x. φ (xP)) in v]" by (rule "\<exists>E") hence"[\<A>(φ (yP)) in v]"using actual_desc_3[deduction] by fast thus"[\<A>(φ (\<iota>x. φ (xP))) in v]" using l_identity[axiom_instance, deduction,
deduction] 1by fast qed
lemma unique_box_desc_1[PLM]: "[(\<exists>!x . \<box>(φ x)) \<rightarrow> (\<forall> y . (yP) = (\<iota>x. φ x) \<rightarrow> φ y) in v]" proof (rule CP) assume"[(\<exists>!x . \<box>(φ x)) in v]" thenobtain α where1: "[\<box>φ α & (\<forall>β. \<box>(φ β) \<rightarrow> β = α) in v]" unfolding exists_unique_def by (rule "\<exists>E")
{ fix y
{ assume"[(yP) = (\<iota>x. φ x) in v]" hence"[\<A>φ α \<rightarrow> α = y in v]" using nec_hintikka_scheme[where x="y"and φ="φ", equiv_lr, conj2, THEN cqt_1[where α=α,axiom_instance, deduction]] by simp hence"[α = y in v]" using1[conj1] nec_imp_act vdash_properties_10 by blast hence"[φ y in v]" using1[conj1] qml_2[axiom_instance, deduction]
l_identity[axiom_instance, deduction, deduction] by fast
} hence"[(yP) = (\<iota>x. φ x) \<rightarrow> φ y in v]" by (rule CP)
} thus"[\<forall> y . (yP) = (\<iota>x. φ x) \<rightarrow> φ y in v]" by (rule "\<forall>I") qed
lemma unique_box_desc[PLM]: "[(\<forall> x . (φ x \<rightarrow> \<box>(φ x))) \<rightarrow> ((\<exists>!x . φ x) \<rightarrow> (\<forall> y . (yP= (\<iota>x . φ x)) \<rightarrow> φ y)) in v]" apply (rule CP, rule CP) using nec_exist_unique[deduction, deduction]
unique_box_desc_1[deduction] by blast
lemma RM_1[PLM]: "(∧v.[φ \<rightarrow> ψ in v]) ==> [\<box>φ \<rightarrow> \<box>ψ in v]" using RN qml_1[axiom_instance] vdash_properties_10 by blast
lemma RM_1_b[PLM]: "(∧v.[χ in v] ==> [φ \<rightarrow> ψ in v]) ==> ([\<box>χ in v] ==> [\<box>φ \<rightarrow> \<box>ψ in v])" using RN_2 qml_1[axiom_instance] vdash_properties_10 by blast
lemma RM_2[PLM]: "(∧v.[φ \<rightarrow> ψ in v]) ==> [\<diamond>φ \<rightarrow> \<diamond>ψ in v]" unfolding diamond_def using RM_1 contraposition_1 by auto
lemma RM_2_b[PLM]: "(∧v.[χ in v] ==> [φ \<rightarrow> ψ in v]) ==> ([\<box>χ in v] ==> [\<diamond>φ \<rightarrow> \<diamond>ψ in v])" unfolding diamond_def using RM_1_b contraposition_1 by blast
lemma KBasic_1[PLM]: "[\<box>φ \<rightarrow> \<box>(ψ \<rightarrow> φ) in v]" by (simp only: pl_1[axiom_instance] RM_1) lemma KBasic_2[PLM]: "[\<box>(\<not>φ) \<rightarrow> \<box>(φ \<rightarrow> ψ) in v]" by (simp only: RM_1 useful_tautologies_3) lemma KBasic_3[PLM]: "[\<box>(φ & ψ) \<equiv> \<box>φ &\<box>ψ in v]" apply (rule "\<equiv>I") apply (rule CP) apply (rule "&I") using RM_1 oth_class_taut_9_a vdash_properties_6 apply blast using RM_1 oth_class_taut_9_b vdash_properties_6 apply blast using qml_1[axiom_instance] RM_1 ded_thm_cor_3 oth_class_taut_10_a
oth_class_taut_8_b vdash_properties_10 by blast lemma KBasic_4[PLM]: "[\<box>(φ \<equiv> ψ) \<equiv> (\<box>(φ \<rightarrow> ψ) &\<box>(ψ \<rightarrow> φ)) in v]" apply (rule "\<equiv>I") unfolding equiv_def using KBasic_3 PLM.CP "\<equiv>E"(1) apply blast using KBasic_3 PLM.CP "\<equiv>E"(2) by blast lemma KBasic_5[PLM]: "[(\<box>(φ \<rightarrow> ψ) &\<box>(ψ \<rightarrow> φ)) \<rightarrow> (\<box>φ \<equiv> \<box>ψ) in v]" by (metis qml_1[axiom_instance] CP "&E""\<equiv>I" vdash_properties_10) lemma KBasic_6[PLM]: "[\<box>(φ \<equiv> ψ) \<rightarrow> (\<box>φ \<equiv> \<box>ψ) in v]" using KBasic_4 KBasic_5 by (metis equiv_def ded_thm_cor_3 "&E"(1)) lemma"[(\<box>φ \<equiv> \<box>ψ) \<rightarrow> \<box>(φ \<equiv> ψ) in v]"
nitpick[expect=genuine, user_axioms, card = 1, card i = 2] oops―‹countermodel as desired› lemma KBasic_7[PLM]: "[(\<box>φ &\<box>ψ) \<rightarrow> \<box>(φ \<equiv> ψ) in v]" proof (rule CP) assume"[\<box>φ &\<box>ψ in v]" hence"[\<box>(ψ \<rightarrow> φ) in v] ∧ [\<box>(φ \<rightarrow> ψ) in v]" using"&E" KBasic_1 vdash_properties_10 by blast thus"[\<box>(φ \<equiv> ψ) in v]" using KBasic_4 "\<equiv>E"(2) intro_elim_1 by blast qed
lemma KBasic_8[PLM]: "[\<box>(φ & ψ) \<rightarrow> \<box>(φ \<equiv> ψ) in v]" using KBasic_7 KBasic_3 by (metis equiv_def PLM.ded_thm_cor_3 "&E"(1)) lemma KBasic_9[PLM]: "[\<box>((\<not>φ) & (\<not>ψ)) \<rightarrow> \<box>(φ \<equiv> ψ) in v]" proof (rule CP) assume"[\<box>((\<not>φ) & (\<not>ψ)) in v]" hence"[\<box>((\<not>φ) \<equiv> (\<not>ψ)) in v]" using KBasic_8 vdash_properties_10 by blast moreoverhave"∧v.[((\<not>φ) \<equiv> (\<not>ψ)) \<rightarrow> (φ \<equiv> ψ) in v]" using CP "\<equiv>E"(2) oth_class_taut_5_d by blast ultimatelyshow"[\<box>(φ \<equiv> ψ) in v]" using RM_1 PLM.vdash_properties_10 by blast qed
lemma rule_sub_lem_1_a[PLM]: "[\<box>(ψ \<equiv> χ) in v] ==> [(\<not>ψ) \<equiv> (\<not>χ) in v]" using qml_2[axiom_instance] "\<equiv>E"(1) oth_class_taut_5_d
vdash_properties_10 by blast lemma rule_sub_lem_1_b[PLM]: "[\<box>(ψ \<equiv> χ) in v] ==> [(ψ \<rightarrow> Θ) \<equiv> (χ \<rightarrow> Θ) in v]" by (metis equiv_def contraposition_1 CP "&E"(2) "\<equiv>I" "\<equiv>E"(1) rule_sub_lem_1_a) lemma rule_sub_lem_1_c[PLM]: "[\<box>(ψ \<equiv> χ) in v] ==> [(Θ \<rightarrow> ψ) \<equiv> (Θ \<rightarrow> χ) in v]" by (metis CP "\<equiv>I""\<equiv>E"(3) "\<equiv>E"(4) "\<not>\<not>I" "\<not>\<not>E" rule_sub_lem_1_a) lemma rule_sub_lem_1_d[PLM]: "(∧x.[\<box>(ψ x \<equiv> χ x) in v]) ==> [(\<forall>α. ψ α) \<equiv> (\<forall>α. χ α) in v]" by (metis equiv_def "\<forall>I" CP "&E""\<equiv>I" raa_cor_1
vdash_properties_10 rule_sub_lem_1_a "\<forall>E") lemma rule_sub_lem_1_e[PLM]: "[\<box>(ψ \<equiv> χ) in v] ==> [\<A>ψ \<equiv> \<A>χ in v]" using Act_Basic_5 "\<equiv>E"(1) nec_imp_act
vdash_properties_10 by blast lemma rule_sub_lem_1_f[PLM]: "[\<box>(ψ \<equiv> χ) in v] ==> [\<box>ψ \<equiv> \<box>χ in v]" using KBasic_6 "\<equiv>I""\<equiv>E"(1) vdash_properties_9 by blast
method PLM_subst_method for ψ::"'a::Substable"and χ::"'a::Substable" =
(match conclusion in"Θ [φ χ in v]"for Θ and φ and v → ‹(rule rule_sub_nec[where Θ=Θ and χ=χ and ψ=ψ and φ=φ and v=v],
((fast intro: Substable_intros, ((assumption)+)?)+; fail),
unfold Substable_Cond_defs)›)
method PLM_autosubst =
(match premises in"∧v . [ψ \<equiv> χ in v]"for ψ and χ → ‹ match conclusion in "Θ [φ χ in v]" for Θ φ and v → ‹(rule rule_sub_nec[where Θ=Θ and χ=χ and ψ=ψ and φ=φ and v=v],
((fast intro: Substable_intros, ((assumption)+)?)+; fail),
unfold Substable_Cond_defs)››)
method PLM_autosubst1 =
(match premises in"∧v x . [ψ x \<equiv> χ x in v]" for ψ::"'a::type→o"and χ::"'a→o"→ ‹ match conclusion in "Θ [φ χ in v]" for Θ φ and v → ‹(rule rule_sub_nec[where Θ=Θ and χ=χ and ψ=ψ and φ=φ and v=v],
((fast intro: Substable_intros, ((assumption)+)?)+; fail),
unfold Substable_Cond_defs)››)
method PLM_autosubst2 =
(match premises in"∧v x y . [ψ x y \<equiv> χ x y in v]" for ψ::"'a::type→'a→o"and χ::"'a::type→'a→o"→ ‹ match conclusion in "Θ [φ χ in v]" for Θ φ and v → ‹(rule rule_sub_nec[where Θ=Θ and χ=χ and ψ=ψ and φ=φ and v=v],
((fast intro: Substable_intros, ((assumption)+)?)+; fail),
unfold Substable_Cond_defs)››)
method PLM_subst_goal_method for φ::"'a::Substable→o"and ψ::"'a" =
(match conclusion in"Θ [φ χ in v]"for Θ and χ and v → ‹(rule rule_sub_nec[where Θ=Θ and χ=χ and ψ=ψ and φ=φ and v=v],
((fast intro: Substable_intros, ((assumption)+)?)+; fail),
unfold Substable_Cond_defs)›)
lemma rule_sub_nec[PLM]: assumes"Substable Substable_Cond φ" shows"(∧v.[(ψ \<equiv> χ) in v]) ==> Θ [φ ψ in v] ==> Θ [φ χ in v]" proof - assume"(∧v.[(ψ \<equiv> χ) in v])" hence"[φ ψ in v] = [φ χ in v]" using assms RN unfolding Substable_def Substable_Cond_defs using"\<equiv>I" CP "\<equiv>E"(1) "\<equiv>E"(2) by meson thus"Θ [φ ψ in v] ==> Θ [φ χ in v]"by auto qed
lemma rule_sub_nec1[PLM]: assumes"Substable Substable_Cond φ" shows"(∧v x .[(ψ x \<equiv> χ x) in v]) ==> Θ [φ ψ in v] ==> Θ [φ χ in v]" proof - assume"(∧v x.[(ψ x \<equiv> χ x) in v])" hence"[φ ψ in v] = [φ χ in v]" using assms RN unfolding Substable_def Substable_Cond_defs using"\<equiv>I" CP "\<equiv>E"(1) "\<equiv>E"(2) by metis thus"Θ [φ ψ in v] ==> Θ [φ χ in v]"by auto qed
lemma rule_sub_nec2[PLM]: assumes"Substable Substable_Cond φ" shows"(∧v x y .[ψ x y \<equiv> χ x y in v]) ==> Θ [φ ψ in v] ==> Θ [φ χ in v]" proof - assume"(∧v x y .[ψ x y \<equiv> χ x y in v])" hence"[φ ψ in v] = [φ χ in v]" using assms RN unfolding Substable_def Substable_Cond_defs using"\<equiv>I" CP "\<equiv>E"(1) "\<equiv>E"(2) by metis thus"Θ [φ ψ in v] ==> Θ [φ χ in v]"by auto qed
lemma rule_sub_remark_1_autosubst: assumes"(∧v.[(A!,x)\<equiv> (\<not>(\<diamond>(E!,x))) in v])" and"[\<not>(A!,x) in v]" shows"[\<not>\<not>\<diamond>(E!,x) in v]" apply (insert assms) apply PLM_autosubst by auto
lemma rule_sub_remark_1: assumes"(∧v.[(A!,x)\<equiv> (\<not>(\<diamond>(E!,x))) in v])" and"[\<not>(A!,x) in v]" shows"[\<not>\<not>\<diamond>(E!,x) in v]" apply (PLM_subst_method "(A!,x)""(\<not>(\<diamond>(E!,x)))") apply (simp add: assms(1)) by (simp add: assms(2))
lemma rule_sub_remark_2: assumes"(∧v.[(R,x,y)\<equiv> ((R,x,y)& ((Q,a)\<or> (\<not>(Q,a)))) in v])" and"[p \<rightarrow> (R,x,y) in v]" shows"[p \<rightarrow> ((R,x,y)& ((Q,a)\<or> (\<not>(Q,a)))) in v]" apply (insert assms) apply PLM_autosubst by auto
lemma rule_sub_remark_3_autosubst: assumes"(∧v x.[(A!,xP)\<equiv> (\<not>(\<diamond>(E!,xP))) in v])" and"[\<exists> x . (A!,xP) in v]" shows"[\<exists> x . (\<not>(\<diamond>(E!,xP))) in v]" apply (insert assms) apply PLM_autosubst1 by auto
lemma rule_sub_remark_3: assumes"(∧v x.[(A!,xP)\<equiv> (\<not>(\<diamond>(E!,xP))) in v])" and"[\<exists> x . (A!,xP) in v]" shows"[\<exists> x . (\<not>(\<diamond>(E!,xP))) in v]" apply (PLM_subst_method "λx . (A!,xP)""λx . (\<not>(\<diamond>(E!,xP)))") apply (simp add: assms(1)) by (simp add: assms(2))
lemma rule_sub_remark_4: assumes"∧v x.[(\<not>(\<not>(P,xP))) \<equiv> (P,xP) in v]" and"[\<A>(\<not>(\<not>(P,xP))) in v]" shows"[\<A>(P,xP) in v]" apply (insert assms) apply PLM_autosubst1 by auto
lemma rule_sub_remark_5: assumes"∧v.[(φ \<rightarrow> ψ) \<equiv> ((\<not>ψ) \<rightarrow> (\<not>φ)) in v]" and"[\<box>(φ \<rightarrow> ψ) in v]" shows"[\<box>((\<not>ψ) \<rightarrow> (\<not>φ)) in v]" apply (insert assms) apply PLM_autosubst by auto
lemma rule_sub_remark_6: assumes"∧v.[ψ \<equiv> χ in v]" and"[\<box>(φ \<rightarrow> ψ) in v]" shows"[\<box>(φ \<rightarrow> χ) in v]" apply (insert assms) apply PLM_autosubst by auto
lemma rule_sub_remark_7: assumes"∧v.[φ \<equiv> (\<not>(\<not>φ)) in v]" and"[\<box>(φ \<rightarrow> φ) in v]" shows"[\<box>((\<not>(\<not>φ)) \<rightarrow> φ) in v]" apply (insert assms) apply PLM_autosubst by auto
lemma rule_sub_remark_8: assumes"∧v.[\<A>φ \<equiv> φ in v]" and"[\<box>(\<A>φ) in v]" shows"[\<box>(φ) in v]" apply (insert assms) apply PLM_autosubst by auto
lemma rule_sub_remark_9: assumes"∧v.[(P,a)\<equiv> ((P,a)& ((Q,b)\<or> (\<not>(Q,b)))) in v]" and"[(P,a)=(P,a) in v]" shows"[(P,a)= ((P,a)& ((Q,b)\<or> (\<not>(Q,b)))) in v]" unfolding identity_defs apply (insert assms) apply PLM_autosubst oops―‹no match as desired›
lemma KBasic2_4[PLM]: "[\<box>(\<not>(φ)) \<equiv> (\<not>(\<diamond>φ)) in v]" unfolding diamond_def by (simp add: oth_class_taut_4_b)
lemma KBasic2_5[PLM]: "[\<box>(φ \<rightarrow> ψ) \<rightarrow> (\<diamond>φ \<rightarrow> \<diamond>ψ) in v]" by (simp only: CP RM_2_b) lemmas"K\<diamond>" = KBasic2_5
lemma KBasic2_6[PLM]: "[\<diamond>(φ \<or> ψ) \<equiv> (\<diamond>φ \<or> \<diamond>ψ) in v]" proof - have"[\<box>((\<not>φ) & (\<not>ψ)) \<equiv> (\<box>(\<not>φ) &\<box>(\<not>ψ)) in v]" using KBasic_3 by blast hence"[(\<not>(\<diamond>(\<not>((\<not>φ) & (\<not>ψ))))) \<equiv> (\<box>(\<not>φ) &\<box>(\<not>ψ)) in v]" using"Df\<box>"by (rule "\<equiv>E"(6)) hence"[(\<not>(\<diamond>(\<not>((\<not>φ) & (\<not>ψ))))) \<equiv> ((\<not>(\<diamond>φ)) & (\<not>(\<diamond>ψ))) in v]" apply - apply (PLM_subst_method "\<box>(\<not>φ)""\<not>(\<diamond>φ)") apply (simp add: KBasic2_4) apply (PLM_subst_method "\<box>(\<not>ψ)""\<not>(\<diamond>ψ)") apply (simp add: KBasic2_4) unfolding diamond_def by assumption hence"[(\<not>(\<diamond>(φ \<or> ψ))) \<equiv> ((\<not>(\<diamond>φ)) & (\<not>(\<diamond>ψ))) in v]" apply - apply (PLM_subst_method "\<not>((\<not>φ) & (\<not>ψ))""φ \<or> ψ") using oth_class_taut_6_b[equiv_sym] by auto hence"[(\<not>(\<not>(\<diamond>(φ \<or> ψ)))) \<equiv> (\<not>((\<not>(\<diamond>φ))&(\<not>(\<diamond>ψ)))) in v]" by (rule oth_class_taut_5_d[equiv_lr]) hence"[\<diamond>(φ \<or> ψ) \<equiv> (\<not>((\<not>(\<diamond>φ)) & (\<not>(\<diamond>ψ)))) in v]" apply - apply (PLM_subst_method "\<not>(\<not>(\<diamond>(φ \<or> ψ)))""\<diamond>(φ \<or> ψ)") using oth_class_taut_4_b[equiv_sym] by auto thus ?thesis apply - apply (PLM_subst_method "\<not>((\<not>(\<diamond>φ)) & (\<not>(\<diamond>ψ)))""(\<diamond>φ) \<or> (\<diamond>ψ)") using oth_class_taut_6_b[equiv_sym] by auto qed
lemma KBasic2_7[PLM]: "[(\<box>φ \<or> \<box>ψ) \<rightarrow> \<box>(φ \<or> ψ) in v]" proof - have"∧ v . [φ \<rightarrow> (φ \<or> ψ) in v]" by (metis contraposition_1 contraposition_2 useful_tautologies_3 disj_def) hence"[\<box>φ \<rightarrow> \<box>(φ \<or> ψ) in v]"using RM_1 by auto moreover { have"∧ v . [ψ \<rightarrow> (φ \<or> ψ) in v]" by (simp only: pl_1[axiom_instance] disj_def) hence"[\<box>ψ \<rightarrow> \<box>(φ \<or> ψ) in v]" using RM_1 by auto
} ultimatelyshow ?thesis using oth_class_taut_10_d vdash_properties_10 by blast qed
lemma KBasic2_8[PLM]: "[\<diamond>(φ & ψ) \<rightarrow> (\<diamond>φ &\<diamond>ψ) in v]" by (metis CP RM_2 "&I" oth_class_taut_9_a
oth_class_taut_9_b vdash_properties_10)
lemma KBasic2_9[PLM]: "[\<diamond>(φ \<rightarrow> ψ) \<equiv> (\<box>φ \<rightarrow> \<diamond>ψ) in v]" apply (PLM_subst_method "(\<not>(\<box>φ)) \<or> (\<diamond>ψ)""\<box>φ \<rightarrow> \<diamond>ψ") using oth_class_taut_5_k[equiv_sym] apply simp apply (PLM_subst_method "(\<not>φ) \<or> ψ""φ \<rightarrow> ψ") using oth_class_taut_5_k[equiv_sym] apply simp apply (PLM_subst_method "\<diamond>(\<not>φ)""\<not>(\<box>φ)") using KBasic2_2[equiv_sym] apply simp using KBasic2_6 .
lemma KBasic2_10[PLM]: "[\<diamond>(\<box>φ) \<equiv> (\<not>(\<box>\<diamond>(\<not>φ))) in v]" unfolding diamond_def apply (PLM_subst_method "φ""\<not>\<not>φ") using oth_class_taut_4_b oth_class_taut_4_a by auto
lemma KBasic2_11[PLM]: "[\<diamond>\<diamond>φ \<equiv> (\<not>(\<box>\<box>(\<not>φ))) in v]" unfolding diamond_def apply (PLM_subst_method "\<box>(\<not>φ)""\<not>(\<not>(\<box>(\<not>φ)))") using oth_class_taut_4_b oth_class_taut_4_a by auto
lemma KBasic2_12[PLM]: "[\<box>(φ \<or> ψ) \<rightarrow> (\<box>φ \<or> \<diamond>ψ) in v]" proof - have"[\<box>(ψ \<or> φ) \<rightarrow> (\<box>(\<not>ψ) \<rightarrow> \<box>φ) in v]" using CP RM_1_b "\<or>E"(2) by blast hence"[\<box>(ψ \<or> φ) \<rightarrow> (\<diamond>ψ \<or> \<box>φ) in v]" unfolding diamond_def disj_def by (meson CP "\<not>\<not>E" vdash_properties_6) thus ?thesis apply - apply (PLM_subst_method "(\<diamond>ψ \<or> \<box>φ)""(\<box>φ \<or> \<diamond>ψ)") apply (simp add: PLM.oth_class_taut_3_e) apply (PLM_subst_method "(ψ \<or> φ)""(φ \<or> ψ)") apply (simp add: PLM.oth_class_taut_3_e) by assumption qed
lemma TBasic[PLM]: "[φ \<rightarrow> \<diamond>φ in v]" unfolding diamond_def apply (subst contraposition_1) apply (PLM_subst_method "\<box>\<not>φ""\<not>\<not>\<box>\<not>φ") apply (simp add: PLM.oth_class_taut_4_b) using qml_2[where φ="\<not>φ", axiom_instance] by simp lemmas"T\<diamond>" = TBasic
lemma S5Basic_1[PLM]: "[\<diamond>\<box>φ \<rightarrow> \<box>φ in v]" proof (rule CP) assume"[\<diamond>\<box>φ in v]" hence"[\<not>\<box>\<diamond>\<not>φ in v]" using KBasic2_10[equiv_lr] by simp moreoverhave"[\<diamond>(\<not>φ) \<rightarrow> \<box>\<diamond>(\<not>φ) in v]" by (simp add: qml_3[axiom_instance]) ultimatelyhave"[\<not>\<diamond>\<not>φ in v]" by (simp add: PLM.modus_tollens_1) thus"[\<box>φ in v]" unfolding diamond_def apply - apply (PLM_subst_method "\<not>\<not>φ""φ") using oth_class_taut_4_b[equiv_sym] apply simp unfolding diamond_def using oth_class_taut_4_b[equiv_rl] by simp qed lemmas"5\<diamond>" = S5Basic_1
lemma S5Basic_2[PLM]: "[\<box>φ \<equiv> \<diamond>\<box>φ in v]" using"5\<diamond>""T\<diamond>""\<equiv>I"by blast
lemma S5Basic_3[PLM]: "[\<diamond>φ \<equiv> \<box>\<diamond>φ in v]" using qml_3[axiom_instance] qml_2[axiom_instance] "\<equiv>I"by blast
lemma S5Basic_4[PLM]: "[φ \<rightarrow> \<box>\<diamond>φ in v]" using"T\<diamond>"[deduction, THEN S5Basic_3[equiv_lr]] by (rule CP)
lemma S5Basic_5[PLM]: "[\<diamond>\<box>φ \<rightarrow> φ in v]" using S5Basic_2[equiv_rl, THEN qml_2[axiom_instance, deduction]] by (rule CP) lemmas"B\<diamond>" = S5Basic_5
lemma S5Basic_6[PLM]: "[\<box>φ \<rightarrow> \<box>\<box>φ in v]" using S5Basic_4[deduction] RM_1[OF S5Basic_1, deduction] CP by auto lemmas"4\<box>" = S5Basic_6
lemma S5Basic_7[PLM]: "[\<box>φ \<equiv> \<box>\<box>φ in v]" using"4\<box>" qml_2[axiom_instance] by (rule "\<equiv>I")
lemma S5Basic_8[PLM]: "[\<diamond>\<diamond>φ \<rightarrow> \<diamond>φ in v]" using S5Basic_6[where φ="\<not>φ", THEN contraposition_1[THEN iffD1], deduction]
KBasic2_11[equiv_lr] CP unfolding diamond_def by auto lemmas"4\<diamond>" = S5Basic_8
lemma S5Basic_9[PLM]: "[\<diamond>\<diamond>φ \<equiv> \<diamond>φ in v]" using"4\<diamond>""T\<diamond>"by (rule "\<equiv>I")
lemma S5Basic_10[PLM]: "[\<box>(φ \<or> \<box>ψ) \<equiv> (\<box>φ \<or> \<box>ψ) in v]" apply (rule "\<equiv>I") apply (PLM_subst_goal_method "λ χ . \<box>(φ \<or> \<box>ψ) \<rightarrow> (\<box>φ \<or> χ)""\<diamond>\<box>ψ") using S5Basic_2[equiv_sym] apply simp using KBasic2_12 apply assumption apply (PLM_subst_goal_method "λ χ .(\<box>φ \<or> χ) \<rightarrow> \<box>(φ \<or> \<box>ψ)""\<box>\<box>ψ") using S5Basic_7[equiv_sym] apply simp using KBasic2_7 by auto
lemma S5Basic_11[PLM]: "[\<box>(φ \<or> \<diamond>ψ) \<equiv> (\<box>φ \<or> \<diamond>ψ) in v]" apply (rule "\<equiv>I") apply (PLM_subst_goal_method "λ χ . \<box>(φ \<or> \<diamond>ψ) \<rightarrow> (\<box>φ \<or> χ)""\<diamond>\<diamond>ψ") using S5Basic_9 apply simp using KBasic2_12 apply assumption apply (PLM_subst_goal_method "λ χ .(\<box>φ \<or> χ) \<rightarrow> \<box>(φ \<or> \<diamond>ψ)""\<box>\<diamond>ψ") using S5Basic_3[equiv_sym] apply simp using KBasic2_7 by assumption
lemma S5Basic_12[PLM]: "[\<diamond>(φ &\<diamond>ψ) \<equiv> (\<diamond>φ &\<diamond>ψ) in v]" proof - have"[\<box>((\<not>φ) \<or> \<box>(\<not>ψ)) \<equiv> (\<box>(\<not>φ) \<or> \<box>(\<not>ψ)) in v]" using S5Basic_10 by auto hence1: "[(\<not>\<box>((\<not>φ) \<or> \<box>(\<not>ψ))) \<equiv> \<not>(\<box>(\<not>φ) \<or>\<box>(\<not>ψ)) in v]" using oth_class_taut_5_d[equiv_lr] by auto have2: "[(\<diamond>(\<not>((\<not>φ) \<or> (\<not>(\<diamond>ψ))))) \<equiv> (\<not>((\<not>(\<diamond>φ)) \<or> (\<not>(\<diamond>ψ)))) in v]" apply (PLM_subst_method "\<box>\<not>ψ""\<not>\<diamond>ψ") using KBasic2_4 apply simp apply (PLM_subst_method "\<box>\<not>φ""\<not>\<diamond>φ") using KBasic2_4 apply simp apply (PLM_subst_method "(\<not>\<box>((\<not>φ) \<or> \<box>(\<not>ψ)))""(\<diamond>(\<not>((\<not>φ) \<or> (\<box>(\<not>ψ)))))") unfolding diamond_def apply (simp add: RN oth_class_taut_4_b rule_sub_lem_1_a rule_sub_lem_1_f) using1by assumption show ?thesis apply (PLM_subst_method "\<not>((\<not>φ) \<or> (\<not>\<diamond>ψ))""φ &\<diamond>ψ") using oth_class_taut_6_a[equiv_sym] apply simp apply (PLM_subst_method "\<not>((\<not>(\<diamond>φ)) \<or> (\<not>\<diamond>ψ))""\<diamond>φ &\<diamond>ψ") using oth_class_taut_6_a[equiv_sym] apply simp using2by assumption qed
lemma S5Basic_13[PLM]: "[\<diamond>(φ & (\<box>ψ)) \<equiv> (\<diamond>φ & (\<box>ψ)) in v]" apply (PLM_subst_method "\<diamond>\<box>ψ""\<box>ψ") using S5Basic_2[equiv_sym] apply simp using S5Basic_12 by simp
lemma S5Basic_14[PLM]: "[\<box>(φ \<rightarrow> (\<box>ψ)) \<equiv> \<box>(\<diamond>φ \<rightarrow> ψ) in v]" proof (rule "\<equiv>I"; rule CP) assume"[\<box>(φ \<rightarrow> \<box>ψ) in v]" moreover { have"∧v.[\<box>(φ \<rightarrow> \<box>ψ) \<rightarrow> (\<diamond>φ \<rightarrow> ψ) in v]" proof (rule CP) fix v assume"[\<box>(φ \<rightarrow> \<box>ψ) in v]" hence"[\<diamond>φ \<rightarrow> \<diamond>\<box>ψ in v]" using"K\<diamond>"[deduction] by auto thus"[\<diamond>φ \<rightarrow> ψ in v]" using"B\<diamond>" ded_thm_cor_3 by blast qed hence"[\<box>(\<box>(φ \<rightarrow> \<box>ψ) \<rightarrow> (\<diamond>φ \<rightarrow> ψ)) in v]" by (rule RN) hence"[\<box>(\<box>(φ \<rightarrow> \<box>ψ)) \<rightarrow> \<box>((\<diamond>φ \<rightarrow> ψ)) in v]" using qml_1[axiom_instance, deduction] by auto
} ultimatelyshow"[\<box>(\<diamond>φ \<rightarrow> ψ) in v]" using S5Basic_6 CP vdash_properties_10 by meson next assume"[\<box>(\<diamond>φ \<rightarrow> ψ) in v]" moreover { fix v
{ assume"[\<box>(\<diamond>φ \<rightarrow> ψ) in v]" hence1: "[\<box>\<diamond>φ \<rightarrow> \<box>ψ in v]" using qml_1[axiom_instance, deduction] by auto assume"[φ in v]" hence"[\<box>\<diamond>φ in v]" using S5Basic_4[deduction] by auto hence"[\<box>ψ in v]" using1[deduction] by auto
} hence"[\<box>(\<diamond>φ \<rightarrow> ψ) in v] ==> [φ \<rightarrow> \<box>ψ in v]" using CP by auto
} ultimatelyshow"[\<box>(φ \<rightarrow> \<box>ψ) in v]" using S5Basic_6 RN_2 vdash_properties_10 by blast qed
lemma sc_eq_box_box_1[PLM]: "[\<box>(φ \<rightarrow> \<box>φ) \<rightarrow> (\<diamond>φ \<equiv> \<box>φ) in v]" proof(rule CP) assume1: "[\<box>(φ \<rightarrow> \<box>φ) in v]" hence"[\<box>(\<diamond>φ \<rightarrow> φ) in v]" using S5Basic_14[equiv_lr] by auto hence"[\<diamond>φ \<rightarrow> φ in v]" using qml_2[axiom_instance, deduction] by auto moreoverfrom1have"[φ \<rightarrow> \<box>φ in v]" using qml_2[axiom_instance, deduction] by auto ultimatelyhave"[\<diamond>φ \<rightarrow> \<box>φ in v]" using ded_thm_cor_3 by blast moreoverhave"[\<box>φ \<rightarrow> \<diamond>φ in v]" using qml_2[axiom_instance] "T\<diamond>" by (rule ded_thm_cor_3) ultimatelyshow"[\<diamond>φ \<equiv> \<box>φ in v]" by (rule "\<equiv>I") qed
lemma sc_eq_box_box_2[PLM]: "[\<box>(φ \<rightarrow> \<box>φ) \<rightarrow> ((\<not>\<box>φ) \<equiv> (\<box>(\<not>φ))) in v]" proof (rule CP) assume"[\<box>(φ \<rightarrow> \<box>φ) in v]" hence"[(\<not>\<box>(\<not>φ)) \<equiv> \<box>φ in v]" using sc_eq_box_box_1[deduction] unfolding diamond_def by auto thus"[((\<not>\<box>φ) \<equiv> (\<box>(\<not>φ))) in v]" by (meson CP "\<equiv>I""\<equiv>E"(3) "\<equiv>E"(4) "\<not>\<not>I""\<not>\<not>E") qed
lemma sc_eq_box_box_3[PLM]: "[(\<box>(φ \<rightarrow> \<box>φ) &\<box>(ψ \<rightarrow> \<box>ψ)) \<rightarrow> ((\<box>φ \<equiv> \<box>ψ) \<rightarrow> \<box>(φ \<equiv> ψ)) in v]" proof (rule CP) assume1: "[(\<box>(φ \<rightarrow> \<box>φ) &\<box>(ψ \<rightarrow> \<box>ψ)) in v]"
{ assume"[\<box>φ \<equiv> \<box>ψ in v]" hence"[(\<box>φ &\<box>ψ) \<or> ((\<not>(\<box>φ)) & (\<not>(\<box>ψ))) in v]" using oth_class_taut_5_i[equiv_lr] by auto moreover { assume"[\<box>φ &\<box>ψ in v]" hence"[\<box>(φ \<equiv> ψ) in v]" using KBasic_7[deduction] by auto
} moreover { assume"[(\<not>(\<box>φ)) & (\<not>(\<box>ψ)) in v]" hence"[\<box>(\<not>φ) &\<box>(\<not>ψ) in v]" using1"&E""&I" sc_eq_box_box_2[deduction, equiv_lr] by metis hence"[\<box>((\<not>φ) & (\<not>ψ)) in v]" using KBasic_3[equiv_rl] by auto hence"[\<box>(φ \<equiv> ψ) in v]" using KBasic_9[deduction] by auto
} ultimatelyhave"[\<box>(φ \<equiv> ψ) in v]" using CP "\<or>E"(1) by blast
} thus"[\<box>φ \<equiv> \<box>ψ \<rightarrow> \<box>(φ \<equiv> ψ) in v]" using CP by auto qed
lemma derived_S5_rules_1_a[PLM]: assumes"∧v. [χ in v] ==> [\<diamond>φ \<rightarrow> ψ in v]" shows"[\<box>χ in v] ==> [φ \<rightarrow> \<box>ψ in v]" proof - have"[\<box>χ in v] ==> [\<box>\<diamond>φ \<rightarrow> \<box>ψ in v]" using assms RM_1_b by metis thus"[\<box>χ in v] ==> [φ \<rightarrow> \<box>ψ in v]" using S5Basic_4 vdash_properties_10 CP by metis qed
lemma derived_S5_rules_1_b[PLM]: assumes"∧v. [\<diamond>φ \<rightarrow> ψ in v]" shows"[φ \<rightarrow> \<box>ψ in v]" using derived_S5_rules_1_a all_self_eq_1 assms by blast
lemma derived_S5_rules_2_a[PLM]: assumes"∧v. [χ in v] ==> [φ \<rightarrow> \<box>ψ in v]" shows"[\<box>χ in v] ==> [\<diamond>φ \<rightarrow> ψ in v]" proof - have"[\<box>χ in v] ==> [\<diamond>φ \<rightarrow> \<diamond>\<box>ψ in v]" using RM_2_b assms by metis thus"[\<box>χ in v] ==> [\<diamond>φ \<rightarrow> ψ in v]" using"B\<diamond>" vdash_properties_10 CP by metis qed
lemma derived_S5_rules_2_b[PLM]: assumes"∧v. [φ \<rightarrow> \<box>ψ in v]" shows"[\<diamond>φ \<rightarrow> ψ in v]" using assms derived_S5_rules_2_a all_self_eq_1 by blast
lemma BFs_1[PLM]: "[(\<forall>α. \<box>(φ α)) \<rightarrow> \<box>(\<forall>α. φ α) in v]" proof (rule derived_S5_rules_1_b) fix v
{ fix α have"∧v.[(\<forall>α . \<box>(φ α)) \<rightarrow> \<box>(φ α) in v]" using cqt_orig_1 by metis hence"[\<diamond>(\<forall>α. \<box>(φ α)) \<rightarrow> \<diamond>\<box>(φ α) in v]" using RM_2 by metis moreoverhave"[\<diamond>\<box>(φ α) \<rightarrow> (φ α) in v]" using"B\<diamond>"by auto ultimatelyhave"[\<diamond>(\<forall>α. \<box>(φ α)) \<rightarrow> (φ α) in v]" using ded_thm_cor_3 by blast
} hence"[\<forall> α . \<diamond>(\<forall>α. \<box>(φ α)) \<rightarrow> (φ α) in v]" using"\<forall>I"by metis thus"[\<diamond>(\<forall>α. \<box>(φ α)) \<rightarrow> (\<forall>α. φ α) in v]" using cqt_orig_2[deduction] by auto qed lemmas BF = BFs_1
lemma BFs_2[PLM]: "[\<box>(\<forall>α. φ α) \<rightarrow> (\<forall>α. \<box>(φ α)) in v]" proof -
{ fix α
{ fix v have"[(\<forall>α. φ α) \<rightarrow> φ α in v]"using cqt_orig_1 by metis
} hence"[\<box>(\<forall>α . φ α) \<rightarrow> \<box>(φ α) in v]"using RM_1 by auto
} hence"[\<forall>α . \<box>(\<forall>α . φ α) \<rightarrow> \<box>(φ α) in v]"using"\<forall>I"by metis thus ?thesis using cqt_orig_2[deduction] by metis qed lemmas CBF = BFs_2
lemma BFs_3[PLM]: "[\<diamond>(\<exists> α. φ α) \<rightarrow> (\<exists> α . \<diamond>(φ α)) in v]" proof - have"[(\<forall>α. \<box>(\<not>(φ α))) \<rightarrow> \<box>(\<forall>α. \<not>(φ α)) in v]" using BF by metis hence1: "[(\<not>(\<box>(\<forall>α. \<not>(φ α)))) \<rightarrow> (\<not>(\<forall>α. \<box>(\<not>(φ α)))) in v]" using contraposition_1 by simp have2: "[\<diamond>(\<not>(\<forall>α. \<not>(φ α))) \<rightarrow> (\<not>(\<forall>α. \<box>(\<not>(φ α)))) in v]" apply (PLM_subst_method "\<not>\<box>(\<forall>α . \<not>(φ α))""\<diamond>(\<not>(\<forall>α. \<not>(φ α)))") using KBasic2_2 1by simp+ have"[\<diamond>(\<not>(\<forall>α. \<not>(φ α))) \<rightarrow> (\<exists> α . \<not>(\<box>(\<not>(φ α)))) in v]" apply (PLM_subst_method "\<not>(\<forall>α. \<box>(\<not>(φ α)))""\<exists> α. \<not>(\<box>(\<not>(φ α)))") using cqt_further_2 apply metis using2by metis thus ?thesis unfolding exists_def diamond_def by auto qed lemmas"BF\<diamond>" = BFs_3
lemma BFs_4[PLM]: "[(\<exists> α . \<diamond>(φ α)) \<rightarrow> \<diamond>(\<exists> α. φ α) in v]" proof - have1: "[\<box>(\<forall>α . \<not>(φ α)) \<rightarrow> (\<forall>α. \<box>(\<not>(φ α))) in v]" using CBF by auto have2: "[(\<exists> α . (\<not>(\<box>(\<not>(φ α))))) \<rightarrow> (\<not>(\<box>(\<forall>α. \<not>(φ α)))) in v]" apply (PLM_subst_method "\<not>(\<forall>α. \<box>(\<not>(φ α)))""(\<exists> α . (\<not>(\<box>(\<not>(φ α)))))") using cqt_further_2 apply blast using1using contraposition_1 by metis have"[(\<exists> α . (\<not>(\<box>(\<not>(φ α))))) \<rightarrow> \<diamond>(\<not>(\<forall> α . \<not>(φ α))) in v]" apply (PLM_subst_method "\<not>(\<box>(\<forall>α. \<not>(φ α)))""\<diamond>(\<not>(\<forall>α. \<not>(φ α)))") using KBasic2_2 apply blast using2by assumption thus ?thesis unfolding diamond_def exists_def by auto qed lemmas"CBF\<diamond>" = BFs_4
lemma sign_S5_thm_1[PLM]: "[(\<exists> α. \<box>(φ α)) \<rightarrow> \<box>(\<exists> α. φ α) in v]" proof (rule CP) assume"[\<exists> α . \<box>(φ α) in v]" thenobtain τ where"[\<box>(φ τ) in v]" by (rule "\<exists>E") moreover { fix v assume"[φ τ in v]" hence"[\<exists> α . φ α in v]" by (rule "\<exists>I")
} ultimatelyshow"[\<box>(\<exists> α . φ α) in v]" using RN_2 by blast qed lemmas Buridan = sign_S5_thm_1
lemma sign_S5_thm_2[PLM]: "[\<diamond>(\<forall> α . φ α) \<rightarrow> (\<forall> α . \<diamond>(φ α)) in v]" proof -
{ fix α
{ fix v have"[(\<forall> α . φ α) \<rightarrow> φ α in v]" using cqt_orig_1 by metis
} hence"[\<diamond>(\<forall> α . φ α) \<rightarrow> \<diamond>(φ α) in v]" using RM_2 by metis
} hence"[\<forall> α . \<diamond>(\<forall> α . φ α) \<rightarrow> \<diamond>(φ α) in v]" using"\<forall>I"by metis thus ?thesis using cqt_orig_2[deduction] by metis qed lemmas"Buridan\<diamond>" = sign_S5_thm_2
lemma sign_S5_thm_4[PLM]: "[((\<box>(\<forall> α. φ α \<rightarrow> ψ α)) & (\<box>(\<forall> α . ψ α \<rightarrow> χ α))) \<rightarrow> \<box>(\<forall>α. φ α \<rightarrow> χ α) in v]" proof (rule CP) assume"[\<box>(\<forall>α. φ α \<rightarrow> ψ α) &\<box>(\<forall>α. ψ α \<rightarrow> χ α) in v]" hence"[\<box>((\<forall>α. φ α \<rightarrow> ψ α) & (\<forall>α. ψ α \<rightarrow> χ α)) in v]" using KBasic_3[equiv_rl] by blast moreover { fix v assume"[((\<forall>α. φ α \<rightarrow> ψ α) & (\<forall>α. ψ α \<rightarrow> χ α)) in v]" hence"[(\<forall> α . φ α \<rightarrow> χ α) in v]" using cqt_basic_9[deduction] by blast
} ultimatelyshow"[\<box>(\<forall>α. φ α \<rightarrow> χ α) in v]" using RN_2 by blast qed
lemma sign_S5_thm_5[PLM]: "[((\<box>(\<forall>α. φ α \<equiv> ψ α)) & (\<box>(\<forall>α. ψ α \<equiv> χ α))) \<rightarrow> (\<box>(\<forall>α. φ α \<equiv> χ α)) in v]" proof (rule CP) assume"[\<box>(\<forall>α. φ α \<equiv> ψ α) &\<box>(\<forall>α. ψ α \<equiv> χ α) in v]" hence"[\<box>((\<forall>α. φ α \<equiv> ψ α) & (\<forall>α. ψ α \<equiv> χ α)) in v]" using KBasic_3[equiv_rl] by blast moreover { fix v assume"[((\<forall>α. φ α \<equiv> ψ α) & (\<forall>α. ψ α \<equiv> χ α)) in v]" hence"[(\<forall> α . φ α \<equiv> χ α) in v]" using cqt_basic_10[deduction] by blast
} ultimatelyshow"[\<box>(\<forall>α. φ α \<equiv> χ α) in v]" using RN_2 by blast qed
lemma id_nec2_1[PLM]: "[\<diamond>((α::'a::id_eq) = β) \<equiv> (α = β) in v]" apply (rule "\<equiv>I"; rule CP) using id_nec[equiv_lr] derived_S5_rules_2_b CP modus_ponens apply blast using"T\<diamond>"[deduction] by auto
lemma id_nec2_2_Aux: "[(\<diamond>φ) \<equiv> ψ in v] ==> [(\<not>ψ) \<equiv> \<box>(\<not>φ) in v]" proof - assume"[(\<diamond>φ) \<equiv> ψ in v]" moreoverhave"∧φ ψ. [(\<not>φ) \<equiv> ψ in v] ==> [(\<not>ψ) \<equiv> φ in v]" by PLM_solver ultimatelyshow ?thesis unfolding diamond_def by blast qed
lemma id_nec2_2[PLM]: "[((α::'a::id_eq) \<noteq> β) \<equiv> \<box>(α \<noteq> β) in v]" using id_nec2_1[THEN id_nec2_2_Aux] by auto
lemma id_nec2_3[PLM]: "[(\<diamond>((α::'a::id_eq) \<noteq> β)) \<equiv> (α \<noteq> β) in v]" using"T\<diamond>""\<equiv>I" id_nec2_2[equiv_lr]
CP derived_S5_rules_2_b by metis
lemma exists_desc_box_1[PLM]: "[(\<exists> y . (yP) = (\<iota>x. φ x)) \<rightarrow> (\<exists> y . \<box>((yP) = (\<iota>x. φ x))) in v]" proof (rule CP) assume"[\<exists>y. (yP) = (\<iota>x. φ x) in v]" thenobtain y where"[(yP) = (\<iota>x. φ x) in v]" by (rule "\<exists>E") hence"[\<box>(yP= (\<iota>x. φ x)) in v]" using l_identity[axiom_instance, deduction, deduction]
cqt_1[axiom_instance] all_self_eq_2[where 'a=ν]
modus_ponens unfolding identity_ν_defby fast thus"[\<exists>y. \<box>((yP) = (\<iota>x. φ x)) in v]" by (rule "\<exists>I") qed
lemma exists_desc_box_2[PLM]: "[(\<exists> y . (yP) = (\<iota>x. φ x)) \<rightarrow> \<box>(\<exists> y .((yP) = (\<iota>x. φ x))) in v]" using exists_desc_box_1 Buridan ded_thm_cor_3 by fast
lemma en_eq_1[PLM]: "[\<diamond>{x,F}\<equiv> \<box>{x,F} in v]" using encoding[axiom_instance] RN
sc_eq_box_box_1 modus_ponens by blast lemma en_eq_2[PLM]: "[{x,F}\<equiv> \<box>{x,F} in v]" using encoding[axiom_instance] qml_2[axiom_instance] by (rule "\<equiv>I") lemma en_eq_3[PLM]: "[\<diamond>{x,F}\<equiv> {x,F} in v]" using encoding[axiom_instance] derived_S5_rules_2_b "\<equiv>I""T\<diamond>"by auto lemma en_eq_4[PLM]: "[({x,F}\<equiv> {y,G}) \<equiv> (\<box>{x,F}\<equiv> \<box>{y,G}) in v]" by (metis CP en_eq_2 "\<equiv>I""\<equiv>E"(1) "\<equiv>E"(2)) lemma en_eq_5[PLM]: "[\<box>({x,F}\<equiv> {y,G}) \<equiv> (\<box>{x,F}\<equiv> \<box>{y,G}) in v]" using"\<equiv>I" KBasic_6 encoding[axiom_necessitation, axiom_instance]
sc_eq_box_box_3[deduction] "&I"by simp lemma en_eq_6[PLM]: "[({x,F}\<equiv> {y,G}) \<equiv> \<box>({x,F}\<equiv> {y,G}) in v]" using en_eq_4 en_eq_5 oth_class_taut_4_a "\<equiv>E"(6) by meson lemma en_eq_7[PLM]: "[(\<not>{x,F}) \<equiv> \<box>(\<not>{x,F}) in v]" using en_eq_3[THEN id_nec2_2_Aux] by blast lemma en_eq_8[PLM]: "[\<diamond>(\<not>{x,F}) \<equiv> (\<not>{x,F}) in v]" unfolding diamond_def apply (PLM_subst_method "{x,F}""\<not>\<not>{x,F}") using oth_class_taut_4_b apply simp apply (PLM_subst_method "{x,F}""\<box>{x,F}") using en_eq_2 apply simp using oth_class_taut_4_a by assumption lemma en_eq_9[PLM]: "[\<diamond>(\<not>{x,F}) \<equiv> \<box>(\<not>{x,F}) in v]" using en_eq_8 en_eq_7 "\<equiv>E"(5) by blast lemma en_eq_10[PLM]: "[\<A>{x,F}\<equiv> {x,F} in v]" apply (rule "\<equiv>I") using encoding[axiom_actualization, axiom_instance, THEN logic_actual_nec_2[axiom_instance, equiv_lr],
deduction, THEN qml_act_2[axiom_instance, equiv_rl], THEN en_eq_2[equiv_rl]] CP apply simp using encoding[axiom_instance] nec_imp_act ded_thm_cor_3 by blast
subsection‹The Theory of Relations› text‹\label{TAO_PLM_Relations}›
lemma beta_equiv_eq_1_1[PLM]: assumes"IsProperInX φ" and"IsProperInX ψ" and"∧x.[φ (xP) \<equiv> ψ (xP) in v]" shows"[(\<lambda> y. φ (yP), xP)\<equiv> (\<lambda> y. ψ (yP), xP) in v]" using lambda_predicates_2_1[OF assms(1), axiom_instance] using lambda_predicates_2_1[OF assms(2), axiom_instance] using assms(3) by (meson "\<equiv>E"(6) oth_class_taut_4_a)
lemma beta_equiv_eq_1_2[PLM]: assumes"IsProperInXY φ" and"IsProperInXY ψ" and"∧x y.[φ (xP) (yP) \<equiv> ψ (xP) (yP) in v]" shows"[(\<lambda>2 (λ x y. φ (xP) (yP)), xP, yP) \<equiv> (\<lambda>2 (λ x y. ψ (xP) (yP)), xP, yP) in v]" using lambda_predicates_2_2[OF assms(1), axiom_instance] using lambda_predicates_2_2[OF assms(2), axiom_instance] using assms(3) by (meson "\<equiv>E"(6) oth_class_taut_4_a)
lemma beta_equiv_eq_1_3[PLM]: assumes"IsProperInXYZ φ" and"IsProperInXYZ ψ" and"∧x y z.[φ (xP) (yP) (zP) \<equiv> ψ (xP) (yP) (zP) in v]" shows"[(\<lambda>3 (λ x y z. φ (xP) (yP) (zP)), xP, yP, zP) \<equiv> (\<lambda>3 (λ x y z. ψ (xP) (yP) (zP)), xP, yP, zP) in v]" using lambda_predicates_2_3[OF assms(1), axiom_instance] using lambda_predicates_2_3[OF assms(2), axiom_instance] using assms(3) by (meson "\<equiv>E"(6) oth_class_taut_4_a)
lemma beta_equiv_eq_2_1[PLM]: assumes"IsProperInX φ" and"IsProperInX ψ" shows"[(\<box>(\<forall> x . φ (xP) \<equiv> ψ (xP))) \<rightarrow> (\<box>(\<forall> x . (\<lambda> y. φ (yP), xP)\<equiv> (\<lambda> y. ψ (yP), xP))) in v]" apply (rule qml_1[axiom_instance, deduction]) apply (rule RN) proof (rule CP, rule "\<forall>I") fix v x assume"[\<forall>x. φ (xP) \<equiv> ψ (xP) in v]" hence"∧x.[φ (xP) \<equiv> ψ (xP) in v]" by PLM_solver thus"[(\<lambda> y. φ (yP), xP)\<equiv> (\<lambda> y. ψ (yP), xP) in v]" using assms beta_equiv_eq_1_1 by auto qed
lemma beta_equiv_eq_2_2[PLM]: assumes"IsProperInXY φ" and"IsProperInXY ψ" shows"[(\<box>(\<forall> x y . φ (xP) (yP) \<equiv> ψ (xP) (yP))) \<rightarrow> (\<box>(\<forall> x y . (\<lambda>2 (λ x y. φ (xP) (yP)), xP, yP) \<equiv> (\<lambda>2 (λ x y. ψ (xP) (yP)), xP, yP))) in v]" apply (rule qml_1[axiom_instance, deduction]) apply (rule RN) proof (rule CP, rule "\<forall>I", rule "\<forall>I") fix v x y assume"[\<forall>x y. φ (xP) (yP) \<equiv> ψ (xP) (yP) in v]" hence"(∧x y.[φ (xP) (yP) \<equiv> ψ (xP) (yP) in v])" by (meson "\<forall>E") thus"[(\<lambda>2 (λ x y. φ (xP) (yP)), xP, yP) \<equiv> (\<lambda>2 (λ x y. ψ (xP) (yP)), xP, yP) in v]" using assms beta_equiv_eq_1_2 by auto qed
lemma beta_equiv_eq_2_3[PLM]: assumes"IsProperInXYZ φ" and"IsProperInXYZ ψ" shows"[(\<box>(\<forall> x y z . φ (xP) (yP) (zP) \<equiv> ψ (xP) (yP) (zP))) \<rightarrow> (\<box>(\<forall> x y z . (\<lambda>3 (λ x y z. φ (xP) (yP) (zP)), xP, yP, zP) \<equiv> (\<lambda>3 (λ x y z. ψ (xP) (yP) (zP)), xP, yP, zP))) in v]" apply (rule qml_1[axiom_instance, deduction]) apply (rule RN) proof (rule CP, rule "\<forall>I", rule "\<forall>I", rule "\<forall>I") fix v x y z assume"[\<forall>x y z. φ (xP) (yP) (zP) \<equiv> ψ (xP) (yP) (zP) in v]" hence"(∧x y z.[φ (xP) (yP) (zP) \<equiv> ψ (xP) (yP) (zP) in v])" by (meson "\<forall>E") thus"[(\<lambda>3 (λ x y z. φ (xP) (yP) (zP)), xP, yP, zP) \<equiv> (\<lambda>3 (λ x y z. ψ (xP) (yP) (zP)), xP, yP, zP) in v]" using assms beta_equiv_eq_1_3 by auto qed
lemma beta_C_meta_1[PLM]: assumes"IsProperInX φ" shows"[(\<lambda> y. φ (yP), xP)\<equiv> φ (xP) in v]" using lambda_predicates_2_1[OF assms, axiom_instance] by auto
lemma beta_C_meta_2[PLM]: assumes"IsProperInXY φ" shows"[(\<lambda>2 (λ x y. φ (xP) (yP)), xP, yP)\<equiv> φ (xP) (yP) in v]" using lambda_predicates_2_2[OF assms, axiom_instance] by auto
lemma beta_C_meta_3[PLM]: assumes"IsProperInXYZ φ" shows"[(\<lambda>3 (λ x y z. φ (xP) (yP) (zP)), xP, yP, zP)\<equiv> φ (xP) (yP) (zP) in v]" using lambda_predicates_2_3[OF assms, axiom_instance] by auto
lemma relations_1[PLM]: assumes"IsProperInX φ" shows"[\<exists> F. \<box>(\<forall> x. (F,xP)\<equiv> φ (xP)) in v]" using assms apply - by PLM_solver
lemma relations_2[PLM]: assumes"IsProperInXY φ" shows"[\<exists> F. \<box>(\<forall> x y. (F,xP,yP)\<equiv> φ (xP) (yP)) in v]" using assms apply - by PLM_solver
lemma relations_3[PLM]: assumes"IsProperInXYZ φ" shows"[\<exists> F. \<box>(\<forall> x y z. (F,xP,yP,zP)\<equiv> φ (xP) (yP) (zP)) in v]" using assms apply - by PLM_solver
lemma prop_equiv[PLM]: shows"[(\<forall> x . ({xP,F}\<equiv> {xP,G})) \<rightarrow> F = G in v]" proof (rule CP) assume1: "[\<forall>x. {xP,F}\<equiv> {xP,G} in v]"
{ fix x have"[{xP,F}\<equiv> {xP,G} in v]" using1by (rule "\<forall>E") hence"[\<box>({xP,F}\<equiv> {xP,G}) in v]" using PLM.en_eq_6 "\<equiv>E"(1) by blast
} hence"[\<forall>x. \<box>({xP,F}\<equiv> {xP,G}) in v]" by (rule "\<forall>I") thus"[F = G in v]" unfolding identity_defs by (rule BF[deduction]) qed
lemma propositions_lemma_1[PLM]: "[\<lambda>0 φ = φ in v]" using lambda_predicates_3_0[axiom_instance] .
lemma propositions_lemma_2[PLM]: "[\<lambda>0 φ \<equiv> φ in v]" using lambda_predicates_3_0[axiom_instance, THEN id_eq_prop_prop_8_b[deduction]] apply (rule l_identity[axiom_instance, deduction, deduction]) by PLM_solver
lemma propositions_lemma_4[PLM]: assumes"∧x.[\<A>(φ x \<equiv> ψ x) in v]" shows"[(χ::κ→o) (\<iota>x. φ x) = χ (\<iota>x. ψ x) in v]" proof - have"[\<lambda>0 (χ (\<iota>x. φ x)) =\<lambda>0 (χ (\<iota>x. ψ x)) in v]" using assms lambda_predicates_4_0[axiom_instance] by blast hence"[(χ (\<iota>x. φ x)) =\<lambda>0 (χ (\<iota>x. ψ x)) in v]" using propositions_lemma_1[THEN id_eq_prop_prop_8_b[deduction]]
id_eq_prop_prop_9_b[deduction] "&I" by blast thus ?thesis using propositions_lemma_1 id_eq_prop_prop_9_b[deduction] "&I" by blast qed
lemma propositions[PLM]: "[\<exists> p . \<box>(p \<equiv> p') in v]" by PLM_solver
lemma pos_not_equiv_then_not_eq[PLM]: "[\<diamond>(\<not>(\<forall>x. (F,xP)\<equiv> (G,xP))) \<rightarrow> F \<noteq> G in v]" unfolding diamond_def proof (subst contraposition_1[symmetric], rule CP) assume"[F = G in v]" thus"[\<box>(\<not>(\<not>(\<forall>x. (F,xP)\<equiv> (G,xP)))) in v]" apply (rule l_identity[axiom_instance, deduction, deduction]) by PLM_solver qed
lemma thm_relation_negation_1_1[PLM]: "[(F-, xP)\<equiv> \<not>(F, xP) in v]" unfolding propnot_defs apply (rule lambda_predicates_2_1[axiom_instance]) by show_proper
lemma thm_relation_negation_1_2[PLM]: "[(F-, xP, yP)\<equiv> \<not>(F, xP, yP) in v]" unfolding propnot_defs apply (rule lambda_predicates_2_2[axiom_instance]) by show_proper
lemma thm_relation_negation_1_3[PLM]: "[(F-, xP, yP, zP)\<equiv> \<not>(F, xP, yP, zP) in v]" unfolding propnot_defs apply (rule lambda_predicates_2_3[axiom_instance]) by show_proper
lemma thm_relation_negation_2_1[PLM]: "[(\<not>(F-, xP)) \<equiv> (F, xP) in v]" using thm_relation_negation_1_1[THEN oth_class_taut_5_d[equiv_lr]] apply - by PLM_solver
lemma thm_relation_negation_2_2[PLM]: "[(\<not>(F-, xP, yP)) \<equiv> (F, xP, yP) in v]" using thm_relation_negation_1_2[THEN oth_class_taut_5_d[equiv_lr]] apply - by PLM_solver
lemma thm_relation_negation_2_3[PLM]: "[(\<not>(F-, xP, yP, zP)) \<equiv> (F, xP, yP, zP) in v]" using thm_relation_negation_1_3[THEN oth_class_taut_5_d[equiv_lr]] apply - by PLM_solver
lemma thm_relation_negation_3[PLM]: "[(p)-\<equiv> \<not>p in v]" unfolding propnot_defs using propositions_lemma_2 by simp
lemma thm_relation_negation_4[PLM]: "[(\<not>((p::o)-)) \<equiv> p in v]" using thm_relation_negation_3[THEN oth_class_taut_5_d[equiv_lr]] apply - by PLM_solver
lemma thm_relation_negation_5_1[PLM]: "[(F::Π1) \<noteq> (F-) in v]" using id_eq_prop_prop_2[deduction]
l_identity[where φ="λ G . (G,xP)\<equiv> (F-,xP)", axiom_instance,
deduction, deduction]
oth_class_taut_4_a thm_relation_negation_1_1 "\<equiv>E"(5)
oth_class_taut_1_b modus_tollens_1 CP by meson
lemma thm_relation_negation_5_2[PLM]: "[(F::Π2) \<noteq> (F-) in v]" using id_eq_prop_prop_5_a[deduction]
l_identity[where φ="λ G . (G,xP,yP)\<equiv> (F-,xP,yP)", axiom_instance,
deduction, deduction]
oth_class_taut_4_a thm_relation_negation_1_2 "\<equiv>E"(5)
oth_class_taut_1_b modus_tollens_1 CP by meson
lemma thm_relation_negation_5_3[PLM]: "[(F::Π3) \<noteq> (F-) in v]" using id_eq_prop_prop_5_b[deduction]
l_identity[where φ="λ G . (G,xP,yP,zP)\<equiv> (F-,xP,yP,zP)",
axiom_instance, deduction, deduction]
oth_class_taut_4_a thm_relation_negation_1_3 "\<equiv>E"(5)
oth_class_taut_1_b modus_tollens_1 CP by meson
lemma thm_relation_negation_6[PLM]: "[(p::o) \<noteq> (p-) in v]" using id_eq_prop_prop_8_b[deduction]
l_identity[where φ="λ G . G \<equiv> (p-)", axiom_instance,
deduction, deduction]
oth_class_taut_4_a thm_relation_negation_3 "\<equiv>E"(5)
oth_class_taut_1_b modus_tollens_1 CP by meson
lemma thm_relation_negation_7[PLM]: "[((p::o)-) =\<not>p in v]" unfolding propnot_defs using propositions_lemma_1 by simp
lemma thm_relation_negation_8[PLM]: "[(p::o) \<noteq> \<not>p in v]" unfolding propnot_defs using id_eq_prop_prop_8_b[deduction]
l_identity[where φ="λ G . G \<equiv> \<not>(p)", axiom_instance,
deduction, deduction]
oth_class_taut_4_a oth_class_taut_1_b
modus_tollens_1 CP by meson
lemma thm_relation_negation_9[PLM]: "[((p::o) = q) \<rightarrow> ((\<not>p) = (\<not>q)) in v]" using l_identity[where α="p"and β="q"and φ="λ x . (\<not>p) = (\<not>x)",
axiom_instance, deduction]
id_eq_prop_prop_7_b using CP modus_ponens by blast
lemma thm_relation_negation_10[PLM]: "[((p::o) = q) \<rightarrow> ((p-) = (q-)) in v]" using l_identity[where α="p"and β="q"and φ="λ x . (p-) = (x-)",
axiom_instance, deduction]
id_eq_prop_prop_7_b using CP modus_ponens by blast
lemma thm_cont_prop_1[PLM]: "[NonContingent (F::Π1) \<equiv> NonContingent (F-) in v]" proof (rule "\<equiv>I"; rule CP) assume"[NonContingent F in v]" hence"[\<box>(\<forall>x.(F,xP)) \<or> \<box>(\<forall>x.\<not>(F,xP)) in v]" unfolding NonContingent_def Necessary_defs Impossible_defs . hence"[\<box>(\<forall>x. \<not>(F-,xP)) \<or> \<box>(\<forall>x. \<not>(F,xP)) in v]" apply - apply (PLM_subst_method "λ x . (F,xP)""λ x . \<not>(F-,xP)") using thm_relation_negation_2_1[equiv_sym] by auto hence"[\<box>(\<forall>x. \<not>(F-,xP)) \<or> \<box>(\<forall>x. (F-,xP)) in v]" apply - apply (PLM_subst_goal_method "λ φ . \<box>(\<forall>x. \<not>(F-,xP)) \<or> \<box>(\<forall>x. φ x)""λ x . \<not>(F,xP)") using thm_relation_negation_1_1[equiv_sym] by auto hence"[\<box>(\<forall>x. (F-,xP)) \<or> \<box>(\<forall>x. \<not>(F-,xP)) in v]" by (rule oth_class_taut_3_e[equiv_lr]) thus"[NonContingent (F-) in v]" unfolding NonContingent_def Necessary_defs Impossible_defs . next assume"[NonContingent (F-) in v]" hence"[\<box>(\<forall>x. \<not>(F-,xP)) \<or> \<box>(\<forall>x. (F-,xP)) in v]" unfolding NonContingent_def Necessary_defs Impossible_defs by (rule oth_class_taut_3_e[equiv_lr]) hence"[\<box>(\<forall>x.(F,xP)) \<or> \<box>(\<forall>x.(F-,xP)) in v]" apply - apply (PLM_subst_method "λ x . \<not>(F-,xP)""λ x . (F,xP)") using thm_relation_negation_2_1 by auto hence"[\<box>(\<forall>x. (F,xP)) \<or> \<box>(\<forall>x. \<not>(F,xP)) in v]" apply - apply (PLM_subst_method "λ x . (F-,xP)""λ x . \<not>(F,xP)") using thm_relation_negation_1_1 by auto thus"[NonContingent F in v]" unfolding NonContingent_def Necessary_defs Impossible_defs . qed
lemma thm_cont_prop_2[PLM]: "[Contingent F \<equiv> \<diamond>(\<exists> x . (F,xP)) &\<diamond>(\<exists> x . \<not>(F,xP)) in v]" proof (rule "\<equiv>I"; rule CP) assume"[Contingent F in v]" hence"[\<not>(\<box>(\<forall>x.(F,xP)) \<or> \<box>(\<forall>x.\<not>(F,xP))) in v]" unfolding Contingent_def Necessary_defs Impossible_defs . hence"[(\<not>\<box>(\<forall>x.(F,xP))) & (\<not>\<box>(\<forall>x.\<not>(F,xP))) in v]" by (rule oth_class_taut_6_d[equiv_lr]) hence"[(\<diamond>\<not>(\<forall>x.\<not>(F,xP))) & (\<diamond>\<not>(\<forall>x.(F,xP))) in v]" using KBasic2_2[equiv_lr] "&I""&E"by meson thus"[(\<diamond>(\<exists> x.(F,xP))) & (\<diamond>(\<exists>x. \<not>(F,xP))) in v]" unfolding exists_def apply - apply (PLM_subst_method "λ x . (F,xP)""λ x . \<not>\<not>(F,xP)") using oth_class_taut_4_b by auto next assume"[(\<diamond>(\<exists> x.(F,xP))) & (\<diamond>(\<exists>x. \<not>(F,xP))) in v]" hence"[(\<diamond>\<not>(\<forall>x.\<not>(F,xP))) & (\<diamond>\<not>(\<forall>x.(F,xP))) in v]" unfolding exists_def apply - apply (PLM_subst_goal_method "λ φ . (\<diamond>\<not>(\<forall>x.\<not>(F,xP))) & (\<diamond>\<not>(\<forall>x. φ x))""λ x . \<not>\<not>(F,xP)") using oth_class_taut_4_b[equiv_sym] by auto hence"[(\<not>\<box>(\<forall>x.(F,xP))) & (\<not>\<box>(\<forall>x.\<not>(F,xP))) in v]" using KBasic2_2[equiv_rl] "&I""&E"by meson hence"[\<not>(\<box>(\<forall>x.(F,xP)) \<or> \<box>(\<forall>x.\<not>(F,xP))) in v]" by (rule oth_class_taut_6_d[equiv_rl]) thus"[Contingent F in v]" unfolding Contingent_def Necessary_defs Impossible_defs . qed
lemma thm_cont_prop_3[PLM]: "[Contingent (F::Π1) \<equiv> Contingent (F-) in v]" using thm_cont_prop_1 unfolding NonContingent_def Contingent_def by (rule oth_class_taut_5_d[equiv_lr])
lemma lem_cont_e[PLM]: "[\<diamond>(\<exists> x . (F,xP)& (\<diamond>(\<not>(F,xP)))) \<equiv> \<diamond>(\<exists> x . ((\<not>(F,xP)) &\<diamond>(F,xP)))in v]" proof - have"[\<diamond>(\<exists> x . (F,xP)& (\<diamond>(\<not>(F,xP)))) in v] = [(\<exists> x . \<diamond>((F,xP)&\<diamond>(\<not>(F,xP)))) in v]" using"BF\<diamond>"[deduction] "CBF\<diamond>"[deduction] by fast alsohave"... = [\<exists> x . (\<diamond>(F,xP)&\<diamond>(\<not>(F,xP))) in v]" apply (PLM_subst_method "λ x . \<diamond>((F,xP)&\<diamond>(\<not>(F,xP)))" "λ x . \<diamond>(F,xP)&\<diamond>(\<not>(F,xP))") using S5Basic_12 by auto alsohave"... = [\<exists> x . \<diamond>(\<not>(F,xP)) &\<diamond>(F,xP) in v]" apply (PLM_subst_method "λ x . \<diamond>(F,xP)&\<diamond>(\<not>(F,xP))" "λ x . \<diamond>(\<not>(F,xP)) &\<diamond>(F,xP)") using oth_class_taut_3_b by auto alsohave"... = [\<exists> x . \<diamond>((\<not>(F,xP)) &\<diamond>(F,xP)) in v]" apply (PLM_subst_method "λ x . \<diamond>(\<not>(F,xP)) &\<diamond>(F,xP)" "λ x . \<diamond>((\<not>(F,xP)) &\<diamond>(F,xP))") using S5Basic_12[equiv_sym] by auto alsohave"... = [\<diamond> (\<exists> x . ((\<not>(F,xP)) &\<diamond>(F,xP))) in v]" using"CBF\<diamond>"[deduction] "BF\<diamond>"[deduction] by fast finallyshow ?thesis using"\<equiv>I" CP by blast qed
lemma lem_cont_e_2[PLM]: "[\<diamond>(\<exists> x . (F,xP)&\<diamond>(\<not>(F,xP))) \<equiv> \<diamond>(\<exists> x . (F-,xP)&\<diamond>(\<not>(F-,xP))) in v]" apply (PLM_subst_method "λ x . (F,xP)""λ x . \<not>(F-,xP)") using thm_relation_negation_2_1[equiv_sym] apply simp apply (PLM_subst_method "λ x . \<not>(F,xP)""λ x . (F-,xP)") using thm_relation_negation_1_1[equiv_sym] apply simp using lem_cont_e by simp
lemma thm_cont_e_1[PLM]: "[\<diamond>(\<exists> x . ((\<not>(E!,xP)) & (\<diamond>(E!,xP)))) in v]" using lem_cont_e[where F="E!", equiv_lr] qml_4[axiom_instance,conj1] by blast
lemma thm_cont_e_2[PLM]: "[Contingent (E!) in v]" using thm_cont_prop_2[equiv_rl] "&I" qml_4[axiom_instance, conj1]
KBasic2_8[deduction, OF sign_S5_thm_3[deduction], conj1]
KBasic2_8[deduction, OF sign_S5_thm_3[deduction, OF thm_cont_e_1], conj1] by fast
lemma thm_cont_e_3[PLM]: "[Contingent (E!-) in v]" using thm_cont_e_2 thm_cont_prop_3[equiv_lr] by blast
lemma thm_cont_e_4[PLM]: "[\<exists> (F::Π1) G . (F \<noteq> G & Contingent F & Contingent G) in v]" apply (rule_tac α="E!"in"\<exists>I", rule_tac α="E!-"in"\<exists>I") using thm_cont_e_2 thm_cont_e_3 thm_relation_negation_5_1 "&I"by auto
context begin
qualified definition L where"L ≡ (\<lambda> x . (E!, xP)\<rightarrow> (E!, xP))"
lemma thm_noncont_e_e_1[PLM]: "[Necessary L in v]" unfolding Necessary_defs L_def apply (rule RN, rule "\<forall>I") apply (rule lambda_predicates_2_1[axiom_instance, equiv_rl]) apply show_proper using if_p_then_p .
lemma thm_noncont_e_e_3[PLM]: "[NonContingent (L) in v]" unfolding NonContingent_def using thm_noncont_e_e_1 by (rule "\<or>I"(1))
lemma thm_noncont_e_e_4[PLM]: "[NonContingent (L-) in v]" unfolding NonContingent_def using thm_noncont_e_e_2 by (rule "\<or>I"(2))
lemma thm_noncont_e_e_5[PLM]: "[\<exists> (F::Π1) G . F \<noteq> G & NonContingent F & NonContingent G in v]" apply (rule_tac α="L"in"\<exists>I", rule_tac α="L-"in"\<exists>I") using"\<exists>I" thm_relation_negation_5_1 thm_noncont_e_e_3
thm_noncont_e_e_4 "&I" by simp
lemma four_distinct_1[PLM]: "[NonContingent (F::Π1) \<rightarrow> \<not>(\<exists> G . (Contingent G & G = F)) in v]" proof (rule CP) assume"[NonContingent F in v]" hence"[\<not>(Contingent F) in v]" unfolding NonContingent_def Contingent_def apply - by PLM_solver moreover { assume"[\<exists> G . Contingent G & G = F in v]" thenobtain P where"[Contingent P & P = F in v]" by (rule "\<exists>E") hence"[Contingent F in v]" using"&E" l_identity[axiom_instance, deduction, deduction] by blast
} ultimatelyshow"[\<not>(\<exists>G. Contingent G & G = F) in v]" using modus_tollens_1 CP by blast qed
lemma four_distinct_2[PLM]: "[Contingent (F::Π1) \<rightarrow> \<not>(\<exists> G . (NonContingent G & G = F)) in v]" proof (rule CP) assume"[Contingent F in v]" hence"[\<not>(NonContingent F) in v]" unfolding NonContingent_def Contingent_def apply - by PLM_solver moreover { assume"[\<exists> G . NonContingent G & G = F in v]" thenobtain P where"[NonContingent P & P = F in v]" by (rule "\<exists>E") hence"[NonContingent F in v]" using"&E" l_identity[axiom_instance, deduction, deduction] by blast
} ultimatelyshow"[\<not>(\<exists>G. NonContingent G & G = F) in v]" using modus_tollens_1 CP by blast qed
lemma four_distinct_3[PLM]: "[L \<noteq> (L-) & L \<noteq> E! & L \<noteq> (E!-) & (L-) \<noteq> E! & (L-) \<noteq> (E!-) & E! \<noteq> (E!-) in v]" proof (rule "&I")+ show"[L \<noteq> (L-) in v]" by (rule thm_relation_negation_5_1) next
{ assume"[L = E! in v]" hence"[NonContingent L & L = E! in v]" using thm_noncont_e_e_3 "&I"by auto hence"[\<exists> G . NonContingent G & G = E! in v]" using thm_noncont_e_e_3 "&I""\<exists>I"by fast
} thus"[L \<noteq> E! in v]" using four_distinct_2[deduction, OF thm_cont_e_2]
modus_tollens_1 CP by blast next
{ assume"[L = (E!-) in v]" hence"[NonContingent L & L = (E!-) in v]" using thm_noncont_e_e_3 "&I"by auto hence"[\<exists> G . NonContingent G & G = (E!-) in v]" using thm_noncont_e_e_3 "&I""\<exists>I"by fast
} thus"[L \<noteq> (E!-) in v]" using four_distinct_2[deduction, OF thm_cont_e_3]
modus_tollens_1 CP by blast next
{ assume"[(L-) = E! in v]" hence"[NonContingent (L-) & (L-) = E! in v]" using thm_noncont_e_e_4 "&I"by auto hence"[\<exists> G . NonContingent G & G = E! in v]" using thm_noncont_e_e_3 "&I""\<exists>I"by fast
} thus"[(L-) \<noteq> E! in v]" using four_distinct_2[deduction, OF thm_cont_e_2]
modus_tollens_1 CP by blast next
{ assume"[(L-) = (E!-) in v]" hence"[NonContingent (L-) & (L-) = (E!-) in v]" using thm_noncont_e_e_4 "&I"by auto hence"[\<exists> G . NonContingent G & G = (E!-) in v]" using thm_noncont_e_e_3 "&I""\<exists>I"by fast
} thus"[(L-) \<noteq> (E!-) in v]" using four_distinct_2[deduction, OF thm_cont_e_3]
modus_tollens_1 CP by blast next show"[E! \<noteq> (E!-) in v]" by (rule thm_relation_negation_5_1) qed end
lemma thm_cont_propos_1[PLM]: "[NonContingent (p::o) \<equiv> NonContingent (p-) in v]" proof (rule "\<equiv>I"; rule CP) assume"[NonContingent p in v]" hence"[\<box>p \<or> \<box>\<not>p in v]" unfolding NonContingent_def Necessary_defs Impossible_defs . hence"[\<box>(\<not>(p-)) \<or> \<box>(\<not>p) in v]" apply - apply (PLM_subst_method "p""\<not>(p-)") using thm_relation_negation_4[equiv_sym] by auto hence"[\<box>(\<not>(p-)) \<or> \<box>(p-) in v]" apply - apply (PLM_subst_goal_method "λφ . \<box>(\<not>(p-)) \<or> \<box>(φ)""\<not>p") using thm_relation_negation_3[equiv_sym] by auto hence"[\<box>(p-) \<or> \<box>(\<not>(p-)) in v]" by (rule oth_class_taut_3_e[equiv_lr]) thus"[NonContingent (p-) in v]" unfolding NonContingent_def Necessary_defs Impossible_defs . next assume"[NonContingent (p-) in v]" hence"[\<box>(\<not>(p-)) \<or> \<box>(p-) in v]" unfolding NonContingent_def Necessary_defs Impossible_defs by (rule oth_class_taut_3_e[equiv_lr]) hence"[\<box>(p) \<or> \<box>(p-) in v]" apply - apply (PLM_subst_goal_method "λφ . \<box>φ \<or> \<box>(p-)""\<not>(p-)") using thm_relation_negation_4 by auto hence"[\<box>(p) \<or> \<box>(\<not>p) in v]" apply - apply (PLM_subst_method "p-""\<not>p") using thm_relation_negation_3 by auto thus"[NonContingent p in v]" unfolding NonContingent_def Necessary_defs Impossible_defs . qed
lemma thm_cont_propos_2[PLM]: "[Contingent p \<equiv> \<diamond>p &\<diamond>(\<not>p) in v]" proof (rule "\<equiv>I"; rule CP) assume"[Contingent p in v]" hence"[\<not>(\<box>p \<or> \<box>(\<not>p)) in v]" unfolding Contingent_def Necessary_defs Impossible_defs . hence"[(\<not>\<box>p) & (\<not>\<box>(\<not>p)) in v]" by (rule oth_class_taut_6_d[equiv_lr]) hence"[(\<diamond>\<not>(\<not>p)) & (\<diamond>\<not>p) in v]" using KBasic2_2[equiv_lr] "&I""&E"by meson thus"[(\<diamond>p) & (\<diamond>(\<not>p)) in v]" apply - apply PLM_solver apply (PLM_subst_method "\<not>\<not>p""p") using oth_class_taut_4_b[equiv_sym] by auto next assume"[(\<diamond>p) & (\<diamond>\<not>(p)) in v]" hence"[(\<diamond>\<not>(\<not>p)) & (\<diamond>\<not>(p)) in v]" apply - apply PLM_solver apply (PLM_subst_method "p""\<not>\<not>p") using oth_class_taut_4_b by auto hence"[(\<not>\<box>p) & (\<not>\<box>(\<not>p)) in v]" using KBasic2_2[equiv_rl] "&I""&E"by meson hence"[\<not>(\<box>(p) \<or> \<box>(\<not>p)) in v]" by (rule oth_class_taut_6_d[equiv_rl]) thus"[Contingent p in v]" unfolding Contingent_def Necessary_defs Impossible_defs . qed
lemma thm_cont_propos_3[PLM]: "[Contingent (p::o) \<equiv> Contingent (p-) in v]" using thm_cont_propos_1 unfolding NonContingent_def Contingent_def by (rule oth_class_taut_5_d[equiv_lr])
context begin privatedefinition p0where "p0≡\<forall>x. (E!,xP)\<rightarrow> (E!,xP)"
lemma thm_noncont_propos_1[PLM]: "[Necessary p0 in v]" unfolding Necessary_defs p0_def apply (rule RN, rule "\<forall>I") using if_p_then_p .
lemma thm_noncont_propos_2[PLM]: "[Impossible (p0-) in v]" unfolding Impossible_defs apply (PLM_subst_method "\<not>p0""p0-") using thm_relation_negation_3[equiv_sym] apply simp apply (PLM_subst_method "p0""\<not>\<not>p0") using oth_class_taut_4_b apply simp using thm_noncont_propos_1 unfolding Necessary_defs by simp
lemma thm_noncont_propos_3[PLM]: "[NonContingent (p0) in v]" unfolding NonContingent_def using thm_noncont_propos_1 by (rule "\<or>I"(1))
lemma thm_noncont_propos_4[PLM]: "[NonContingent (p0-) in v]" unfolding NonContingent_def using thm_noncont_propos_2 by (rule "\<or>I"(2))
lemma thm_noncont_propos_5[PLM]: "[\<exists> (p::o) q . p \<noteq> q & NonContingent p & NonContingent q in v]" apply (rule_tac α="p0"in"\<exists>I", rule_tac α="p0-"in"\<exists>I") using"\<exists>I" thm_relation_negation_6 thm_noncont_propos_3
thm_noncont_propos_4 "&I"by simp
privatedefinition q0where "q0≡\<exists> x . (E!,xP)&\<diamond>(\<not>(E!,xP))"
lemma basic_prop_1[PLM]: "[\<exists> p . \<diamond>p &\<diamond>(\<not>p) in v]" apply (rule_tac α="q0"in"\<exists>I") unfolding q0_def using qml_4[axiom_instance] by simp
lemma basic_prop_2[PLM]: "[Contingent q0 in v]" unfolding Contingent_def Necessary_defs Impossible_defs apply (rule oth_class_taut_6_d[equiv_rl]) apply (PLM_subst_goal_method "λ φ . (\<not>\<box>(φ)) &\<not>\<box>\<not>q0""\<not>\<not>q0") using oth_class_taut_4_b[equiv_sym] apply simp using qml_4[axiom_instance,conj_sym] unfolding q0_def diamond_def by simp
lemma basic_prop_3[PLM]: "[Contingent (q0-) in v]" apply (rule thm_cont_propos_3[equiv_lr]) using basic_prop_2 .
lemma basic_prop_4[PLM]: "[\<exists> (p::o) q . p \<noteq> q & Contingent p & Contingent q in v]" apply (rule_tac α="q0"in"\<exists>I", rule_tac α="q0-"in"\<exists>I") using thm_relation_negation_6 basic_prop_2 basic_prop_3 "&I"by simp
lemma four_distinct_props_1[PLM]: "[NonContingent (p::Π0) \<rightarrow> (\<not>(\<exists> q . Contingent q & q = p)) in v]" proof (rule CP) assume"[NonContingent p in v]" hence"[\<not>(Contingent p) in v]" unfolding NonContingent_def Contingent_def apply - by PLM_solver moreover { assume"[\<exists> q . Contingent q & q = p in v]" thenobtain r where"[Contingent r & r = p in v]" by (rule "\<exists>E") hence"[Contingent p in v]" using"&E" l_identity[axiom_instance, deduction, deduction] by blast
} ultimatelyshow"[\<not>(\<exists>q. Contingent q & q = p) in v]" using modus_tollens_1 CP by blast qed
lemma four_distinct_props_2[PLM]: "[Contingent (p::o) \<rightarrow> \<not>(\<exists> q . (NonContingent q & q = p)) in v]" proof (rule CP) assume"[Contingent p in v]" hence"[\<not>(NonContingent p) in v]" unfolding NonContingent_def Contingent_def apply - by PLM_solver moreover { assume"[\<exists> q . NonContingent q & q = p in v]" thenobtain r where"[NonContingent r & r = p in v]" by (rule "\<exists>E") hence"[NonContingent p in v]" using"&E" l_identity[axiom_instance, deduction, deduction] by blast
} ultimatelyshow"[\<not>(\<exists>q. NonContingent q & q = p) in v]" using modus_tollens_1 CP by blast qed
lemma four_distinct_props_4[PLM]: "[p0\<noteq> (p0-) & p0\<noteq> q0& p0\<noteq> (q0-) & (p0-) \<noteq> q0 & (p0-) \<noteq> (q0-) & q0\<noteq> (q0-) in v]" proof (rule "&I")+ show"[p0\<noteq> (p0-) in v]" by (rule thm_relation_negation_6) next
{ assume"[p0= q0 in v]" hence"[\<exists> q . NonContingent q & q = q0 in v]" using"&I" thm_noncont_propos_3 "\<exists>I"[where α=p0] by simp
} thus"[p0\<noteq> q0 in v]" using four_distinct_props_2[deduction, OF basic_prop_2]
modus_tollens_1 CP by blast next
{ assume"[p0= (q0-) in v]" hence"[\<exists> q . NonContingent q & q = (q0-) in v]" using thm_noncont_propos_3 "&I""\<exists>I"[where α=p0] by simp
} thus"[p0\<noteq> (q0-) in v]" using four_distinct_props_2[deduction, OF basic_prop_3]
modus_tollens_1 CP by blast next
{ assume"[(p0-) = q0 in v]" hence"[\<exists> q . NonContingent q & q = q0 in v]" using thm_noncont_propos_4 "&I""\<exists>I"[where α="p0-"] by auto
} thus"[(p0-) \<noteq> q0 in v]" using four_distinct_props_2[deduction, OF basic_prop_2]
modus_tollens_1 CP by blast next
{ assume"[(p0-) = (q0-) in v]" hence"[\<exists> q . NonContingent q & q = (q0-) in v]" using thm_noncont_propos_4 "&I""\<exists>I"[where α="p0-"] by auto
} thus"[(p0-) \<noteq> (q0-) in v]" using four_distinct_props_2[deduction, OF basic_prop_3]
modus_tollens_1 CP by blast next show"[q0\<noteq> (q0-) in v]" by (rule thm_relation_negation_6) qed
lemma cont_true_cont_1[PLM]: "[ContingentlyTrue p \<rightarrow> Contingent p in v]" apply (rule CP, rule thm_cont_propos_2[equiv_rl]) unfolding ContingentlyTrue_def apply (rule "&I", drule "&E"(1)) using"T\<diamond>"[deduction] apply simp by (rule "&E"(2))
lemma cont_true_cont_2[PLM]: "[ContingentlyFalse p \<rightarrow> Contingent p in v]" apply (rule CP, rule thm_cont_propos_2[equiv_rl]) unfolding ContingentlyFalse_def apply (rule "&I", drule "&E"(2)) apply simp apply (drule "&E"(1)) using"T\<diamond>"[deduction] by simp
lemma cont_true_cont_3[PLM]: "[ContingentlyTrue p \<equiv> ContingentlyFalse (p-) in v]" unfolding ContingentlyTrue_def ContingentlyFalse_def apply (PLM_subst_method "\<not>p""p-") using thm_relation_negation_3[equiv_sym] apply simp apply (PLM_subst_method "p""\<not>\<not>p") by PLM_solver+
lemma cont_true_cont_4[PLM]: "[ContingentlyFalse p \<equiv> ContingentlyTrue (p-) in v]" unfolding ContingentlyTrue_def ContingentlyFalse_def apply (PLM_subst_method "\<not>p""p-") using thm_relation_negation_3[equiv_sym] apply simp apply (PLM_subst_method "p""\<not>\<not>p") by PLM_solver+
lemma cont_tf_thm_1[PLM]: "[ContingentlyTrue q0\<or> ContingentlyFalse q0 in v]" proof - have"[q0\<or> \<not>q0 in v]" by PLM_solver moreover { assume"[q0 in v]" hence"[q0&\<diamond>\<not>q0 in v]" unfolding q0_def using qml_4[axiom_instance,conj2] "&I" by auto
} moreover { assume"[\<not>q0 in v]" hence"[(\<not>q0) &\<diamond>q0 in v]" unfolding q0_def using qml_4[axiom_instance,conj1] "&I" by auto
} ultimatelyshow ?thesis unfolding ContingentlyTrue_def ContingentlyFalse_def using"\<or>E"(4) CP by auto qed
lemma cont_tf_thm_2[PLM]: "[ContingentlyFalse q0\<or> ContingentlyFalse (q0-) in v]" using cont_tf_thm_1 cont_true_cont_3[where p="q0"]
cont_true_cont_4[where p="q0"] apply - by PLM_solver
lemma cont_tf_thm_3[PLM]: "[\<exists> p . ContingentlyTrue p in v]" proof (rule "\<or>E"(1); (rule CP)?) show"[ContingentlyTrue q0\<or> ContingentlyFalse q0 in v]" using cont_tf_thm_1 . next assume"[ContingentlyTrue q0 in v]" thus ?thesis using"\<exists>I"by metis next assume"[ContingentlyFalse q0 in v]" hence"[ContingentlyTrue (q0-) in v]" using cont_true_cont_4[equiv_lr] by simp thus ?thesis using"\<exists>I"by metis qed
lemma cont_tf_thm_4[PLM]: "[\<exists> p . ContingentlyFalse p in v]" proof (rule "\<or>E"(1); (rule CP)?) show"[ContingentlyTrue q0\<or> ContingentlyFalse q0 in v]" using cont_tf_thm_1 . next assume"[ContingentlyTrue q0 in v]" hence"[ContingentlyFalse (q0-) in v]" using cont_true_cont_3[equiv_lr] by simp thus ?thesis using"\<exists>I"by metis next assume"[ContingentlyFalse q0 in v]" thus ?thesis using"\<exists>I"by metis qed
lemma cont_tf_thm_5[PLM]: "[ContingentlyTrue p & Necessary q \<rightarrow> p \<noteq> q in v]" proof (rule CP) assume"[ContingentlyTrue p & Necessary q in v]" hence1: "[\<diamond>(\<not>p) &\<box> q in v]" unfolding ContingentlyTrue_def Necessary_defs using"&E""&I"by blast hence"[\<not>\<box>p in v]" apply - apply (drule "&E"(1)) unfolding diamond_def apply (PLM_subst_method "\<not>\<not>p""p") using oth_class_taut_4_b[equiv_sym] by auto moreover { assume"[p = q in v]" hence"[\<box>p in v]" using l_identity[where α="q"and β="p"and φ="λ x . \<box> x",
axiom_instance, deduction, deduction] 1[conj2] id_eq_prop_prop_8_b[deduction] by blast
} ultimatelyshow"[p \<noteq> q in v]" using modus_tollens_1 CP by blast qed
lemma cont_tf_thm_6[PLM]: "[(ContingentlyFalse p & Impossible q) \<rightarrow> p \<noteq> q in v]" proof (rule CP) assume"[ContingentlyFalse p & Impossible q in v]" hence1: "[\<diamond>p &\<box>(\<not>q) in v]" unfolding ContingentlyFalse_def Impossible_defs using"&E""&I"by blast hence"[\<not>\<diamond>q in v]" unfolding diamond_def apply - by PLM_solver moreover { assume"[p = q in v]" hence"[\<diamond>q in v]" using l_identity[axiom_instance, deduction, deduction] 1[conj1]
id_eq_prop_prop_8_b[deduction] by blast
} ultimatelyshow"[p \<noteq> q in v]" using modus_tollens_1 CP by blast qed end
lemma oa_contingent_1[PLM]: "[O! \<noteq> A! in v]" proof -
{ assume"[O! = A! in v]" hence"[(\<lambda>x. \<diamond>(E!,xP)) = (\<lambda>x. \<not>\<diamond>(E!,xP)) in v]" unfolding Ordinary_def Abstract_def . moreoverhave"[((\<lambda>x. \<diamond>(E!,xP)), xP)\<equiv> \<diamond>(E!,xP) in v]" apply (rule beta_C_meta_1) by show_proper ultimatelyhave"[((\<lambda>x. \<not>\<diamond>(E!,xP)), xP)\<equiv> \<diamond>(E!,xP) in v]" using l_identity[axiom_instance, deduction, deduction] by fast moreoverhave"[((\<lambda>x. \<not>\<diamond>(E!,xP)), xP)\<equiv> \<not>\<diamond>(E!,xP) in v]" apply (rule beta_C_meta_1) by show_proper ultimatelyhave"[\<diamond>(E!,xP)\<equiv> \<not>\<diamond>(E!,xP) in v]" apply - by PLM_solver
} thus ?thesis using oth_class_taut_1_b modus_tollens_1 CP by blast qed
lemma oa_contingent_2[PLM]: "[(O!,xP)\<equiv> \<not>(A!,xP) in v]" proof - have"[((\<lambda>x. \<not>\<diamond>(E!,xP)), xP)\<equiv> \<not>\<diamond>(E!,xP) in v]" apply (rule beta_C_meta_1) by show_proper hence"[(\<not>((\<lambda>x. \<not>\<diamond>(E!,xP)), xP)) \<equiv> \<diamond>(E!,xP) in v]" using oth_class_taut_5_d[equiv_lr] oth_class_taut_4_b[equiv_sym] "\<equiv>E"(5) by blast moreoverhave"[((\<lambda>x. \<diamond>(E!,xP)), xP)\<equiv> \<diamond>(E!,xP) in v]" apply (rule beta_C_meta_1) by show_proper ultimatelyshow ?thesis unfolding Ordinary_def Abstract_def apply - by PLM_solver qed
lemma oa_contingent_3[PLM]: "[(A!,xP)\<equiv> \<not>(O!,xP) in v]" using oa_contingent_2 apply - by PLM_solver
lemma oa_contingent_4[PLM]: "[Contingent O! in v]" apply (rule thm_cont_prop_2[equiv_rl], rule "&I") subgoal unfolding Ordinary_def apply (PLM_subst_method "λ x . \<diamond>(E!,xP)""λ x . (\<lambda>x. \<diamond>(E!,xP),xP)") apply (safe intro!: beta_C_meta_1[equiv_sym]) apply show_proper using"BF\<diamond>"[deduction, OF thm_cont_prop_2[equiv_lr, OF thm_cont_e_2, conj1]] by (rule "T\<diamond>"[deduction]) subgoal apply (PLM_subst_method "λ x . (A!,xP)""λ x . \<not>(O!,xP)") using oa_contingent_3 apply simp using cqt_further_5[deduction,conj1, OF A_objects[axiom_instance]] by (rule "T\<diamond>"[deduction]) done
lemma oa_contingent_5[PLM]: "[Contingent A! in v]" apply (rule thm_cont_prop_2[equiv_rl], rule "&I") subgoal using cqt_further_5[deduction,conj1, OF A_objects[axiom_instance]] by (rule "T\<diamond>"[deduction]) subgoal unfolding Abstract_def apply (PLM_subst_method "λ x . \<not>\<diamond>(E!,xP)""λ x . (\<lambda>x. \<not>\<diamond>(E!,xP),xP)") apply (safe intro!: beta_C_meta_1[equiv_sym]) apply show_proper apply (PLM_subst_method "λ x . \<diamond>(E!,xP)""λ x . \<not>\<not>\<diamond>(E!,xP)") using oth_class_taut_4_b apply simp using"BF\<diamond>"[deduction, OF thm_cont_prop_2[equiv_lr, OF thm_cont_e_2, conj1]] by (rule "T\<diamond>"[deduction]) done
lemma oa_contingent_6[PLM]: "[(O!-) \<noteq> (A!-) in v]" proof -
{ assume"[(O!-) = (A!-) in v]" hence"[(\<lambda>x. \<not>(O!,xP)) = (\<lambda>x. \<not>(A!,xP)) in v]" unfolding propnot_defs . moreoverhave"[((\<lambda>x. \<not>(O!,xP)), xP)\<equiv> \<not>(O!,xP) in v]" apply (rule beta_C_meta_1) by show_proper ultimatelyhave"[(\<lambda>x. \<not>(A!,xP),xP)\<equiv> \<not>(O!,xP) in v]" using l_identity[axiom_instance, deduction, deduction] by fast hence"[(\<not>(A!,xP)) \<equiv> \<not>(O!,xP) in v]" apply - apply (PLM_subst_method "(\<lambda>x. \<not>(A!,xP),xP)""(\<not>(A!,xP))") apply (safe intro!: beta_C_meta_1) by show_proper hence"[(O!,xP)\<equiv> \<not>(O!,xP) in v]" using oa_contingent_2 apply - by PLM_solver
} thus ?thesis using oth_class_taut_1_b modus_tollens_1 CP by blast qed
lemma oa_contingent_7[PLM]: "[(O!-,xP)\<equiv> \<not>(A!-,xP) in v]" proof - have"[(\<not>(\<lambda>x. \<not>(A!,xP),xP)) \<equiv> (A!,xP) in v]" apply (PLM_subst_method "(\<not>(A!,xP))""(\<lambda>x. \<not>(A!,xP),xP)") apply (safe intro!: beta_C_meta_1[equiv_sym]) apply show_proper using oth_class_taut_4_b[equiv_sym] by auto moreoverhave"[(\<lambda>x. \<not>(O!,xP),xP)\<equiv> \<not>(O!,xP) in v]" apply (rule beta_C_meta_1) by show_proper ultimatelyshow ?thesis unfolding propnot_defs using oa_contingent_3 apply - by PLM_solver qed
lemma oa_contingent_8[PLM]: "[Contingent (O!-) in v]" using oa_contingent_4 thm_cont_prop_3[equiv_lr] by auto
lemma oa_contingent_9[PLM]: "[Contingent (A!-) in v]" using oa_contingent_5 thm_cont_prop_3[equiv_lr] by auto
lemma oa_facts_1[PLM]: "[(O!,xP)\<rightarrow> \<box>(O!,xP) in v]" proof (rule CP) assume"[(O!,xP) in v]" hence"[\<diamond>(E!,xP) in v]" unfolding Ordinary_def apply - apply (rule beta_C_meta_1[equiv_lr]) by show_proper hence"[\<box>\<diamond>(E!,xP) in v]" using qml_3[axiom_instance, deduction] by auto thus"[\<box>(O!,xP) in v]" unfolding Ordinary_def apply - apply (PLM_subst_method "\<diamond>(E!,xP)""(\<lambda>x. \<diamond>(E!,xP),xP)") apply (safe intro!: beta_C_meta_1[equiv_sym]) by show_proper qed
lemma oa_facts_2[PLM]: "[(A!,xP)\<rightarrow> \<box>(A!,xP) in v]" proof (rule CP) assume"[(A!,xP) in v]" hence"[\<not>\<diamond>(E!,xP) in v]" unfolding Abstract_def apply - apply (rule beta_C_meta_1[equiv_lr]) by show_proper hence"[\<box>\<box>\<not>(E!,xP) in v]" using KBasic2_4[equiv_rl] "4\<box>"[deduction] by auto hence"[\<box>\<not>\<diamond>(E!,xP) in v]" apply - apply (PLM_subst_method "\<box>\<not>(E!,xP)""\<not>\<diamond>(E!,xP)") using KBasic2_4 by auto thus"[\<box>(A!,xP) in v]" unfolding Abstract_def apply - apply (PLM_subst_method "\<not>\<diamond>(E!,xP)""(\<lambda>x. \<not>\<diamond>(E!,xP),xP)") apply (safe intro!: beta_C_meta_1[equiv_sym]) by show_proper qed
lemma oa_facts_3[PLM]: "[\<diamond>(O!,xP)\<rightarrow> (O!,xP) in v]" using oa_facts_1 by (rule derived_S5_rules_2_b)
lemma oa_facts_4[PLM]: "[\<diamond>(A!,xP)\<rightarrow> (A!,xP) in v]" using oa_facts_2 by (rule derived_S5_rules_2_b)
lemma oa_facts_5[PLM]: "[\<diamond>(O!,xP)\<equiv> \<box>(O!,xP) in v]" using oa_facts_1[deduction, OF oa_facts_3[deduction]] "T\<diamond>"[deduction, OF qml_2[axiom_instance, deduction]] "\<equiv>I" CP by blast
lemma oa_facts_6[PLM]: "[\<diamond>(A!,xP)\<equiv> \<box>(A!,xP) in v]" using oa_facts_2[deduction, OF oa_facts_4[deduction]] "T\<diamond>"[deduction, OF qml_2[axiom_instance, deduction]] "\<equiv>I" CP by blast
lemma oa_facts_7[PLM]: "[(O!,xP)\<equiv> \<A>(O!,xP) in v]" apply (rule "\<equiv>I"; rule CP) apply (rule nec_imp_act[deduction, OF oa_facts_1[deduction]]; assumption) proof - assume"[\<A>(O!,xP) in v]" hence"[\<A>(\<diamond>(E!,xP)) in v]" unfolding Ordinary_def apply - apply (PLM_subst_method "(\<lambda>x. \<diamond>(E!,xP),xP)""\<diamond>(E!,xP)") apply (safe intro!: beta_C_meta_1) by show_proper hence"[\<diamond>(E!,xP) in v]" using Act_Basic_6[equiv_rl] by auto thus"[(O!,xP) in v]" unfolding Ordinary_def apply - apply (PLM_subst_method "\<diamond>(E!,xP)""(\<lambda>x. \<diamond>(E!,xP),xP)") apply (safe intro!: beta_C_meta_1[equiv_sym]) by show_proper qed
lemma oa_facts_8[PLM]: "[(A!,xP)\<equiv> \<A>(A!,xP) in v]" apply (rule "\<equiv>I"; rule CP) apply (rule nec_imp_act[deduction, OF oa_facts_2[deduction]]; assumption) proof - assume"[\<A>(A!,xP) in v]" hence"[\<A>(\<not>\<diamond>(E!,xP)) in v]" unfolding Abstract_def apply - apply (PLM_subst_method "(\<lambda>x. \<not>\<diamond>(E!,xP),xP)""\<not>\<diamond>(E!,xP)") apply (safe intro!: beta_C_meta_1) by show_proper hence"[\<A>(\<box>\<not>(E!,xP)) in v]" apply - apply (PLM_subst_method "(\<not>\<diamond>(E!,xP))""(\<box>\<not>(E!,xP))") using KBasic2_4[equiv_sym] by auto hence"[\<not>\<diamond>(E!,xP) in v]" using qml_act_2[axiom_instance, equiv_rl] KBasic2_4[equiv_lr] by auto thus"[(A!,xP) in v]" unfolding Abstract_def apply - apply (PLM_subst_method "\<not>\<diamond>(E!,xP)""(\<lambda>x. \<not>\<diamond>(E!,xP),xP)") apply (safe intro!: beta_C_meta_1[equiv_sym]) by show_proper qed
lemma cont_nec_fact1_1[PLM]: "[WeaklyContingent F \<equiv> WeaklyContingent (F-) in v]" proof (rule "\<equiv>I"; rule CP) assume"[WeaklyContingent F in v]" hence wc_def: "[Contingent F & (\<forall> x . (\<diamond>(F,xP)\<rightarrow> \<box>(F,xP))) in v]" unfolding WeaklyContingent_def . have"[Contingent (F-) in v]" using wc_def[conj1] by (rule thm_cont_prop_3[equiv_lr]) moreover {
{ fix x assume"[\<diamond>(F-,xP) in v]" hence"[\<not>\<box>(F,xP) in v]" unfolding diamond_def apply - apply (PLM_subst_method "\<not>(F-,xP)""(F,xP)") using thm_relation_negation_2_1 by auto moreover { assume"[\<not>\<box>(F-,xP) in v]" hence"[\<not>\<box>(\<lambda>x. \<not>(F,xP),xP) in v]" unfolding propnot_defs . hence"[\<diamond>(F,xP) in v]" unfolding diamond_def apply - apply (PLM_subst_method "(\<lambda>x. \<not>(F,xP),xP)""\<not>(F,xP)") apply (safe intro!: beta_C_meta_1) by show_proper hence"[\<box>(F,xP) in v]" using wc_def[conj2] cqt_1[axiom_instance, deduction]
modus_ponens by fast
} ultimatelyhave"[\<box>(F-, xP) in v]" using"\<not>\<not>E" modus_tollens_1 CP by blast
} hence"[\<forall> x . \<diamond>(F-,xP)\<rightarrow> \<box>(F-, xP) in v]" using"\<forall>I" CP by fast
} ultimatelyshow"[WeaklyContingent (F-) in v]" unfolding WeaklyContingent_def by (rule "&I") next assume"[WeaklyContingent (F-) in v]" hence wc_def: "[Contingent (F-) & (\<forall> x . (\<diamond>(F-,xP)\<rightarrow> \<box>(F-,xP))) in v]" unfolding WeaklyContingent_def . have"[Contingent F in v]" using wc_def[conj1] by (rule thm_cont_prop_3[equiv_rl]) moreover {
{ fix x assume"[\<diamond>(F,xP) in v]" hence"[\<not>\<box>(F-,xP) in v]" unfolding diamond_def apply - apply (PLM_subst_method "\<not>(F,xP)""(F-,xP)") using thm_relation_negation_1_1[equiv_sym] by auto moreover { assume"[\<not>\<box>(F,xP) in v]" hence"[\<diamond>(F-,xP) in v]" unfolding diamond_def apply - apply (PLM_subst_method "(F,xP)""\<not>(F-,xP)") using thm_relation_negation_2_1[equiv_sym] by auto hence"[\<box>(F-,xP) in v]" using wc_def[conj2] cqt_1[axiom_instance, deduction]
modus_ponens by fast
} ultimatelyhave"[\<box>(F, xP) in v]" using"\<not>\<not>E" modus_tollens_1 CP by blast
} hence"[\<forall> x . \<diamond>(F,xP)\<rightarrow> \<box>(F, xP) in v]" using"\<forall>I" CP by fast
} ultimatelyshow"[WeaklyContingent (F) in v]" unfolding WeaklyContingent_def by (rule "&I") qed
lemma cont_nec_fact1_2[PLM]: "[(WeaklyContingent F &\<not>(WeaklyContingent G)) \<rightarrow> (F \<noteq> G) in v]" using l_identity[axiom_instance,deduction,deduction] "&E""&I"
modus_tollens_1 CP by metis
lemma cont_nec_fact2_1[PLM]: "[WeaklyContingent (O!) in v]" unfolding WeaklyContingent_def apply (rule "&I") using oa_contingent_4 apply simp using oa_facts_5 unfolding equiv_def using"&E"(1) "\<forall>I"by fast
lemma cont_nec_fact2_2[PLM]: "[WeaklyContingent (A!) in v]" unfolding WeaklyContingent_def apply (rule "&I") using oa_contingent_5 apply simp using oa_facts_6 unfolding equiv_def using"&E"(1) "\<forall>I"by fast
lemma cont_nec_fact2_3[PLM]: "[\<not>(WeaklyContingent (E!)) in v]" proof (rule modus_tollens_1, rule CP) assume"[WeaklyContingent E! in v]" thus"[\<forall> x . \<diamond>(E!,xP)\<rightarrow> \<box>(E!,xP) in v]" unfolding WeaklyContingent_def using"&E"(2) by fast next
{ assume1: "[\<forall> x . \<diamond>(E!,xP)\<rightarrow> \<box>(E!,xP) in v]" have"[\<exists> x . \<diamond>((E!,xP)&\<diamond>(\<not>(E!,xP))) in v]" using qml_4[axiom_instance,conj1, THEN BFs_3[deduction]] . thenobtain x where"[\<diamond>((E!,xP)&\<diamond>(\<not>(E!,xP))) in v]" by (rule "\<exists>E") hence"[\<diamond>(E!,xP)&\<diamond>(\<not>(E!,xP)) in v]" using KBasic2_8[deduction] S5Basic_8[deduction] "&I""&E"by blast hence"[\<box>(E!,xP)& (\<not>\<box>(E!,xP)) in v]" using1[THEN"\<forall>E", deduction] "&E""&I"
KBasic2_2[equiv_rl] by blast hence"[\<not>(\<forall> x . \<diamond>(E!,xP)\<rightarrow> \<box>(E!,xP)) in v]" using oth_class_taut_1_a modus_tollens_1 CP by blast
} thus"[\<not>(\<forall> x . \<diamond>(E!,xP)\<rightarrow> \<box>(E!,xP)) in v]" using reductio_aa_2 if_p_then_p CP by meson qed
lemma cont_nec_fact2_4[PLM]: "[\<not>(WeaklyContingent (PLM.L)) in v]" proof -
{ assume"[WeaklyContingent PLM.L in v]" hence"[Contingent PLM.L in v]" unfolding WeaklyContingent_def using"&E"(1) by blast
} thus ?thesis using thm_noncont_e_e_3 unfolding Contingent_def NonContingent_def using modus_tollens_2 CP by blast qed
lemma cont_nec_fact2_5[PLM]: "[O! \<noteq> E! & O! \<noteq> (E!-) & O! \<noteq> PLM.L & O! \<noteq> (PLM.L-) in v]" proof ((rule "&I")+) show"[O! \<noteq> E! in v]" using cont_nec_fact2_1 cont_nec_fact2_3
cont_nec_fact1_2[deduction] "&I"by simp next have"[\<not>(WeaklyContingent (E!-)) in v]" using cont_nec_fact1_1[THEN oth_class_taut_5_d[equiv_lr], equiv_lr]
cont_nec_fact2_3 by auto thus"[O! \<noteq> (E!-) in v]" using cont_nec_fact2_1 cont_nec_fact1_2[deduction] "&I"by simp next show"[O! \<noteq> PLM.L in v]" using cont_nec_fact2_1 cont_nec_fact2_4
cont_nec_fact1_2[deduction] "&I"by simp next have"[\<not>(WeaklyContingent (PLM.L-)) in v]" using cont_nec_fact1_1[THEN oth_class_taut_5_d[equiv_lr], equiv_lr]
cont_nec_fact2_4 by auto thus"[O! \<noteq> (PLM.L-) in v]" using cont_nec_fact2_1 cont_nec_fact1_2[deduction] "&I"by simp qed
lemma cont_nec_fact2_6[PLM]: "[A! \<noteq> E! & A! \<noteq> (E!-) & A! \<noteq> PLM.L & A! \<noteq> (PLM.L-) in v]" proof ((rule "&I")+) show"[A! \<noteq> E! in v]" using cont_nec_fact2_2 cont_nec_fact2_3
cont_nec_fact1_2[deduction] "&I"by simp next have"[\<not>(WeaklyContingent (E!-)) in v]" using cont_nec_fact1_1[THEN oth_class_taut_5_d[equiv_lr], equiv_lr]
cont_nec_fact2_3 by auto thus"[A! \<noteq> (E!-) in v]" using cont_nec_fact2_2 cont_nec_fact1_2[deduction] "&I"by simp next show"[A! \<noteq> PLM.L in v]" using cont_nec_fact2_2 cont_nec_fact2_4
cont_nec_fact1_2[deduction] "&I"by simp next have"[\<not>(WeaklyContingent (PLM.L-)) in v]" using cont_nec_fact1_1[THEN oth_class_taut_5_d[equiv_lr],
equiv_lr] cont_nec_fact2_4 by auto thus"[A! \<noteq> (PLM.L-) in v]" using cont_nec_fact2_2 cont_nec_fact1_2[deduction] "&I"by simp qed
lemma id_nec3_1[PLM]: "[((xP) =E (yP)) \<equiv> (\<box>((xP) =E (yP))) in v]" proof (rule "\<equiv>I"; rule CP) assume"[(xP) =E (yP) in v]" hence"[(O!,xP) in v] ∧ [(O!,yP) in v] ∧ [\<box>(\<forall> F . (F,xP)\<equiv> (F,yP)) in v]" using eq_E_simple_1[equiv_lr] using"&E"by blast hence"[\<box>(O!,xP) in v] ∧ [\<box>(O!,yP) in v] ∧ [\<box>\<box>(\<forall> F . (F,xP)\<equiv> (F,yP)) in v]" using oa_facts_1[deduction] S5Basic_6[deduction] by blast hence"[\<box>((O!,xP)&(O!,yP)&\<box>(\<forall> F. (F,xP)\<equiv> (F,yP))) in v]" using"&I" KBasic_3[equiv_rl] by presburger thus"[\<box>((xP) =E (yP)) in v]" apply - apply (PLM_subst_method "((O!,xP)&(O!,yP)&\<box>(\<forall> F. (F,xP)\<equiv> (F,yP)))" "(xP) =E (yP)") using eq_E_simple_1[equiv_sym] by auto next assume"[\<box>((xP) =E (yP)) in v]" thus"[((xP) =E (yP)) in v]" using qml_2[axiom_instance,deduction] by simp qed
lemma id_nec3_2[PLM]: "[\<diamond>((xP) =E (yP)) \<equiv> ((xP) =E (yP)) in v]" proof (rule "\<equiv>I"; rule CP) assume"[\<diamond>((xP) =E (yP)) in v]" thus"[(xP) =E (yP) in v]" using derived_S5_rules_2_b[deduction] id_nec3_1[equiv_lr]
CP modus_ponens by blast next assume"[(xP) =E (yP) in v]" thus"[\<diamond>((xP) =E (yP)) in v]" by (rule TBasic[deduction]) qed
lemma thm_neg_eqE[PLM]: "[((xP) \<noteq>E (yP)) \<equiv> (\<not>((xP) =E (yP))) in v]" proof - have"[(xP) \<noteq>E (yP) in v] = [((\<lambda>2 (λ x y . (xP) =E (yP)))-, xP, yP) in v]" unfolding not_identicalE_defby simp alsohave"... = [\<not>((\<lambda>2 (λ x y . (xP) =E (yP))), xP, yP) in v]" unfolding propnot_defs apply (safe intro!: beta_C_meta_2[equiv_lr] beta_C_meta_2[equiv_rl]) by show_proper+ alsohave"... = [\<not>((xP) =E (yP)) in v]" apply (PLM_subst_method "((\<lambda>2 (λ x y . (xP) =E (yP))), xP, yP)" "(xP) =E (yP)") apply (safe intro!: beta_C_meta_2) unfolding identity_defs by show_proper finallyshow ?thesis using"\<equiv>I" CP by presburger qed
lemma id_nec4_1[PLM]: "[((xP) \<noteq>E (yP)) \<equiv> \<box>((xP) \<noteq>E (yP)) in v]" proof - have"[(\<not>((xP) =E (yP))) \<equiv> \<box>(\<not>((xP) =E (yP))) in v]" using id_nec3_2[equiv_sym] oth_class_taut_5_d[equiv_lr]
KBasic2_4[equiv_sym] intro_elim_6_e by fast thus ?thesis apply - apply (PLM_subst_method "(\<not>((xP) =E (yP)))""(xP) \<noteq>E (yP)") using thm_neg_eqE[equiv_sym] by auto qed
lemma id_act_1[PLM]: "[((xP) =E (yP)) \<equiv> (\<A>((xP) =E (yP))) in v]" proof (rule "\<equiv>I"; rule CP) assume"[(xP) =E (yP) in v]" hence"[\<box>((xP) =E (yP)) in v]" using id_nec3_1[equiv_lr] by auto thus"[\<A>((xP) =E (yP)) in v]" using nec_imp_act[deduction] by fast next assume"[\<A>((xP) =E (yP)) in v]" hence"[\<A>((O!,xP)&(O!,yP)&\<box>(\<forall> F . (F,xP)\<equiv> (F,yP))) in v]" apply - apply (PLM_subst_method "(xP) =E (yP)" "((O!,xP)&(O!,yP)&\<box>(\<forall> F . (F,xP)\<equiv> (F,yP)))") using eq_E_simple_1 by auto hence"[\<A>(O!,xP)&\<A>(O!,yP)&\<A>(\<box>(\<forall> F . (F,xP)\<equiv> (F,yP))) in v]" using Act_Basic_2[equiv_lr] "&I""&E"by meson thus"[(xP) =E (yP) in v]" apply - apply (rule eq_E_simple_1[equiv_rl]) using oa_facts_7[equiv_rl] qml_act_2[axiom_instance, equiv_rl] "&I""&E"by meson qed
lemma id_act_2[PLM]: "[((xP) \<noteq>E (yP)) \<equiv> (\<A>((xP) \<noteq>E (yP))) in v]" apply (PLM_subst_method "(\<not>((xP) =E (yP)))""((xP) \<noteq>E (yP))") using thm_neg_eqE[equiv_sym] apply simp using id_act_1 oth_class_taut_5_d[equiv_lr] thm_neg_eqE intro_elim_6_e
logic_actual_nec_1[axiom_instance,equiv_sym] by meson
end
class id_act = id_eq + assumes id_act_prop: "[\<A>(α = β) in v] ==> [(α = β) in v]"
instantiation ν :: id_act begin instanceproof interpret PLM . fix x::ν and y::ν and v::i assume"[\<A>(x = y) in v]" hence"[\<A>(((xP) =E (yP)) \<or> ((A!,xP)&(A!,yP) &\<box>(\<forall> F . {xP,F}\<equiv> {yP,F}))) in v]" unfolding identity_defs by auto hence"[\<A>(((xP) =E (yP))) \<or> \<A>(((A!,xP)&(A!,yP) &\<box>(\<forall> F . {xP,F}\<equiv> {yP,F}))) in v]" using Act_Basic_10[equiv_lr] by auto moreover { assume"[\<A>(((xP) =E (yP))) in v]" hence"[(xP) = (yP) in v]" using id_act_1[equiv_rl] eq_E_simple_2[deduction] by auto
} moreover { assume"[\<A>((A!,xP)&(A!,yP)&\<box>(\<forall> F . {xP,F}\<equiv> {yP,F})) in v]" hence"[\<A>(A!,xP)&\<A>(A!,yP)&\<A>(\<box>(\<forall> F . {xP,F}\<equiv> {yP,F})) in v]" using Act_Basic_2[equiv_lr] "&I""&E"by meson hence"[(A!,xP)&(A!,yP)& (\<box>(\<forall> F . {xP,F}\<equiv> {yP,F})) in v]" using oa_facts_8[equiv_rl] qml_act_2[axiom_instance,equiv_rl] "&I""&E"by meson hence"[(xP) = (yP) in v]" unfolding identity_defs using"\<or>I"by auto
} ultimatelyhave"[(xP) = (yP) in v]" using intro_elim_4_a CP by meson thus"[x = y in v]" unfolding identity_defs by auto qed end
instantiation Π1 :: id_act begin instanceproof interpret PLM . fix F::Π1and G::Π1and v::i show"[\<A>(F = G) in v] ==> [(F = G) in v]" unfolding identity_defs using qml_act_2[axiom_instance,equiv_rl] by auto qed end
instantiationo :: id_act begin instanceproof interpret PLM . fix p :: oand q :: oand v::i show"[\<A>(p = q) in v] ==> [p = q in v]" unfolding identity\<o>_defusing id_act_prop by blast qed end
instantiation Π2 :: id_act begin instanceproof interpret PLM . fix F::Π2and G::Π2and v::i assume a: "[\<A>(F = G) in v]"
{ fix x have"[\<A>((\<lambda>y. (F,xP,yP)) = (\<lambda>y. (G,xP,yP)) & (\<lambda>y. (F,yP,xP)) = (\<lambda>y. (G,yP,xP))) in v]" using a logic_actual_nec_3[axiom_instance, equiv_lr] cqt_basic_4[equiv_lr] "\<forall>E" unfolding identity2_defby fast hence"[((\<lambda>y. (F,xP,yP)) = (\<lambda>y. (G,xP,yP))) & ((\<lambda>y. (F,yP,xP)) = (\<lambda>y. (G,yP,xP))) in v]" using"&I""&E" id_act_prop Act_Basic_2[equiv_lr] by metis
} thus"[F = G in v]"unfolding identity_defs by (rule "\<forall>I") qed end
instantiation Π3 :: id_act begin instanceproof interpret PLM . fix F::Π3and G::Π3and v::i assume a: "[\<A>(F = G) in v]" let ?p = "λ x y . (\<lambda>z. (F,zP,xP,yP)) = (\<lambda>z. (G,zP,xP,yP)) & (\<lambda>z. (F,xP,zP,yP)) = (\<lambda>z. (G,xP,zP,yP)) & (\<lambda>z. (F,xP,yP,zP)) = (\<lambda>z. (G,xP,yP,zP))"
{ fix x
{ fix y have"[\<A>(?p x y) in v]" using a logic_actual_nec_3[axiom_instance, equiv_lr]
cqt_basic_4[equiv_lr] "\<forall>E"[where 'a=ν] unfolding identity3_defby blast hence"[?p x y in v]" using"&I""&E" id_act_prop Act_Basic_2[equiv_lr] by metis
} hence"[\<forall> y . ?p x y in v]" by (rule "\<forall>I")
} thus"[F = G in v]" unfolding identity3_defby (rule "\<forall>I") qed end
context PLM begin lemma id_act_3[PLM]: "[((α::('a::id_act)) = β) \<equiv> \<A>(α = β) in v]" using"\<equiv>I" CP id_nec[equiv_lr, THEN nec_imp_act[deduction]]
id_act_prop by metis
lemma id_act_4[PLM]: "[((α::('a::id_act)) \<noteq> β) \<equiv> \<A>(α \<noteq> β) in v]" using id_act_3[THEN oth_class_taut_5_d[equiv_lr]]
logic_actual_nec_1[axiom_instance, equiv_sym]
intro_elim_6_e by blast
lemma id_act_desc[PLM]: "[(yP) = (\<iota>x . x = y) in v]" using descriptions[axiom_instance,equiv_rl]
id_act_3[equiv_sym] "\<forall>I"by fast
lemma eta_conversion_lemma_1[PLM]: "[(\<lambda> x . (F,xP)) = F in v]" using lambda_predicates_3_1[axiom_instance] .
lemma eta_conversion_lemma_0[PLM]: "[(\<lambda>0 p) = p in v]" using lambda_predicates_3_0[axiom_instance] .
lemma eta_conversion_lemma_2[PLM]: "[(\<lambda>2 (λ x y . (F,xP,yP))) = F in v]" using lambda_predicates_3_2[axiom_instance] .
lemma eta_conversion_lemma_3[PLM]: "[(\<lambda>3 (λ x y z . (F,xP,yP,zP))) = F in v]" using lambda_predicates_3_3[axiom_instance] .
lemma lambda_p_q_p_eq_q[PLM]: "[((\<lambda>0 p) = (\<lambda>0 q)) \<equiv> (p = q) in v]" using eta_conversion_lemma_0
l_identity[axiom_instance, deduction, deduction]
eta_conversion_lemma_0[eq_sym] "\<equiv>I" CP by metis
subsection‹The Theory of Objects› text‹\label{TAO_PLM_Objects}›
lemma partition_1[PLM]: "[\<forall> x . (O!,xP)\<or> (A!,xP) in v]" proof (rule "\<forall>I") fix x have"[\<diamond>(E!,xP)\<or> \<not>\<diamond>(E!,xP) in v]" by PLM_solver moreoverhave"[\<diamond>(E!,xP)\<equiv> (\<lambda> y . \<diamond>(E!,yP), xP) in v]" apply (rule beta_C_meta_1[equiv_sym]) by show_proper moreoverhave"[(\<not>\<diamond>(E!,xP)) \<equiv> (\<lambda> y . \<not>\<diamond>(E!,yP), xP) in v]" apply (rule beta_C_meta_1[equiv_sym]) by show_proper ultimatelyshow"[(O!, xP)\<or> (A!, xP) in v]" unfolding Ordinary_def Abstract_def by PLM_solver qed
lemma partition_2[PLM]: "[\<not>(\<exists> x . (O!,xP)&(A!,xP)) in v]" proof -
{ assume"[\<exists> x . (O!,xP)&(A!,xP) in v]" thenobtain b where"[(O!,bP)&(A!,bP) in v]" by (rule "\<exists>E") hence ?thesis using"&E" oa_contingent_2[equiv_lr]
reductio_aa_2 by fast
} thus ?thesis using reductio_aa_2 by blast qed
lemma ord_eq_Eequiv_1[PLM]: "[(O!,x)\<rightarrow> (x =E x) in v]" proof (rule CP) assume"[(O!,x) in v]" moreoverhave"[\<box>(\<forall> F . (F,x)\<equiv> (F,x)) in v]" by PLM_solver ultimatelyshow"[(x) =E (x) in v]" using"&I" eq_E_simple_1[equiv_rl] by blast qed
lemma ord_eq_Eequiv_2[PLM]: "[(x =E y) \<rightarrow> (y =E x) in v]" proof (rule CP) assume"[x =E y in v]" hence1: "[(O!,x)&(O!,y)&\<box>(\<forall> F . (F,x)\<equiv> (F,y)) in v]" using eq_E_simple_1[equiv_lr] by simp have"[\<box>(\<forall> F . (F,y)\<equiv> (F,x)) in v]" apply (PLM_subst_method "λ F . (F,x)\<equiv> (F,y)" "λ F . (F,y)\<equiv> (F,x)") using oth_class_taut_3_g 1[conj2] by auto thus"[y =E x in v]" using eq_E_simple_1[equiv_rl] 1[conj1] "&E""&I"by meson qed
lemma ord_eq_Eequiv_3[PLM]: "[((x =E y) & (y =E z)) \<rightarrow> (x =E z) in v]" proof (rule CP) assume a: "[(x =E y) & (y =E z) in v]" have"[\<box>((\<forall> F . (F,x)\<equiv> (F,y)) & (\<forall> F . (F,y)\<equiv> (F,z))) in v]" using KBasic_3[equiv_rl] a[conj1, THEN eq_E_simple_1[equiv_lr,conj2]]
a[conj2, THEN eq_E_simple_1[equiv_lr,conj2]] "&I"by blast moreover {
{ fix w have"[((\<forall> F . (F,x)\<equiv> (F,y)) & (\<forall> F . (F,y)\<equiv> (F,z))) \<rightarrow> (\<forall> F . (F,x)\<equiv> (F,z)) in w]" by PLM_solver
} hence"[\<box>(((\<forall> F . (F,x)\<equiv> (F,y)) & (\<forall> F . (F,y)\<equiv> (F,z))) \<rightarrow> (\<forall> F . (F,x)\<equiv> (F,z))) in v]" by (rule RN)
} ultimatelyhave"[\<box>(\<forall> F . (F,x)\<equiv> (F,z)) in v]" using qml_1[axiom_instance,deduction,deduction] by blast thus"[x =E z in v]" using a[conj1, THEN eq_E_simple_1[equiv_lr,conj1,conj1]] using a[conj2, THEN eq_E_simple_1[equiv_lr,conj1,conj2]]
eq_E_simple_1[equiv_rl] "&I" by presburger qed
lemma ord_eq_E_eq[PLM]: "[((O!,xP)\<or> (O!,yP)) \<rightarrow> ((xP= yP) \<equiv> (xP=E yP)) in v]" proof (rule CP) assume"[(O!,xP)\<or> (O!,yP) in v]" moreover { assume"[(O!,xP) in v]" hence"[(xP= yP) \<equiv> (xP=E yP) in v]" using"\<equiv>I" CP l_identity[axiom_instance, deduction, deduction]
ord_eq_Eequiv_1[deduction] eq_E_simple_2[deduction] by metis
} moreover { assume"[(O!,yP) in v]" hence"[(xP= yP) \<equiv> (xP=E yP) in v]" using"\<equiv>I" CP l_identity[axiom_instance, deduction, deduction]
ord_eq_Eequiv_1[deduction] eq_E_simple_2[deduction] id_eq_2[deduction]
ord_eq_Eequiv_2[deduction] identity_ν_defby metis
} ultimatelyshow"[(xP= yP) \<equiv> (xP=E yP) in v]" using intro_elim_4_a CP by blast qed
lemma ord_eq_E[PLM]: "[((O!,xP)&(O!,yP)) \<rightarrow> ((\<forall> F . (F,xP)\<equiv> (F,yP)) \<rightarrow> xP=E yP) in v]" proof (rule CP; rule CP) assume ord_xy: "[(O!,xP)&(O!,yP) in v]" assume"[\<forall> F . (F,xP)\<equiv> (F,yP) in v]" hence"[(\<lambda> z . zP=E xP, xP)\<equiv> (\<lambda> z . zP=E xP, yP) in v]" by (rule "\<forall>E") moreoverhave"[(\<lambda> z . zP=E xP, xP) in v]" apply (rule beta_C_meta_1[equiv_rl]) unfolding identityE_infix_def apply show_proper using ord_eq_Eequiv_1[deduction] ord_xy[conj1] unfolding identityE_infix_defby simp ultimatelyhave"[(\<lambda> z . zP=E xP, yP) in v]" using"\<equiv>E"by blast hence"[yP=E xP in v]" unfolding identityE_infix_def apply (safe intro!:
beta_C_meta_1[where φ = "λ z . (basic_identityE,z,xP)", equiv_lr]) by show_proper thus"[xP=E yP in v]" by (rule ord_eq_Eequiv_2[deduction]) qed
lemma ord_eq_E2[PLM]: "[((O!,xP)&(O!,yP)) \<rightarrow> ((xP\<noteq> yP) \<equiv> (\<lambda>z . zP=E xP) \<noteq> (\<lambda>z . zP=E yP)) in v]" proof (rule CP; rule "\<equiv>I"; rule CP) assume ord_xy: "[(O!,xP)&(O!,yP) in v]" assume"[xP\<noteq> yP in v]" hence"[\<not>(xP=E yP) in v]" using eq_E_simple_2 modus_tollens_1 by fast moreover { assume"[(\<lambda>z . zP=E xP) = (\<lambda>z . zP=E yP) in v]" moreoverhave"[(\<lambda>z . zP=E xP, xP) in v]" apply (rule beta_C_meta_1[equiv_rl]) unfolding identityE_infix_def apply show_proper using ord_eq_Eequiv_1[deduction] ord_xy[conj1] unfolding identityE_infix_defby presburger ultimatelyhave"[(\<lambda>z . zP=E yP, xP) in v]" using l_identity[axiom_instance, deduction, deduction] by fast hence"[xP=E yP in v]" unfolding identityE_infix_def apply (safe intro!:
beta_C_meta_1[where φ = "λ z . (basic_identityE,z,yP)", equiv_lr]) by show_proper
} ultimatelyshow"[(\<lambda>z . zP=E xP) \<noteq> (\<lambda>z . zP=E yP) in v]" using modus_tollens_1 CP by blast next assume ord_xy: "[(O!,xP)&(O!,yP) in v]" assume"[(\<lambda>z . zP=E xP) \<noteq> (\<lambda>z . zP=E yP) in v]" moreover { assume"[xP= yP in v]" hence"[(\<lambda>z . zP=E xP) = (\<lambda>z . zP=E yP) in v]" using id_eq_1 l_identity[axiom_instance, deduction, deduction] by fast
} ultimatelyshow"[xP\<noteq> yP in v]" using modus_tollens_1 CP by blast qed
lemma ab_obey_1[PLM]: "[((A!,xP)&(A!,yP)) \<rightarrow> ((\<forall> F . {xP, F}\<equiv> {yP, F}) \<rightarrow> xP= yP) in v]" proof(rule CP; rule CP) assume abs_xy: "[(A!,xP)&(A!,yP) in v]" assume enc_equiv: "[\<forall> F . {xP, F}\<equiv> {yP, F} in v]"
{ fix P have"[{xP, P}\<equiv> {yP, P} in v]" using enc_equiv by (rule "\<forall>E") hence"[\<box>({xP, P}\<equiv> {yP, P}) in v]" using en_eq_2 intro_elim_6_e intro_elim_6_f
en_eq_5[equiv_rl] by meson
} hence"[\<box>(\<forall> F . {xP, F}\<equiv> {yP, F}) in v]" using BF[deduction] "\<forall>I"by fast thus"[xP= yP in v]" unfolding identity_defs using"\<or>I"(2) abs_xy "&I"by presburger qed
lemma ab_obey_2[PLM]: "[((A!,xP)&(A!,yP)) \<rightarrow> ((\<exists> F . {xP, F}&\<not>{yP, F}) \<rightarrow> xP\<noteq> yP) in v]" proof(rule CP; rule CP) assume abs_xy: "[(A!,xP)&(A!,yP) in v]" assume"[\<exists> F . {xP, F}&\<not>{yP, F} in v]" thenobtain P where P_prop: "[{xP, P}&\<not>{yP, P} in v]" by (rule "\<exists>E")
{ assume"[xP= yP in v]" hence"[{xP, P}\<equiv> {yP, P} in v]" using l_identity[axiom_instance, deduction, deduction]
oth_class_taut_4_a by fast hence"[{yP, P} in v]" using P_prop[conj1] by (rule "\<equiv>E")
} thus"[xP\<noteq> yP in v]" using P_prop[conj2] modus_tollens_1 CP by blast qed
lemma ordnecfail[PLM]: "[(O!,xP)\<rightarrow> \<box>(\<not>(\<exists> F . {xP, F})) in v]" proof (rule CP) assume"[(O!,xP) in v]" hence"[\<box>(O!,xP) in v]" using oa_facts_1[deduction] by simp moreoverhence"[\<box>((O!,xP)\<rightarrow> (\<not>(\<exists> F . {xP, F}))) in v]" using nocoder[axiom_necessitation, axiom_instance] by simp ultimatelyshow"[\<box>(\<not>(\<exists> F . {xP, F})) in v]" using qml_1[axiom_instance, deduction, deduction] by fast qed
lemma o_objects_exist_1[PLM]: "[\<diamond>(\<exists> x . (E!,xP)) in v]" proof - have"[\<diamond>(\<exists> x . (E!,xP)&\<diamond>(\<not>(E!,xP))) in v]" using qml_4[axiom_instance, conj1] . hence"[\<diamond>((\<exists> x . (E!,xP)) & (\<exists> x . \<diamond>(\<not>(E!,xP)))) in v]" using sign_S5_thm_3[deduction] by fast hence"[\<diamond>(\<exists> x . (E!,xP)) &\<diamond>(\<exists> x . \<diamond>(\<not>(E!,xP))) in v]" using KBasic2_8[deduction] by blast thus ?thesis using"&E"by blast qed
lemma o_objects_exist_2[PLM]: "[\<box>(\<exists> x . (O!,xP)) in v]" apply (rule RN) unfolding Ordinary_def apply (PLM_subst_method "λ x . \<diamond>(E!,xP)""λ x . (\<lambda>y. \<diamond>(E!,yP), xP)") apply (safe intro!: beta_C_meta_1[equiv_sym]) apply show_proper using o_objects_exist_1 "BF\<diamond>"[deduction] by blast
lemma o_objects_exist_3[PLM]: "[\<box>(\<not>(\<forall> x . (A!,xP))) in v]" apply (PLM_subst_method "(\<exists>x. \<not>(A!,xP))""\<not>(\<forall>x. (A!,xP))") using cqt_further_2[equiv_sym] apply fast apply (PLM_subst_method "λ x . (O!,xP)""λ x . \<not>(A!,xP)") using oa_contingent_2 o_objects_exist_2 by auto
lemma a_objects_exist_1[PLM]: "[\<box>(\<exists> x . (A!,xP)) in v]" proof -
{ fix v have"[\<exists> x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> (F = F)) in v]" using A_objects[axiom_instance] by simp hence"[\<exists> x . (A!,xP) in v]" using cqt_further_5[deduction,conj1] by fast
} thus ?thesis by (rule RN) qed
lemma a_objects_exist_2[PLM]: "[\<box>(\<not>(\<forall> x . (O!,xP))) in v]" apply (PLM_subst_method "(\<exists>x. \<not>(O!,xP))""\<not>(\<forall>x. (O!,xP))") using cqt_further_2[equiv_sym] apply fast apply (PLM_subst_method "λ x . (A!,xP)""λ x . \<not>(O!,xP)") using oa_contingent_3 a_objects_exist_1 by auto
lemma a_objects_exist_3[PLM]: "[\<box>(\<not>(\<forall> x . (E!,xP))) in v]" proof -
{ fix v have"[\<exists> x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> (F = F)) in v]" using A_objects[axiom_instance] by simp hence"[\<exists> x . (A!,xP) in v]" using cqt_further_5[deduction,conj1] by fast thenobtain a where "[(A!,aP) in v]" by (rule "\<exists>E") hence"[\<not>(\<diamond>(E!,aP)) in v]" unfolding Abstract_def apply (safe intro!: beta_C_meta_1[equiv_lr]) by show_proper hence"[(\<not>(E!,aP)) in v]" using KBasic2_4[equiv_rl] qml_2[axiom_instance,deduction] by simp hence"[\<not>(\<forall> x . (E!,xP)) in v]" using"\<exists>I" cqt_further_2[equiv_rl] by fast
} thus ?thesis by (rule RN) qed
lemma encoders_are_abstract[PLM]: "[(\<exists> F . {xP, F}) \<rightarrow> (A!,xP) in v]" using nocoder[axiom_instance] contraposition_2
oa_contingent_2[THEN oth_class_taut_5_d[equiv_lr], equiv_lr]
useful_tautologies_1[deduction]
vdash_properties_10 CP by metis
lemma A_objects_unique[PLM]: "[\<exists>! x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F) in v]" proof - have"[\<exists> x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F) in v]" using A_objects[axiom_instance] by simp thenobtain a where a_prop: "[(A!,aP)& (\<forall> F . {aP, F}\<equiv> φ F) in v]"by (rule "\<exists>E") moreoverhave"[\<forall> y . (A!,yP)& (\<forall> F . {yP, F}\<equiv> φ F) \<rightarrow> (y = a) in v]" proof (rule "\<forall>I"; rule CP) fix b assume b_prop: "[(A!,bP)& (\<forall> F . {bP, F}\<equiv> φ F) in v]"
{ fix P have"[{bP,P}\<equiv> {aP, P} in v]" using a_prop[conj2] b_prop[conj2] "\<equiv>I""\<equiv>E"(1) "\<equiv>E"(2)
CP vdash_properties_10 "\<forall>E"by metis
} hence"[\<forall> F . {bP,F}\<equiv> {aP, F} in v]" using"\<forall>I"by fast thus"[b = a in v]" unfolding identity_ν_def using ab_obey_1[deduction, deduction]
a_prop[conj1] b_prop[conj1] "&I"by blast qed ultimatelyshow ?thesis unfolding exists_unique_def using"&I""\<exists>I"by fast qed
lemma obj_oth_1[PLM]: "[\<exists>! x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> (F, yP)) in v]" using A_objects_unique .
lemma obj_oth_2[PLM]: "[\<exists>! x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> ((F, yP)&(F, zP))) in v]" using A_objects_unique .
lemma obj_oth_3[PLM]: "[\<exists>! x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> ((F, yP)\<or> (F, zP))) in v]" using A_objects_unique .
lemma obj_oth_4[PLM]: "[\<exists>! x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> (\<box>(F, yP))) in v]" using A_objects_unique .
lemma obj_oth_5[PLM]: "[\<exists>! x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> (F = G)) in v]" using A_objects_unique .
lemma obj_oth_6[PLM]: "[\<exists>! x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> \<box>(\<forall> y . (G, yP)\<rightarrow> (F, yP))) in v]" using A_objects_unique .
lemma A_Exists_1[PLM]: "[\<A>(\<exists>! x :: ('a :: id_act) . φ x) \<equiv> (\<exists>! x . \<A>(φ x)) in v]" unfolding exists_unique_def proof (rule "\<equiv>I"; rule CP) assume"[\<A>(\<exists>α. φ α & (\<forall>β. φ β \<rightarrow> β = α)) in v]" hence"[\<exists>α. \<A>(φ α & (\<forall>β. φ β \<rightarrow> β = α)) in v]" using Act_Basic_11[equiv_lr] by blast thenobtain α where "[\<A>(φ α & (\<forall>β. φ β \<rightarrow> β = α)) in v]" by (rule "\<exists>E") hence1: "[\<A>(φ α) &\<A>(\<forall>β. φ β \<rightarrow> β = α) in v]" using Act_Basic_2[equiv_lr] by blast have2: "[\<forall>β. \<A>(φ β \<rightarrow> β = α) in v]" using1[conj2] logic_actual_nec_3[axiom_instance, equiv_lr] by blast
{ fix β have"[\<A>(φ β \<rightarrow> β = α) in v]" using2by (rule "\<forall>E") hence"[\<A>(φ β) \<rightarrow> (β = α) in v]" using logic_actual_nec_2[axiom_instance, equiv_lr, deduction]
id_act_3[equiv_rl] CP by blast
} hence"[\<forall> β . \<A>(φ β) \<rightarrow> (β = α) in v]" by (rule "\<forall>I") thus"[\<exists>α. \<A>φ α & (\<forall>β. \<A>φ β \<rightarrow> β = α) in v]" using1[conj1] "&I""\<exists>I"by fast next assume"[\<exists>α. \<A>φ α & (\<forall>β. \<A>φ β \<rightarrow> β = α) in v]" thenobtain α where1: "[\<A>φ α & (\<forall>β. \<A>φ β \<rightarrow> β = α) in v]" by (rule "\<exists>E")
{ fix β have"[\<A>(φ β) \<rightarrow> β = α in v]" using1[conj2] by (rule "\<forall>E") hence"[\<A>(φ β \<rightarrow> β = α) in v]" using logic_actual_nec_2[axiom_instance, equiv_rl] id_act_3[equiv_lr]
vdash_properties_10 CP by blast
} hence"[\<forall> β . \<A>(φ β \<rightarrow> β = α) in v]" by (rule "\<forall>I") hence"[\<A>(\<forall> β . φ β \<rightarrow> β = α) in v]" using logic_actual_nec_3[axiom_instance, equiv_rl] by fast hence"[\<A>(φ α & (\<forall> β . φ β \<rightarrow> β = α)) in v]" using1[conj1] Act_Basic_2[equiv_rl] "&I"by blast hence"[\<exists>α. \<A>(φ α & (\<forall>β. φ β \<rightarrow> β = α)) in v]" using"\<exists>I"by fast thus"[\<A>(\<exists>α. φ α & (\<forall>β. φ β \<rightarrow> β = α)) in v]" using Act_Basic_11[equiv_rl] by fast qed
lemma A_Exists_2[PLM]: "[(\<exists> y . yP= (\<iota>x . φ x)) \<equiv> \<A>(\<exists>!x . φ x) in v]" using actual_desc_1 A_Exists_1[equiv_sym]
intro_elim_6_e by blast
lemma A_descriptions[PLM]: "[\<exists> y . yP= (\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F)) in v]" using A_objects_unique[THEN RN, THEN nec_imp_act[deduction]]
A_Exists_2[equiv_rl] by auto
lemma thm_can_terms2[PLM]: "[(yP= (\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F))) \<rightarrow> ((A!,yP)& (\<forall> F . {yP,F}\<equiv> φ F)) in dw]" using y_in_2 by auto
lemma can_ab2[PLM]: "[(yP= (\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F))) \<rightarrow> (A!,yP) in v]" proof (rule CP) assume"[yP= (\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F)) in v]" hence"[\<A>(A!,yP)&\<A>(\<forall> F . {yP,F}\<equiv> φ F) in v]" using nec_hintikka_scheme[equiv_lr, conj1]
Act_Basic_2[equiv_lr] by blast thus"[(A!,yP) in v]" using oa_facts_8[equiv_rl] "&E"by blast qed
lemma desc_encode[PLM]: "[{\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F), G}\<equiv> φ G in dw]" proof - obtain a where "[aP= (\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F)) in dw]" using A_descriptions by (rule "\<exists>E") moreoverhence"[{aP, G}\<equiv> φ G in dw]" using hintikka[equiv_lr, conj1] "&E""\<forall>E"by fast ultimatelyshow ?thesis using l_identity[axiom_instance, deduction, deduction] by fast qed
lemma desc_nec_encode[PLM]: "[{\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F), G}\<equiv> \<A>(φ G) in v]" proof - obtain a where "[aP= (\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F)) in v]" using A_descriptions by (rule "\<exists>E") moreover { hence"[\<A>((A!,aP)& (\<forall> F . {aP,F}\<equiv> φ F)) in v]" using nec_hintikka_scheme[equiv_lr, conj1] by fast hence"[\<A>(\<forall> F . {aP,F}\<equiv> φ F) in v]" using Act_Basic_2[equiv_lr,conj2] by blast hence"[\<forall> F . \<A>( {aP,F}\<equiv> φ F) in v]" using logic_actual_nec_3[axiom_instance, equiv_lr] by blast hence"[\<A>({aP, G}\<equiv> φ G) in v]" using"\<forall>E"by fast hence"[\<A>{aP, G}\<equiv> \<A>(φ G) in v]" using Act_Basic_5[equiv_lr] by fast hence"[{aP, G}\<equiv> \<A>(φ G) in v]" using en_eq_10[equiv_sym] intro_elim_6_e by blast
} ultimatelyshow ?thesis using l_identity[axiom_instance, deduction, deduction] by fast qed
notepad begin fix v let ?x = "\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> (\<exists> q . q & F = (\<lambda> y . q)))" have"[\<box>(\<exists> p . ContingentlyTrue p) in v]" using cont_tf_thm_3 RN by auto hence"[\<A>(\<exists> p . ContingentlyTrue p) in v]" using nec_imp_act[deduction] by simp hence"[\<exists> p . \<A>(ContingentlyTrue p) in v]" using Act_Basic_11[equiv_lr] by auto thenobtain p1where "[\<A>(ContingentlyTrue p1) in v]" by (rule "\<exists>E") hence"[\<A>p1 in v]" unfolding ContingentlyTrue_def using Act_Basic_2[equiv_lr] "&E"by fast hence"[\<A>p1&\<A>((\<lambda> y . p1) = (\<lambda> y . p1)) in v]" using"&I" id_eq_1[THEN RN, THEN nec_imp_act[deduction]] by fast hence"[\<A>(p1& (\<lambda> y . p1) = (\<lambda> y . p1)) in v]" using Act_Basic_2[equiv_rl] by fast hence"[\<exists> q . \<A>( q & (\<lambda> y . p1) = (\<lambda> y . q)) in v]" using"\<exists>I"by fast hence"[\<A>(\<exists> q . q & (\<lambda> y . p1) = (\<lambda> y . q)) in v]" using Act_Basic_11[equiv_rl] by fast moreoverhave"[{?x, \<lambda> y . p1}\<equiv> \<A>(\<exists> q . q & (\<lambda> y . p1) = (\<lambda> y . q)) in v]" using desc_nec_encode by fast ultimatelyhave"[{?x, \<lambda> y . p1} in v]" using"\<equiv>E"by blast end
lemma Box_desc_encode_1[PLM]: "[\<box>(φ G) \<rightarrow> {(\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)), G} in v]" proof (rule CP) assume"[\<box>(φ G) in v]" hence"[\<A>(φ G) in v]" using nec_imp_act[deduction] by auto thus"[{\<iota>x . (A!,xP)& (\<forall> F . {xP,F}\<equiv> φ F), G} in v]" using desc_nec_encode[equiv_rl] by simp qed
lemma Box_desc_encode_2[PLM]: "[\<box>(φ G) \<rightarrow> \<box>({(\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)), G}\<equiv> φ G) in v]" proof (rule CP) assume a: "[\<box>(φ G) in v]" hence"[\<box>({(\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)), G}\<rightarrow> φ G) in v]" using KBasic_1[deduction] by simp moreover { have"[{(\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)), G} in v]" using a Box_desc_encode_1[deduction] by auto hence"[\<box>{(\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)), G} in v]" using encoding[axiom_instance,deduction] by blast hence"[\<box>(φ G \<rightarrow> {(\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)), G}) in v]" using KBasic_1[deduction] by simp
} ultimatelyshow"[\<box>({(\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)), G} \<equiv> φ G) in v]" using"&I" KBasic_4[equiv_rl] by blast qed
lemma box_phi_a_1[PLM]: assumes"[\<box>(\<forall> F . φ F \<rightarrow> \<box>(φ F)) in v]" shows"[((A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)) \<rightarrow> \<box>((A!,xP) & (\<forall> F . {xP, F}\<equiv> φ F)) in v]" proof (rule CP) assume a: "[((A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)) in v]" have"[\<box>(A!,xP) in v]" using oa_facts_2[deduction] a[conj1] by auto moreoverhave"[\<box>(\<forall> F . {xP, F}\<equiv> φ F) in v]" proof (rule BF[deduction]; rule "\<forall>I") fix F have θ: "[\<box>(φ F \<rightarrow> \<box>(φ F)) in v]" using assms[THEN CBF[deduction]] by (rule "\<forall>E") moreoverhave"[\<box>({xP, F}\<rightarrow> \<box>{xP, F}) in v]" using encoding[axiom_necessitation, axiom_instance] by simp moreoverhave"[\<box>{xP, F}\<equiv> \<box>(φ F) in v]" proof (rule "\<equiv>I"; rule CP) assume"[\<box>{xP, F} in v]" hence"[{xP, F} in v]" using qml_2[axiom_instance, deduction] by blast hence"[φ F in v]" using a[conj2] "\<forall>E"[where 'a=Π1] "\<equiv>E"by blast thus"[\<box>(φ F) in v]" using θ[THEN qml_2[axiom_instance, deduction], deduction] by simp next assume"[\<box>(φ F) in v]" hence"[φ F in v]" using qml_2[axiom_instance, deduction] by blast hence"[{xP, F} in v]" using a[conj2] "\<forall>E"[where 'a=Π1] "\<equiv>E"by blast thus"[\<box>{xP, F} in v]" using encoding[axiom_instance, deduction] by simp qed ultimatelyshow"[\<box>({xP,F}\<equiv> φ F) in v]" using sc_eq_box_box_3[deduction, deduction] "&I"by blast qed ultimatelyshow"[\<box>((A!,xP)& (\<forall>F. {xP,F}\<equiv> φ F)) in v]" using"&I" KBasic_3[equiv_rl] by blast qed
lemma box_phi_a_2[PLM]: assumes"[\<box>(\<forall> F . φ F \<rightarrow> \<box>(φ F)) in v]" shows"[yP= (\<iota>x . (A!,xP)& (\<forall> F. {xP, F}\<equiv> φ F)) \<rightarrow> ((A!,yP)& (\<forall> F . {yP, F}\<equiv> φ F)) in v]" proof - let ?ψ = "λ x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)" have"[\<forall> x . ?ψ x \<rightarrow> \<box>(?ψ x) in v]" using box_phi_a_1[OF assms] "\<forall>I"by fast hence"[(\<exists>! x . ?ψ x) \<rightarrow> (\<forall> y . yP= (\<iota>x . ?ψ x) \<rightarrow> ?ψ y) in v]" using unique_box_desc[deduction] by fast hence"[(\<forall> y . yP= (\<iota>x . ?ψ x) \<rightarrow> ?ψ y) in v]" using A_objects_unique modus_ponens by blast thus ?thesis by (rule "\<forall>E") qed
lemma box_phi_a_3[PLM]: assumes"[\<box>(\<forall> F . φ F \<rightarrow> \<box>(φ F)) in v]" shows"[{\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F), G}\<equiv> φ G in v]" proof - obtain a where "[aP= (\<iota>x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> φ F)) in v]" using A_descriptions by (rule "\<exists>E") moreover { hence"[(\<forall> F . {aP, F}\<equiv> φ F) in v]" using box_phi_a_2[OF assms, deduction, conj2] by blast hence"[{aP, G}\<equiv> φ G in v]"by (rule "\<forall>E")
} ultimatelyshow ?thesis using l_identity[axiom_instance, deduction, deduction] by fast qed
lemma null_uni_uniq_1[PLM]: "[\<exists>! x . Null (xP) in v]" proof - have"[\<exists> x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> (F \<noteq> F)) in v]" using A_objects[axiom_instance] by simp thenobtain a where a_prop: "[(A!,aP)& (\<forall> F . {aP, F}\<equiv> (F \<noteq> F)) in v]" by (rule "\<exists>E") have1: "[(A!,aP)& (\<not>(\<exists> F . {aP, F})) in v]" using a_prop[conj1] apply (rule "&I") proof -
{ assume"[\<exists> F . {aP, F} in v]" thenobtain P where "[{aP, P} in v]"by (rule "\<exists>E") hence"[P \<noteq> P in v]" using a_prop[conj2, THEN"\<forall>E", equiv_lr] by simp hence"[\<not>(\<exists> F . {aP, F}) in v]" using id_eq_1 reductio_aa_1 by fast
} thus"[\<not>(\<exists> F . {aP, F}) in v]" using reductio_aa_1 by blast qed moreoverhave"[\<forall> y . ((A!,yP)& (\<not>(\<exists> F . {yP, F}))) \<rightarrow> y = a in v]" proof (rule "\<forall>I"; rule CP) fix y assume2: "[(A!,yP)& (\<not>(\<exists> F . {yP, F})) in v]" have"[\<forall> F . {yP, F}\<equiv> {aP, F} in v]" using cqt_further_12[deduction] 1[conj2] 2[conj2] "&I"by blast thus"[y = a in v]" using ab_obey_1[deduction, deduction] "&I"[OF 2[conj1] 1[conj1]] identity_ν_defby presburger qed ultimatelyshow ?thesis using"&I""\<exists>I" unfolding Null_def exists_unique_def by fast qed
lemma null_uni_uniq_2[PLM]: "[\<exists>! x . Universal (xP) in v]" proof - have"[\<exists> x . (A!,xP)& (\<forall> F . {xP, F}\<equiv> (F = F)) in v]" using A_objects[axiom_instance] by simp thenobtain a where a_prop: "[(A!,aP)& (\<forall> F . {aP, F}\<equiv> (F = F)) in v]" by (rule "\<exists>E") have1: "[(A!,aP)& (\<forall> F . {aP, F}) in v]" using a_prop[conj1] apply (rule "&I") using"\<forall>I" a_prop[conj2, THEN"\<forall>E", equiv_rl] id_eq_1 by fast moreoverhave"[\<forall> y . ((A!,yP)& (\<forall> F . {yP, F})) \<rightarrow> y = a in v]" proof (rule "\<forall>I"; rule CP) fix y assume2: "[(A!,yP)& (\<forall> F . {yP, F}) in v]" have"[\<forall> F . {yP, F}\<equiv> {aP, F} in v]" using cqt_further_11[deduction] 1[conj2] 2[conj2] "&I"by blast thus"[y = a in v]" using ab_obey_1[deduction, deduction] "&I"[OF 2[conj1] 1[conj1]] identity_ν_def by presburger qed ultimatelyshow ?thesis using"&I""\<exists>I" unfolding Universal_def exists_unique_def by fast qed
lemma null_uni_uniq_3[PLM]: "[\<exists> y . yP= (\<iota>x . Null (xP)) in v]" using null_uni_uniq_1[THEN RN, THEN nec_imp_act[deduction]]
A_Exists_2[equiv_rl] by auto
lemma null_uni_uniq_4[PLM]: "[\<exists> y . yP= (\<iota>x . Universal (xP)) in v]" using null_uni_uniq_2[THEN RN, THEN nec_imp_act[deduction]]
A_Exists_2[equiv_rl] by auto
lemma null_uni_facts_1[PLM]: "[Null (xP) \<rightarrow> \<box>(Null (xP)) in v]" proof (rule CP) assume"[Null (xP) in v]" hence1: "[(A!,xP)& (\<not>(\<exists> F . {xP,F})) in v]" unfolding Null_def . have"[\<box>(A!,xP) in v]" using1[conj1] oa_facts_2[deduction] by simp moreoverhave"[\<box>(\<not>(\<exists> F . {xP,F})) in v]" proof -
{ assume"[\<not>\<box>(\<not>(\<exists> F . {xP,F})) in v]" hence"[\<diamond>(\<exists> F . {xP,F}) in v]" unfolding diamond_def . hence"[\<exists> F . \<diamond>{xP,F} in v]" using"BF\<diamond>"[deduction] by blast thenobtain P where"[\<diamond>{xP,P} in v]" by (rule "\<exists>E") hence"[{xP, P} in v]" using en_eq_3[equiv_lr] by simp hence"[\<exists> F . {xP, F} in v]" using"\<exists>I"by fast
} thus ?thesis using1[conj2] modus_tollens_1 CP
useful_tautologies_1[deduction] by metis qed ultimatelyshow"[\<box>Null (xP) in v]" unfolding Null_def using"&I" KBasic_3[equiv_rl] by blast qed
lemma null_uni_facts_2[PLM]: "[Universal (xP) \<rightarrow> \<box>(Universal (xP)) in v]" proof (rule CP) assume"[Universal (xP) in v]" hence1: "[(A!,xP)& (\<forall> F . {xP,F}) in v]" unfolding Universal_def . have"[\<box>(A!,xP) in v]" using1[conj1] oa_facts_2[deduction] by simp moreoverhave"[\<box>(\<forall> F . {xP,F}) in v]" proof (rule BF[deduction]; rule "\<forall>I") fix F have"[{xP, F} in v]" using1[conj2] by (rule "\<forall>E") thus"[\<box>{xP, F} in v]" using encoding[axiom_instance, deduction] by auto qed ultimatelyshow"[\<box>Universal (xP) in v]" unfolding Universal_def using"&I" KBasic_3[equiv_rl] by blast qed
lemma null_uni_facts_3[PLM]: "[Null (a\<emptyset>) in v]" proof - let ?ψ = "λ x . Null x" have"[((\<exists>! x . ?ψ (xP)) \<rightarrow> (\<forall> y . yP= (\<iota>x . ?ψ (xP))\<rightarrow> ?ψ (yP))) in v]" using unique_box_desc[deduction] null_uni_facts_1[THEN"\<forall>I"] by fast have1: "[(\<forall> y . yP= (\<iota>x . ?ψ (xP)) \<rightarrow> ?ψ (yP)) in v]" using unique_box_desc[deduction, deduction] null_uni_uniq_1
null_uni_facts_1[THEN"\<forall>I"] by fast have"[\<exists> y . yP= (a\<emptyset>) in v]" unfolding NullObject_def using null_uni_uniq_3 . thenobtain y where"[yP= (a\<emptyset>) in v]" by (rule "\<exists>E") moreoverhence"[?ψ (yP) in v]" using1[THEN"\<forall>E", deduction] unfolding NullObject_def by simp ultimatelyshow"[?ψ (a\<emptyset>) in v]" using l_identity[axiom_instance, deduction, deduction] by blast qed
lemma null_uni_facts_4[PLM]: "[Universal (aV) in v]" proof - let ?ψ = "λ x . Universal x" have"[((\<exists>! x . ?ψ (xP)) \<rightarrow> (\<forall> y . yP= (\<iota>x . ?ψ (xP))\<rightarrow> ?ψ (yP))) in v]" using unique_box_desc[deduction] null_uni_facts_2[THEN"\<forall>I"] by fast have1: "[(\<forall> y . yP= (\<iota>x . ?ψ (xP)) \<rightarrow> ?ψ (yP)) in v]" using unique_box_desc[deduction, deduction] null_uni_uniq_2
null_uni_facts_2[THEN"\<forall>I"] by fast have"[\<exists> y . yP= (aV) in v]" unfolding UniversalObject_def using null_uni_uniq_4 . thenobtain y where"[yP= (aV) in v]" by (rule "\<exists>E") moreoverhence"[?ψ (yP) in v]" using1[THEN"\<forall>E", deduction] unfolding UniversalObject_def by simp ultimatelyshow"[?ψ (aV) in v]" using l_identity[axiom_instance, deduction, deduction] by blast qed
lemma aclassical_1[PLM]: "[\<forall> R . \<exists> x y . (A!,xP)&(A!,yP)& (x \<noteq> y) & (\<lambda> z . (R,zP,xP)) = (\<lambda> z . (R,zP,yP)) in v]" proof (rule "\<forall>I") fix R obtain a where θ: "[(A!,aP)& (\<forall> F . {aP, F}\<equiv> (\<exists> y . (A!,yP) & F = (\<lambda> z . (R,zP,yP)) &\<not>{yP, F})) in v]" using A_objects[axiom_instance] by (rule "\<exists>E")
{ assume"[\<not>{aP, (\<lambda> z . (R,zP,aP))} in v]" hence"[\<not>((A!,aP)& (\<lambda> z . (R,zP,aP)) = (\<lambda> z . (R,zP,aP)) &\<not>{aP, (\<lambda> z . (R,zP,aP))}) in v]" using θ[conj2, THEN"\<forall>E", THEN oth_class_taut_5_d[equiv_lr], equiv_lr]
cqt_further_4[equiv_lr] "\<forall>E"by fast hence"[(A!,aP)& (\<lambda> z . (R,zP,aP)) = (\<lambda> z . (R,zP,aP)) \<rightarrow> {aP, (\<lambda> z . (R,zP,aP))} in v]" apply - by PLM_solver hence"[{aP, (\<lambda> z . (R,zP,aP))} in v]" using θ[conj1] id_eq_1 "&I" vdash_properties_10 by fast
} hence1: "[{aP, (\<lambda> z . (R,zP,aP))} in v]" using reductio_aa_1 CP if_p_then_p by blast thenobtain b where ξ: "[(A!,bP)& (\<lambda> z . (R,zP,aP)) = (\<lambda> z . (R,zP,bP)) &\<not>{bP, (\<lambda> z . (R,zP,aP))} in v]" using θ[conj2, THEN"\<forall>E", equiv_lr] "\<exists>E"by blast have"[a \<noteq> b in v]" proof -
{ assume"[a = b in v]" hence"[{bP, (\<lambda> z . (R,zP,aP))} in v]" using1 l_identity[axiom_instance, deduction, deduction] by fast hence ?thesis using ξ[conj2] reductio_aa_1 by blast
} thus ?thesis using reductio_aa_1 by blast qed hence"[(A!,aP)&(A!,bP)& a \<noteq> b & (\<lambda> z . (R,zP,aP)) = (\<lambda> z . (R,zP,bP)) in v]" using θ[conj1] ξ[conj1, conj1] ξ[conj1, conj2] "&I"by presburger hence"[\<exists> y . (A!,aP)&(A!,yP)& a \<noteq> y & (\<lambda>z. (R,zP,aP)) = (\<lambda>z. (R,zP,yP)) in v]" using"\<exists>I"by fast thus"[\<exists> x y . (A!,xP)&(A!,yP)& x \<noteq> y & (\<lambda>z. (R,zP,xP)) = (\<lambda>z. (R,zP,yP)) in v]" using"\<exists>I"by fast qed
lemma aclassical_2[PLM]: "[\<forall> R . \<exists> x y . (A!,xP)&(A!,yP)& (x \<noteq> y) & (\<lambda> z . (R,xP,zP)) = (\<lambda> z . (R,yP,zP)) in v]" proof (rule "\<forall>I") fix R obtain a where θ: "[(A!,aP)& (\<forall> F . {aP, F}\<equiv> (\<exists> y . (A!,yP) & F = (\<lambda> z . (R,yP,zP)) &\<not>{yP, F})) in v]" using A_objects[axiom_instance] by (rule "\<exists>E")
{ assume"[\<not>{aP, (\<lambda> z . (R,aP,zP))} in v]" hence"[\<not>((A!,aP)& (\<lambda> z . (R,aP,zP)) = (\<lambda> z . (R,aP,zP)) &\<not>{aP, (\<lambda> z . (R,aP,zP))}) in v]" using θ[conj2, THEN"\<forall>E", THEN oth_class_taut_5_d[equiv_lr], equiv_lr]
cqt_further_4[equiv_lr] "\<forall>E"by fast hence"[(A!,aP)& (\<lambda> z . (R,aP,zP)) = (\<lambda> z . (R,aP,zP)) \<rightarrow> {aP, (\<lambda> z . (R,aP,zP))} in v]" apply - by PLM_solver hence"[{aP, (\<lambda> z . (R,aP,zP))} in v]" using θ[conj1] id_eq_1 "&I" vdash_properties_10 by fast
} hence1: "[{aP, (\<lambda> z . (R,aP,zP))} in v]" using reductio_aa_1 CP if_p_then_p by blast thenobtain b where ξ: "[(A!,bP)& (\<lambda> z . (R,aP,zP)) = (\<lambda> z . (R,bP,zP)) &\<not>{bP, (\<lambda> z . (R,aP,zP))} in v]" using θ[conj2, THEN"\<forall>E", equiv_lr] "\<exists>E"by blast have"[a \<noteq> b in v]" proof -
{ assume"[a = b in v]" hence"[{bP, (\<lambda> z . (R,aP,zP))} in v]" using1 l_identity[axiom_instance, deduction, deduction] by fast hence ?thesis using ξ[conj2] reductio_aa_1 by blast
} thus ?thesis using ξ[conj2] reductio_aa_1 by blast qed hence"[(A!,aP)&(A!,bP)& a \<noteq> b & (\<lambda> z . (R,aP,zP)) = (\<lambda> z . (R,bP,zP)) in v]" using θ[conj1] ξ[conj1, conj1] ξ[conj1, conj2] "&I"by presburger hence"[\<exists> y . (A!,aP)&(A!,yP)& a \<noteq> y & (\<lambda>z. (R,aP,zP)) = (\<lambda>z. (R,yP,zP)) in v]" using"\<exists>I"by fast thus"[\<exists> x y . (A!,xP)&(A!,yP)& x \<noteq> y & (\<lambda>z. (R,xP,zP)) = (\<lambda>z. (R,yP,zP)) in v]" using"\<exists>I"by fast qed
lemma aclassical_3[PLM]: "[\<forall> F . \<exists> x y . (A!,xP)&(A!,yP)& (x \<noteq> y) & ((\<lambda>0(F,xP)) = (\<lambda>0(F,yP))) in v]" proof (rule "\<forall>I") fix R obtain a where θ: "[(A!,aP)& (\<forall> F . {aP, F}\<equiv> (\<exists> y . (A!,yP) & F = (\<lambda> z . (R,yP)) &\<not>{yP, F})) in v]" using A_objects[axiom_instance] by (rule "\<exists>E")
{ assume"[\<not>{aP, (\<lambda> z . (R,aP))} in v]" hence"[\<not>((A!,aP)& (\<lambda> z . (R,aP)) = (\<lambda> z . (R,aP)) &\<not>{aP, (\<lambda> z . (R,aP))}) in v]" using θ[conj2, THEN"\<forall>E", THEN oth_class_taut_5_d[equiv_lr], equiv_lr]
cqt_further_4[equiv_lr] "\<forall>E"by fast hence"[(A!,aP)& (\<lambda> z . (R,aP)) = (\<lambda> z . (R,aP)) \<rightarrow> {aP, (\<lambda> z . (R,aP))} in v]" apply - by PLM_solver hence"[{aP, (\<lambda> z . (R,aP))} in v]" using θ[conj1] id_eq_1 "&I" vdash_properties_10 by fast
} hence1: "[{aP, (\<lambda> z . (R,aP))} in v]" using reductio_aa_1 CP if_p_then_p by blast thenobtain b where ξ: "[(A!,bP)& (\<lambda> z . (R,aP)) = (\<lambda> z . (R,bP)) &\<not>{bP, (\<lambda> z . (R,aP))} in v]" using θ[conj2, THEN"\<forall>E", equiv_lr] "\<exists>E"by blast have"[a \<noteq> b in v]" proof -
{ assume"[a = b in v]" hence"[{bP, (\<lambda> z . (R,aP))} in v]" using1 l_identity[axiom_instance, deduction, deduction] by fast hence ?thesis using ξ[conj2] reductio_aa_1 by blast
} thus ?thesis using reductio_aa_1 by blast qed moreover { have"[(R,aP)=(R,bP) in v]" unfolding identity\<o>_def using ξ[conj1, conj2] by auto hence"[(\<lambda>0(R,aP)) = (\<lambda>0(R,bP)) in v]" using lambda_p_q_p_eq_q[equiv_rl] by simp
} ultimatelyhave"[(A!,aP)&(A!,bP)& a \<noteq> b & ((\<lambda>0(R,aP)) =(\<lambda>0(R,bP))) in v]" using θ[conj1] ξ[conj1, conj1] ξ[conj1, conj2] "&I" by presburger hence"[\<exists> y . (A!,aP)&(A!,yP)& a \<noteq> y & (\<lambda>0(R,aP)) = (\<lambda>0(R,yP)) in v]" using"\<exists>I"by fast thus"[\<exists> x y . (A!,xP)&(A!,yP)& x \<noteq> y & (\<lambda>0(R,xP)) = (\<lambda>0(R,yP)) in v]" using"\<exists>I"by fast qed
lemma aclassical2[PLM]: "[\<exists> x y . (A!,xP)&(A!,yP)& x \<noteq> y & (\<forall> F . (F,xP)\<equiv> (F,yP)) in v]" proof - let ?R1 = "\<lambda>2 (λ x y . \<forall> F . (F,xP)\<equiv> (F,yP))" have"[\<exists> x y . (A!,xP)&(A!,yP)& x \<noteq> y & (\<lambda>z. (?R1,zP,xP)) = (\<lambda>z. (?R1,zP,yP)) in v]" using aclassical_1 by (rule "\<forall>E") thenobtain a where "[\<exists> y . (A!,aP)&(A!,yP)& a \<noteq> y & (\<lambda>z. (?R1,zP,aP)) = (\<lambda>z. (?R1,zP,yP)) in v]" by (rule "\<exists>E") thenobtain b where ab_prop: "[(A!,aP)&(A!,bP)& a \<noteq> b & (\<lambda>z. (?R1,zP,aP)) = (\<lambda>z. (?R1,zP,bP)) in v]" by (rule "\<exists>E") have"[(?R1, aP, aP) in v]" apply (rule beta_C_meta_2[equiv_rl]) apply show_proper using oth_class_taut_4_a[THEN"\<forall>I"] by fast hence"[(\<lambda> z . (?R1, zP, aP), aP) in v]" apply - apply (rule beta_C_meta_1[equiv_rl]) apply show_proper by auto hence"[(\<lambda> z . (?R1, zP, bP), aP) in v]" using ab_prop[conj2] l_identity[axiom_instance, deduction, deduction] by fast hence"[(?R1, aP, bP) in v]" apply (safe intro!: beta_C_meta_1[where φ= "λz . (\<lambda>2 (λx y. \<forall>F. (F,xP)\<equiv> (F,yP)),z,bP)", equiv_lr]) by show_proper moreoverhave"IsProperInXY (λx y. \<forall>F. (F,x)\<equiv> (F,y))" by show_proper ultimatelyhave"[\<forall>F. (F,aP)\<equiv> (F,bP) in v]" using beta_C_meta_2[equiv_lr] by blast hence"[(A!,aP)&(A!,bP)& a \<noteq> b & (\<forall>F. (F,aP)\<equiv> (F,bP)) in v]" using ab_prop[conj1] "&I"by presburger hence"[\<exists> y . (A!,aP)&(A!,yP)& a \<noteq> y & (\<forall>F. (F,aP)\<equiv>(F,yP)) in v]" using"\<exists>I"by fast thus ?thesis using"\<exists>I"by fast qed
lemma prop_prop2_1: "[\<forall> p . \<exists> F . F = (\<lambda> x . p) in v]" proof (rule "\<forall>I") fix p have"[(\<lambda> x . p) = (\<lambda> x . p) in v]" using id_eq_prop_prop_1 by auto thus"[\<exists> F . F = (\<lambda> x . p) in v]" by PLM_solver qed
lemma prop_prop2_2: "[F = (\<lambda> x . p) \<rightarrow> \<box>(\<forall> x . (F,xP)\<equiv> p) in v]" proof (rule CP) assume1: "[F = (\<lambda> x . p) in v]"
{ fix v
{ fix x have"[((\<lambda> x . p), xP)\<equiv> p in v]" apply (rule beta_C_meta_1) by show_proper
} hence"[\<forall> x . ((\<lambda> x . p), xP)\<equiv> p in v]" by (rule "\<forall>I")
} hence"[\<box>(\<forall> x . ((\<lambda> x . p), xP)\<equiv> p) in v]" by (rule RN) thus"[\<box>(\<forall>x. (F,xP)\<equiv> p) in v]" using l_identity[axiom_instance,deduction,deduction,
OF 1[THEN id_eq_prop_prop_2[deduction]]] by fast qed
lemma prop_prop2_3: "[Propositional F \<rightarrow> \<box>(Propositional F) in v]" proof (rule CP) assume"[Propositional F in v]" hence"[\<exists> p . F = (\<lambda> x . p) in v]" unfolding Propositional_def . thenobtain q where"[F = (\<lambda> x . q) in v]" by (rule "\<exists>E") hence"[\<box>(F = (\<lambda> x . q)) in v]" using id_nec[equiv_lr] by auto hence"[\<exists> p . \<box>(F = (\<lambda> x . p)) in v]" using"\<exists>I"by fast thus"[\<box>(Propositional F) in v]" unfolding Propositional_def using sign_S5_thm_1[deduction] by fast qed
lemma prop_indis: "[Indiscriminate F \<rightarrow> (\<not>(\<exists> x y . (F,xP)& (\<not>(F,yP)))) in v]" proof (rule CP) assume"[Indiscriminate F in v]" hence1: "[\<box>((\<exists>x. (F,xP)) \<rightarrow> (\<forall>x. (F,xP))) in v]" unfolding Indiscriminate_def .
{ assume"[\<exists> x y . (F,xP)&\<not>(F,yP) in v]" thenobtain x where"[\<exists> y . (F,xP)&\<not>(F,yP) in v]" by (rule "\<exists>E") thenobtain y where2: "[(F,xP)&\<not>(F,yP) in v]" by (rule "\<exists>E") hence"[\<exists> x . (F, xP) in v]" using"&E"(1) "\<exists>I"by fast hence"[\<forall> x . (F,xP) in v]" using1[THEN qml_2[axiom_instance, deduction], deduction] by fast hence"[(F,yP) in v]" using cqt_orig_1[deduction] by fast hence"[(F,yP)& (\<not>(F,yP)) in v]" using2"&I""&E"by fast hence"[\<not>(\<exists> x y . (F,xP)&\<not>(F,yP)) in v]" using pl_1[axiom_instance, deduction, THEN modus_tollens_1]
oth_class_taut_1_a by blast
} thus"[\<not>(\<exists> x y . (F,xP)&\<not>(F,yP)) in v]" using reductio_aa_2 if_p_then_p deduction_theorem by blast qed
lemma prop_in_thm: "[Propositional F \<rightarrow> Indiscriminate F in v]" proof (rule CP) assume"[Propositional F in v]" hence"[\<box>(Propositional F) in v]" using prop_prop2_3[deduction] by auto moreover { fix w assume"[\<exists> p . (F = (\<lambda> y . p)) in w]" thenobtain q where q_prop: "[F = (\<lambda> y . q) in w]" by (rule "\<exists>E")
{ assume"[\<exists> x . (F,xP) in w]" thenobtain a where"[(F,aP) in w]" by (rule "\<exists>E") hence"[(\<lambda> y . q, aP) in w]" using q_prop l_identity[axiom_instance,deduction,deduction] by fast hence q: "[q in w]" apply (safe intro!: beta_C_meta_1[where φ="λy. q", equiv_lr]) apply show_proper by simp
{ fix x have"[(\<lambda> y . q, xP) in w]" apply (safe intro!: q beta_C_meta_1[equiv_rl]) by show_proper hence"[(F,xP) in w]" using q_prop[eq_sym] l_identity[axiom_instance, deduction, deduction] by fast
} hence"[\<forall> x . (F,xP) in w]" by (rule "\<forall>I")
} hence"[(\<exists> x . (F,xP)) \<rightarrow> (\<forall> x . (F, xP)) in w]" by (rule CP)
} ultimatelyshow"[Indiscriminate F in v]" unfolding Propositional_def Indiscriminate_def using RM_1[deduction] deduction_theorem by blast qed
lemma prop_in_f_1: "[Necessary F \<rightarrow> Indiscriminate F in v]" unfolding Necessary_defs Indiscriminate_def using pl_1[axiom_instance, THEN RM_1] by simp
lemma prop_in_f_2: "[Impossible F \<rightarrow> Indiscriminate F in v]" proof -
{ fix w have"[(\<not>(\<exists> x . (F,xP))) \<rightarrow> ((\<exists> x . (F,xP)) \<rightarrow> (\<forall> x . (F,xP))) in w]" using useful_tautologies_3 by auto hence"[(\<forall> x . \<not>(F,xP)) \<rightarrow> ((\<exists> x . (F,xP)) \<rightarrow> (\<forall> x . (F,xP))) in w]" apply - apply (PLM_subst_method "\<not>(\<exists> x. (F,xP))""(\<forall> x. \<not>(F,xP))") using cqt_further_4 unfolding exists_def by fast+
} thus ?thesis unfolding Impossible_defs Indiscriminate_def using RM_1 CP by blast qed
lemma prop_in_f_3_a: "[\<not>(Indiscriminate (E!)) in v]" proof (rule reductio_aa_2) show"[\<box>\<not>(\<forall>x. (E!,xP)) in v]" using a_objects_exist_3 . next assume"[Indiscriminate E! in v]" thus"[\<not>\<box>\<not>(\<forall> x . (E!,xP)) in v]" unfolding Indiscriminate_def using o_objects_exist_1 KBasic2_5[deduction,deduction] unfolding diamond_def by blast qed
lemma prop_in_f_3_b: "[\<not>(Indiscriminate (E!-)) in v]" proof (rule reductio_aa_2) assume"[Indiscriminate (E!-) in v]" moreoverhave"[\<box>(\<exists> x . (E!-, xP)) in v]" apply (PLM_subst_method "λ x . \<not>(E!, xP)""λ x . (E!-, xP)") using thm_relation_negation_1_1[equiv_sym] apply simp unfolding exists_def apply (PLM_subst_method "λ x . (E!, xP)""λ x . \<not>\<not>(E!, xP)") using oth_class_taut_4_b apply simp using a_objects_exist_3 by auto ultimatelyhave"[\<box>(\<forall>x. (E!-,xP)) in v]" unfolding Indiscriminate_def using qml_1[axiom_instance, deduction, deduction] by blast thus"[\<box>(\<forall>x. \<not>(E!,xP)) in v]" apply - apply (PLM_subst_method "λ x . (E!-, xP)""λ x . \<not>(E!, xP)") using thm_relation_negation_1_1 by auto next show"[\<not>\<box>(\<forall> x . \<not>(E!, xP)) in v]" using o_objects_exist_1 unfolding diamond_def exists_def apply - apply (PLM_subst_method "\<not>\<not>(\<forall>x. \<not>(E!,xP))""\<forall>x. \<not>(E!,xP)") using oth_class_taut_4_b[equiv_sym] by auto qed
lemma prop_in_f_3_c: "[\<not>(Indiscriminate (O!)) in v]" proof (rule reductio_aa_2) show"[\<not>(\<forall> x . (O!,xP)) in v]" using a_objects_exist_2[THEN qml_2[axiom_instance, deduction]] by blast next assume"[Indiscriminate O! in v]" thus"[(\<forall> x . (O!,xP)) in v]" unfolding Indiscriminate_def using o_objects_exist_2 qml_1[axiom_instance, deduction, deduction]
qml_2[axiom_instance, deduction] by blast qed
lemma prop_in_f_3_d: "[\<not>(Indiscriminate (A!)) in v]" proof (rule reductio_aa_2) show"[\<not>(\<forall> x . (A!,xP)) in v]" using o_objects_exist_3[THEN qml_2[axiom_instance, deduction]] by blast next assume"[Indiscriminate A! in v]" thus"[(\<forall> x . (A!,xP)) in v]" unfolding Indiscriminate_def using a_objects_exist_1 qml_1[axiom_instance, deduction, deduction]
qml_2[axiom_instance, deduction] by blast qed
lemma prop_in_f_4_a: "[\<not>(Propositional E!) in v]" using prop_in_thm[deduction] prop_in_f_3_a modus_tollens_1 CP by meson
lemma prop_in_f_4_b: "[\<not>(Propositional (E!-)) in v]" using prop_in_thm[deduction] prop_in_f_3_b modus_tollens_1 CP by meson
lemma prop_in_f_4_c: "[\<not>(Propositional (O!)) in v]" using prop_in_thm[deduction] prop_in_f_3_c modus_tollens_1 CP by meson
lemma prop_in_f_4_d: "[\<not>(Propositional (A!)) in v]" using prop_in_thm[deduction] prop_in_f_3_d modus_tollens_1 CP by meson
lemma prop_prop_nec_1: "[\<diamond>(\<exists> p . F = (\<lambda> x . p)) \<rightarrow> (\<exists> p . F = (\<lambda> x . p)) in v]" proof (rule CP) assume"[\<diamond>(\<exists> p . F = (\<lambda> x . p)) in v]" hence"[\<exists> p . \<diamond>(F = (\<lambda> x . p)) in v]" using"BF\<diamond>"[deduction] by auto thenobtain p where"[\<diamond>(F = (\<lambda> x . p)) in v]" by (rule "\<exists>E") hence"[\<diamond>\<box>(\<forall>x. {xP,F}\<equiv> {xP,\<lambda>x. p}) in v]" unfolding identity_defs . hence"[\<box>(\<forall>x. {xP,F}\<equiv> {xP,\<lambda>x. p}) in v]" using"5\<diamond>"[deduction] by auto hence"[(F = (\<lambda> x . p)) in v]" unfolding identity_defs . thus"[\<exists> p . (F = (\<lambda> x . p)) in v]" by PLM_solver qed
lemma prop_prop_nec_2: "[(\<forall> p . F \<noteq> (\<lambda> x . p)) \<rightarrow> \<box>(\<forall> p . F \<noteq> (\<lambda> x . p)) in v]" apply (PLM_subst_method "\<not>(\<exists> p . (F = (\<lambda> x . p)))" "(\<forall> p . \<not>(F = (\<lambda> x . p)))") using cqt_further_4 apply blast apply (PLM_subst_method "\<not>\<diamond>(\<exists>p. F = (\<lambda>x. p))" "\<box>\<not>(\<exists>p. F = (\<lambda>x. p))") using KBasic2_4[equiv_sym] prop_prop_nec_1
contraposition_1 by auto
lemma prop_prop_nec_3: "[(\<exists> p . F = (\<lambda> x . p)) \<rightarrow> \<box>(\<exists> p . F = (\<lambda> x . p)) in v]" using prop_prop_nec_1 derived_S5_rules_1_b by simp
lemma prop_prop_nec_4: "[\<diamond>(\<forall> p . F \<noteq> (\<lambda> x . p)) \<rightarrow> (\<forall> p . F \<noteq> (\<lambda> x . p)) in v]" using prop_prop_nec_2 derived_S5_rules_2_b by simp
lemma enc_prop_nec_1: "[\<diamond>(\<forall> F . {xP, F}\<rightarrow> (\<exists> p . F = (\<lambda> x . p))) \<rightarrow> (\<forall> F . {xP, F}\<rightarrow> (\<exists> p . F = (\<lambda> x . p))) in v]" proof (rule CP) assume"[\<diamond>(\<forall>F. {xP,F}\<rightarrow> (\<exists>p. F = (\<lambda>x. p))) in v]" hence1: "[(\<forall>F. \<diamond>({xP,F}\<rightarrow> (\<exists>p. F = (\<lambda>x. p)))) in v]" using"Buridan\<diamond>"[deduction] by auto
{ fix Q assume"[{xP,Q} in v]" hence"[\<box>{xP,Q} in v]" using encoding[axiom_instance, deduction] by auto moreoverhave"[\<diamond>({xP,Q}\<rightarrow> (\<exists>p. Q = (\<lambda>x. p))) in v]" using cqt_1[axiom_instance, deduction] 1by fast ultimatelyhave"[\<diamond>(\<exists>p. Q = (\<lambda>x. p)) in v]" using KBasic2_9[equiv_lr,deduction] by auto hence"[(\<exists>p. Q = (\<lambda>x. p)) in v]" using prop_prop_nec_1[deduction] by auto
} thus"[(\<forall> F . {xP, F}\<rightarrow> (\<exists> p . F = (\<lambda> x . p))) in v]" apply - by PLM_solver qed
lemma enc_prop_nec_2: "[(\<forall> F . {xP, F}\<rightarrow> (\<exists> p . F = (\<lambda> x . p))) \<rightarrow> \<box>(\<forall> F . {xP, F} \<rightarrow> (\<exists> p . F = (\<lambda> x . p))) in v]" using derived_S5_rules_1_b enc_prop_nec_1 by blast end end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.379 Sekunden
(vorverarbeitet am 2026-07-01)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.