(*<*) theory TAO_10_PossibleWorlds imports TAO_9_PLM begin (*>*) section‹Possible Worlds› text‹\label{TAO_PossibleWorlds}› locale PossibleWorlds = PLM begin subsection‹Definitions› text‹\label{TAO_PossibleWorlds_Definitions}› definition Situation where "Situation x ≡ ⦇A!,x⦈ ❙&(❙∀F. ⦃x,F⦄ ❙→Propositional F)" definition EncodeProposition (infixl "❙Σ" 70) where "x❙Σp ≡ ⦇A!,x⦈ ❙&⦃x, ❙λx . p⦄" definition TrueInSituation (infixl "❙⊨" 10) where "x ❙⊨p ≡ Situation x ❙&x❙Σp" definition PossibleWorld where "PossibleWorld x ≡ Situation x ❙&❙◇(❙∀p . x❙Σp ❙≡p)" subsection‹Auxiliary Lemmas› text‹\label{TAO_PossibleWorlds_Aux}› lemma possit_sit_1: "[Situation (x⇧^{P}) ❙≡❙□(Situation (x⇧^{P})) in v]" proof (rule "❙≡I"; rule CP) assume "[Situation (x⇧^{P}) in v]" hence 1: "[⦇A!,x⇧^{P}⦈ ❙&(❙∀F. ⦃x⇧^{P},F⦄ ❙→Propositional F) in v]" unfolding Situation_def by auto have "[❙□⦇A!,x⇧^{P}⦈ in v]" using 1[conj1, THEN oa_facts_2[deduction]] . moreover have "[❙□(❙∀F. ⦃x⇧^{P},F⦄ ❙→Propositional F) in v]" using 1[conj2] unfolding Propositional_def by (rule enc_prop_nec_2[deduction]) ultimately show "[❙□Situation (x⇧^{P}) in v]" unfolding Situation_def apply cut_tac apply (rule KBasic_3[equiv_rl]) by (rule intro_elim_1) next assume "[❙□Situation (x⇧^{P}) in v]" thus "[Situation (x⇧^{P}) in v]" using qml_2[axiom_instance, deduction] by auto qed lemma possworld_nec: "[PossibleWorld (x⇧^{P}) ❙≡❙□(PossibleWorld (x⇧^{P})) in v]" apply (rule "❙≡I"; rule CP) subgoal unfolding PossibleWorld_def apply (rule KBasic_3[equiv_rl]) apply (rule intro_elim_1) using possit_sit_1[equiv_lr] "❙&E"(1) apply blast using qml_3[axiom_instance, deduction] "❙&E"(2) by blast using qml_2[axiom_instance,deduction] by auto lemma TrueInWorldNecc: "[((x⇧^{P}) ❙⊨p) ❙≡❙□((x⇧^{P}) ❙⊨p) in v]" proof (rule "❙≡I"; rule CP) assume "[x⇧^{P}❙⊨p in v]" hence "[Situation (x⇧^{P}) ❙&(⦇A!,x⇧^{P}⦈ ❙&⦃x⇧^{P},❙λx. p⦄) in v]" unfolding TrueInSituation_def EncodeProposition_def . hence "[(❙□Situation (x⇧^{P}) ❙&❙□⦇A!,x⇧^{P}⦈) ❙&❙□⦃x⇧^{P}, ❙λx. p⦄ in v]" using "❙&I" "❙&E" possit_sit_1[equiv_lr] oa_facts_2[deduction] encoding[axiom_instance,deduction] by metis thus "[❙□((x⇧^{P}) ❙⊨p) in v]" unfolding TrueInSituation_def EncodeProposition_def using KBasic_3[equiv_rl] "❙&I" "❙&E" by metis next assume "[❙□(x⇧^{P}❙⊨p) in v]" thus "[x⇧^{P}❙⊨p in v]" using qml_2[axiom_instance,deduction] by auto qed lemma PossWorldAux: "[(⦇A!,x⇧^{P}⦈ ❙&(❙∀F . (⦃x⇧^{P},F⦄ ❙≡(❙∃p . p ❙&(F ❙=(❙λx . p)))))) ❙→(PossibleWorld (x⇧^{P})) in v]" proof (rule CP) assume DefX: "[⦇A!,x⇧^{P}⦈ ❙&(❙∀F . (⦃x⇧^{P},F⦄ ❙≡(❙∃p . p ❙&(F ❙=(❙λx . p))))) in v]" have "[Situation (x⇧^{P}) in v]" proof - have "[⦇A!,x⇧^{P}⦈ in v]" using DefX[conj1] . moreover have "[(❙∀F. ⦃x⇧^{P},F⦄ ❙→Propositional F) in v]" proof (rule "❙∀I"; rule CP) fix F assume "[⦃x⇧^{P},F⦄ in v]" moreover have "[⦃x⇧^{P},F⦄ ❙≡(❙∃p . p ❙&(F ❙=(❙λx . p))) in v]" using DefX[conj2] cqt_1[axiom_instance, deduction] by auto ultimately have "[(❙∃p . p ❙&(F ❙=(❙λx . p))) in v]" using "❙≡E"(1) by blast then obtain p where "[p ❙&(F ❙=(❙λx . p)) in v]" by (rule "❙∃E") hence "[(F ❙=(❙λx . p)) in v]" by (rule "❙&E"(2)) hence "[(❙∃p . (F ❙=(❙λx . p))) in v]" by PLM_solver thus "[Propositional F in v]" unfolding Propositional_def . qed ultimately show "[Situation (x⇧^{P}) in v]" unfolding Situation_def by (rule "❙&I") qed moreover have "[❙◇(❙∀p. x⇧^{P}❙Σp ❙≡p) in v]" unfolding EncodeProposition_def proof (rule TBasic[deduction]; rule "❙∀I") fix q have EncodeLambda: "[⦃x⇧^{P}, ❙λx. q⦄ ❙≡(❙∃p . p ❙&((❙λx. q) ❙=(❙λx . p))) in v]" using DefX[conj2] by (rule cqt_1[axiom_instance, deduction]) moreover { assume "[q in v]" moreover have "[(❙λx. q) ❙=(❙λx . q) in v]" using id_eq_prop_prop_1 by auto ultimately have "[q ❙&((❙λx. q) ❙=(❙λx . q)) in v]" by (rule "❙&I") hence "[❙∃p . p ❙&((❙λx. q) ❙=(❙λx . p)) in v]" by PLM_solver moreover have "[⦇A!,x⇧^{P}⦈ in v]" using DefX[conj1] . ultimately have "[⦇A!,x⇧^{P}⦈ ❙&⦃x⇧^{P}, ❙λx. q⦄ in v]" using EncodeLambda[equiv_rl] "❙&I" by auto } moreover { assume "[⦇A!,x⇧^{P}⦈ ❙&⦃x⇧^{P}, ❙λx. q⦄ in v]" hence "[⦃x⇧^{P}, ❙λx. q⦄ in v]" using "❙&E"(2) by auto hence "[❙∃p . p ❙&((❙λx. q) ❙=(❙λx . p)) in v]" using EncodeLambda[equiv_lr] by auto then obtain p where p_and_lambda_q_is_lambda_p: "[p ❙&((❙λx. q) ❙=(❙λx . p)) in v]" by (rule "❙∃E") have "[⦇(❙λx . p), x⇧^{P}⦈ ❙≡p in v]" apply (rule beta_C_meta_1) by show_proper hence "[⦇(❙λx . p), x⇧^{P}⦈ in v]" using p_and_lambda_q_is_lambda_p[conj1] "❙≡E"(2) by auto hence "[⦇(❙λx . q), x⇧^{P}⦈ in v]" using p_and_lambda_q_is_lambda_p[conj2, THEN id_eq_prop_prop_2[deduction]] l_identity[axiom_instance, deduction, deduction] by fast moreover have "[⦇(❙λx . q), x⇧^{P}⦈ ❙≡q in v]" apply (rule beta_C_meta_1) by show_proper ultimately have "[q in v]" using "❙≡E"(1) by blast } ultimately show "[⦇A!,x⇧^{P}⦈ ❙&⦃x⇧^{P},❙λx. q⦄ ❙≡q in v]" using "❙&I" "❙≡I" CP by auto qed ultimately show "[PossibleWorld (x⇧^{P}) in v]" unfolding PossibleWorld_def by (rule "❙&I") qed subsection‹For every syntactic Possible World there is a semantic Possible World› text‹\label{TAO_PossibleWorlds_SyntacticSemantic}› theorem SemanticPossibleWorldForSyntacticPossibleWorlds: "∀ x . [PossibleWorld (x⇧^{P}) in w] ⟶ (∃ v . ∀ p . [(x⇧^{P}❙⊨p) in w] ⟷ [p in v])" proof fix x { assume PossWorldX: "[PossibleWorld (x⇧^{P}) in w]" hence SituationX: "[Situation (x⇧^{P}) in w]" unfolding PossibleWorld_def apply cut_tac by PLM_solver have PossWorldExpanded: "[⦇A!,x⇧^{P}⦈ ❙&(❙∀F. ⦃x⇧^{P},F⦄ ❙→(❙∃p. F ❙=(❙λx. p))) ❙&❙◇(❙∀p. ⦇A!,x⇧^{P}⦈ ❙&⦃x⇧^{P},❙λx. p⦄ ❙≡p) in w]" using PossWorldX unfolding PossibleWorld_def Situation_def Propositional_def EncodeProposition_def . have AbstractX: "[⦇A!,x⇧^{P}⦈ in w]" using PossWorldExpanded[conj1,conj1] . have "[❙◇(❙∀p. ⦃x⇧^{P},❙λx. p⦄ ❙≡p) in w]" apply (PLM_subst_method "λp. ⦇A!,x⇧^{P}⦈ ❙&⦃x⇧^{P},❙λx. p⦄" "λ p . ⦃x⇧^{P},❙λx. p⦄") subgoal using PossWorldExpanded[conj1,conj1,THEN oa_facts_2[deduction]] using Semantics.T6 apply cut_tac by PLM_solver using PossWorldExpanded[conj2] . hence "∃v. ∀p. ([⦃x⇧^{P},❙λx. p⦄ in v]) = [p in v]" unfolding diamond_def equiv_def conj_def apply (simp add: Semantics.T4 Semantics.T6 Semantics.T5 Semantics.T8) by auto then obtain v where PropsTrueInSemWorld: "∀p. ([⦃x⇧^{P},❙λx. p⦄ in v]) = [p in v]" by auto { fix p { assume "[((x⇧^{P}) ❙⊨p) in w]" hence "[((x⇧^{P}) ❙⊨p) in v]" using TrueInWorldNecc[equiv_lr] Semantics.T6 by simp hence "[Situation (x⇧^{P}) ❙&(⦇A!,x⇧^{P}⦈ ❙&⦃x⇧^{P},❙λx. p⦄) in v]" unfolding TrueInSituation_def EncodeProposition_def . hence "[⦃x⇧^{P},❙λx. p⦄ in v]" using "❙&E"(2) by blast hence "[p in v]" using PropsTrueInSemWorld by blast } moreover { assume "[p in v]" hence "[⦃x⇧^{P},❙λx. p⦄ in v]" using PropsTrueInSemWorld by blast hence "[(x⇧^{P}) ❙⊨p in v]" apply cut_tac unfolding TrueInSituation_def EncodeProposition_def apply (rule "❙&I") using SituationX[THEN possit_sit_1[equiv_lr]] subgoal using Semantics.T6 by auto apply (rule "❙&I") subgoal using AbstractX[THEN oa_facts_2[deduction]] using Semantics.T6 by auto by assumption hence "[❙□((x⇧^{P}) ❙⊨p) in v]" using TrueInWorldNecc[equiv_lr] by simp hence "[(x⇧^{P}) ❙⊨p in w]" using Semantics.T6 by simp } ultimately have "[p in v] ⟷ [(x⇧^{P}) ❙⊨p in w]" by auto } hence "(∃ v . ∀ p . [p in v] ⟷ [(x⇧^{P}) ❙⊨p in w])" by blast } thus "[PossibleWorld (x⇧^{P}) in w] ⟶ (∃v. ∀ p . [(x⇧^{P}) ❙⊨p in w] ⟷ [p in v])" by blast qed subsection‹For every semantic Possible World there is a syntactic Possible World› text‹\label{TAO_PossibleWorlds_SemanticSyntactic}› theorem SyntacticPossibleWorldForSemanticPossibleWorlds: "∀ v . ∃ x . [PossibleWorld (x⇧^{P}) in w] ∧ (∀ p . [p in v] ⟷ [((x⇧^{P}) ❙⊨p) in w])" proof fix v have "[❙∃x. ⦇A!,x⇧^{P}⦈ ❙&(❙∀F . (⦃x⇧^{P},F⦄ ❙≡(❙∃p . p ❙&(F ❙=(❙λx . p))))) in v]" using A_objects[axiom_instance] by fast then obtain x where DefX: "[⦇A!,x⇧^{P}⦈ ❙&(❙∀F . (⦃x⇧^{P},F⦄ ❙≡(❙∃p . p ❙&(F ❙=(❙λx . p))))) in v]" by (rule "❙∃E") hence PossWorldX: "[PossibleWorld (x⇧^{P}) in v]" using PossWorldAux[deduction] by blast hence "[PossibleWorld (x⇧^{P}) in w]" using possworld_nec[equiv_lr] Semantics.T6 by auto moreover have "(∀ p . [p in v] ⟷ [(x⇧^{P}) ❙⊨p in w])" proof fix q { assume "[q in v]" moreover have "[(❙λx . q) ❙=(❙λx . q) in v]" using id_eq_prop_prop_1 by auto ultimately have "[q ❙&(❙λx . q) ❙=(❙λx . q) in v]" using "❙&I" by auto hence "[(❙∃p . p ❙&((❙λx . q) ❙=(❙λx . p))) in v]" by PLM_solver hence 4: "[⦃x⇧^{P}, (❙λx . q)⦄ in v]" using cqt_1[axiom_instance,deduction, OF DefX[conj2], equiv_rl] by blast have "[(x⇧^{P}❙⊨q) in v]" unfolding TrueInSituation_def apply (rule "❙&I") using PossWorldX unfolding PossibleWorld_def using "❙&E"(1) apply blast unfolding EncodeProposition_def apply (rule "❙&I") using DefX[conj1] apply simp using 4 . hence "[(x⇧^{P}❙⊨q) in w]" using TrueInWorldNecc[equiv_lr] Semantics.T6 by auto } moreover { assume "[(x⇧^{P}❙⊨q) in w]" hence "[(x⇧^{P}❙⊨q) in v]" using TrueInWorldNecc[equiv_lr] Semantics.T6 by auto hence "[⦃x⇧^{P}, (❙λx . q)⦄ in v]" unfolding TrueInSituation_def EncodeProposition_def using "❙&E"(2) by blast hence "[(❙∃p . p ❙&((❙λx . q) ❙=(❙λx . p))) in v]" using cqt_1[axiom_instance,deduction, OF DefX[conj2], equiv_lr] by blast then obtain p where 4: "[(p ❙&((❙λx . q) ❙=(❙λx . p))) in v]" by (rule "❙∃E") have "[⦇(❙λx . p),x⇧^{P}⦈ ❙≡p in v]" apply (rule beta_C_meta_1) by show_proper hence "[⦇(❙λx . q),x⇧^{P}⦈ ❙≡p in v]" using l_identity[where β="(❙λx . q)" and α="(❙λx . p)", axiom_instance, deduction, deduction] using 4[conj2,THEN id_eq_prop_prop_2[deduction]] by meson hence "[⦇(❙λx . q),x⇧^{P}⦈ in v]" using 4[conj1] "❙≡E"(2) by blast moreover have "[⦇(❙λx . q),x⇧^{P}⦈ ❙≡q in v]" apply (rule beta_C_meta_1) by show_proper ultimately have "[q in v]" using "❙≡E"(1) by blast } ultimately show "[q in v] ⟷ [(x⇧^{P}) ❙⊨q in w]" by blast qed ultimately show "∃ x . [PossibleWorld (x⇧^{P}) in w] ∧ (∀ p . [p in v] ⟷ [(x⇧^{P}) ❙⊨p in w])" by auto qed end (*<*) end (*>*)