Theory TAO_10_PossibleWorlds

(*<*)
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
(*>*)