diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,705 +1,706 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRYSTALS-Kyber CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DPRM_Theorem DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Padic_Field Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions SCC_Bloemen_Sequential Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching +Stalnaker_Logic Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Stalnaker_Logic/ROOT b/thys/Stalnaker_Logic/ROOT new file mode 100644 --- /dev/null +++ b/thys/Stalnaker_Logic/ROOT @@ -0,0 +1,9 @@ +chapter AFP + +session Stalnaker_Logic (AFP) = "Epistemic_Logic" + + options [timeout = 300] + theories + Stalnaker_Logic + document_files + "root.tex" + "root.bib" diff --git a/thys/Stalnaker_Logic/Stalnaker_Logic.thy b/thys/Stalnaker_Logic/Stalnaker_Logic.thy new file mode 100644 --- /dev/null +++ b/thys/Stalnaker_Logic/Stalnaker_Logic.thy @@ -0,0 +1,599 @@ +(* + File: Stalnaker_Logic.thy + Author: Laura Gamboa Guzman + + This work is a formalization of Stalnaker's epistemic logic with countably + many agents and its soundness and completeness theorems, as well as the + equivalence between the axiomatization of S4 available in the Epistemic + Logic theory and the topological one. + It builds on the Epistemic_Logic theory by A.H. From. +*) + +theory Stalnaker_Logic + imports "Epistemic_Logic.Epistemic_Logic" + +begin + + +section \Utility\ + +subsection \Some properties of Normal Modal Logics\ + +lemma duality_taut: \tautology (((K i p) \<^bold>\ K i (\<^bold>\q))\<^bold>\ ((L i q) \<^bold>\ (\<^bold>\ K i p)))\ + by force + +lemma K_imp_trans: + assumes \A \ (p \<^bold>\ q)\ \A \ (q \<^bold>\ r)\ + shows \A \ (p \<^bold>\ r)\ +proof - + have \tautology ((p \<^bold>\ q) \<^bold>\ ( (q \<^bold>\ r) \<^bold>\ (p \<^bold>\ r)))\ + by fastforce + then show ?thesis + by (meson A1 R1 assms(1) assms(2)) +qed + +lemma K_imp_trans': + assumes \A \ (q \<^bold>\ r)\ + shows \A \ ((p \<^bold>\ q) \<^bold>\ (p \<^bold>\ r))\ +proof - + have \tautology ((q \<^bold>\ r) \<^bold>\ ((p \<^bold>\ q) \<^bold>\ (p \<^bold>\ r)))\ + by fastforce + then show ?thesis + using A1 R1 assms by blast +qed + +lemma K_imply_multi: + assumes \A \ (a \<^bold>\ b)\ and \A \ (a \<^bold>\ c)\ + shows \A \ (a \<^bold>\ (b\<^bold>\c))\ +proof - + have \tautology ((a\<^bold>\b)\<^bold>\(a\<^bold>\c)\<^bold>\(a\<^bold>\(b\<^bold>\c)))\ + by force + then have \A \ ((a\<^bold>\b)\<^bold>\(a\<^bold>\c)\<^bold>\(a\<^bold>\(b\<^bold>\c)))\ + using A1 by blast + then have \A \ ((a\<^bold>\c)\<^bold>\(a\<^bold>\(b\<^bold>\c)))\ + using assms(1) R1 by blast + then show ?thesis + using assms(2) R1 by blast +qed + +lemma K_multi_imply: + assumes \A \ (a \<^bold>\ b \<^bold>\ c)\ + shows \A \ ((a\<^bold>\b) \<^bold>\ c)\ +proof - + have \tautology ((a \<^bold>\ b \<^bold>\ c) \<^bold>\ ((a\<^bold>\b) \<^bold>\ c))\ + by force + then have \A \ ((a \<^bold>\ b \<^bold>\ c) \<^bold>\ ((a\<^bold>\b) \<^bold>\ c))\ + using A1 by blast + then show ?thesis + using assms R1 by blast +qed + +lemma K_thm: \A \ ((K i p) \<^bold>\ (L i q) \<^bold>\ L i (p \<^bold>\ q))\ +proof - + have \tautology (p \<^bold>\ (\<^bold>\(p \<^bold>\ q)) \<^bold>\ \<^bold>\ q)\ + by force + then have \A \ (p \<^bold>\ (\<^bold>\(p \<^bold>\ q)) \<^bold>\ \<^bold>\ q)\ + by (simp add: A1) + then have \A \ ((K i p) \<^bold>\ K i ((\<^bold>\(p \<^bold>\ q)) \<^bold>\ \<^bold>\ q))\ + and \A \ (K i ((\<^bold>\(p \<^bold>\ q)) \<^bold>\ \<^bold>\ q) \<^bold>\ K i (\<^bold>\(p \<^bold>\ q)) \<^bold>\ K i (\<^bold>\ q))\ + apply (simp add: K_map) + by (meson K_A2') + then have \A \ ((K i p) \<^bold>\ K i (\<^bold>\(p \<^bold>\ q)) \<^bold>\ K i (\<^bold>\ q))\ + using K_imp_trans by blast + then have \A \ ((K i p) \<^bold>\ L i (q) \<^bold>\ L i (p \<^bold>\ q))\ + by (metis AK.simps K_imp_trans duality_taut) + then show ?thesis + by (simp add: K_multi_imply) +qed + +primrec conjunct :: \'i fm list \ 'i fm\ where + \conjunct [] = \<^bold>\\ +| \conjunct (p#ps) = (p \<^bold>\ conjunct ps)\ + +lemma imply_conjunct: \tautology ((imply G p) \<^bold>\ ((conjunct G) \<^bold>\ p))\ + apply(induction G) + apply simp + by force + +lemma conjunct_imply: \tautology (((conjunct G) \<^bold>\ p) \<^bold>\(imply G p))\ + by (induct G) simp_all + +lemma K_imply_conjunct: + assumes \A \ imply G p\ + shows \A \ ((conjunct G) \<^bold>\ p)\ + using A1 R1 assms imply_conjunct by blast + +lemma K_conjunct_imply: + assumes \A \ ((conjunct G) \<^bold>\ p)\ + shows \A \ imply G p\ + using A1 R1 assms conjunct_imply by blast + +lemma K_conj_imply_factor: + fixes A :: \(('i :: countable) fm \ bool)\ + shows \A \ ((((K i p) \<^bold>\ (K i q)) \<^bold>\ r) \<^bold>\((K i (p \<^bold>\ q)) \<^bold>\ r))\ +proof - + have *: \A \ ((K i (p \<^bold>\ q)) \<^bold>\ ((K i p) \<^bold>\ (K i q)))\ + proof (rule ccontr) + assume \\ A \ ((K i (p \<^bold>\ q)) \<^bold>\ ((K i p) \<^bold>\ (K i q)))\ + then have \consistent A {\<^bold>\((K i (p \<^bold>\ q)) \<^bold>\ ((K i p) \<^bold>\ (K i q)))}\ + by (metis imply.simps(1) inconsistent_imply insert_is_Un list.set(1)) + let ?V = \Extend A {\<^bold>\((K i (p \<^bold>\ q)) \<^bold>\ ((K i p) \<^bold>\ (K i q)))} from_nat\ + let ?M = \Kripke (mcss A) pi (reach A)\ + have \?V \ \ ?M \ ?M, ?V \ \<^bold>\((K i (p \<^bold>\ q)) \<^bold>\ ((K i p) \<^bold>\ (K i q)))\ + using canonical_model \consistent A {\<^bold>\ (K i (p \<^bold>\ q) \<^bold>\ K i p \<^bold>\ K i q)}\ + insert_iff kripke.sel(1) mem_Collect_eq by fastforce + then have o: \?M, ?V \ ((K i (p \<^bold>\ q)) \<^bold>\ \<^bold>\((K i p) \<^bold>\ (K i q)))\ + by auto + then have \?M, ?V \ (K i (p \<^bold>\ q))\ \(?M, ?V \ \<^bold>\(K i p)) \ (?M, ?V \ \<^bold>\(K i q))\ + by auto + then have \\ U \ \ ?M \ \ ?M i ?V. ?M, U \(p \<^bold>\ q)\ + \\ U \ \ ?M \ \ ?M i ?V. ?M, U \ ((\<^bold>\p) \<^bold>\ (\<^bold>\q))\ + apply (meson semantics.simps(6)) + using o by auto + then show False + by simp + qed + then have \A \ (((K i (p \<^bold>\ q)) \<^bold>\ ((K i p) \<^bold>\ (K i q))) \<^bold>\ + ((((K i p) \<^bold>\ (K i q)) \<^bold>\ r) \<^bold>\ ((K i (p \<^bold>\ q)) \<^bold>\ r)))\ + by (simp add: A1) + then show ?thesis + using "*" R1 by blast +qed + +lemma K_conjunction_in: \A \ (K i (p \<^bold>\ q) \<^bold>\ ((K i p) \<^bold>\ K i q))\ +proof - + have o1: \A \ ((p\<^bold>\q) \<^bold>\ p)\ and o2: \A \ ((p\<^bold>\q) \<^bold>\ q)\ + apply(simp add: A1) + by (simp add: A1) + then have c1: \A \ (K i (p \<^bold>\ q) \<^bold>\ K i q)\ and c2: \A \ (K i (p \<^bold>\ q) \<^bold>\ K i p)\ + apply (simp add: K_map o2) + by (simp add: K_map o1) + then show ?thesis + by (simp add: K_imply_multi) +qed + +lemma K_conjunction_in_mult: \A \ ((K i (conjunct G)) \<^bold>\ conjunct (map (K i) G))\ +proof (induct G) + case Nil + then show ?case + by (simp add: A1) + case (Cons a G) + then have \A \ ((K i (conjunct (a#G))) \<^bold>\ (K i (a \<^bold>\ conjunct G)))\ + and \A \ ((K i (a \<^bold>\ conjunct G)) \<^bold>\ ((K i a) \<^bold>\ K i (conjunct G)))\ + apply (simp add: A1) + by (metis K_conjunction_in) + then have o1: \A \ ((K i (conjunct (a#G))) \<^bold>\ ((K i a) \<^bold>\ K i (conjunct G)))\ + using K_imp_trans by blast + then have \A \ (((K i a) \<^bold>\ K i (conjunct G)) \<^bold>\ K i a)\ + and o2: \A \ (((K i a) \<^bold>\ K i (conjunct G)) \<^bold>\ conjunct (map (K i) G))\ + apply (simp add: A1) + by (metis Cons.hyps K_imply_Cons K_multi_imply imply.simps(1) imply.simps(2)) + then have \A \ (((K i a) \<^bold>\ K i (conjunct G)) \<^bold>\ (K i a) \<^bold>\ conjunct (map (K i) G))\ + using K_imply_multi by blast + then show ?case + using K_imp_trans o1 by auto +qed + +lemma K_conjunction_out: \A \ ((K i p) \<^bold>\ (K i q) \<^bold>\ K i (p \<^bold>\ q))\ +proof - + have \A \ (p \<^bold>\ q \<^bold>\ p\<^bold>\q)\ + by (simp add: A1) + then have \A \ K i (p \<^bold>\ q \<^bold>\ p\<^bold>\q)\ + by (simp add: R2) + then have \A \ ((K i p) \<^bold>\ K i (q \<^bold>\ p\<^bold>\q))\ + by (simp add: K_map \A \ (p \<^bold>\ q \<^bold>\ p \<^bold>\ q)\) + then have \A \ ((K i p) \<^bold>\ (K i q) \<^bold>\ K i (p\<^bold>\q))\ + by (meson K_A2' K_imp_trans) + then show ?thesis + using K_multi_imply by blast +qed + +lemma K_conjunction_out_mult: \A \ (conjunct (map (K i) G) \<^bold>\ (K i (conjunct G)))\ +proof (induct G) + case Nil + then show ?case + by (metis A1 K_imply_conjunct Nil_is_map_conv R2 conjunct.simps(1) eval.simps(5) imply.simps(1)) + case (Cons a G) + then have \A \ ((conjunct (map (K i) (a#G))) \<^bold>\ ((K i a) \<^bold>\ conjunct (map (K i) G)))\ + by (simp add: A1) + then have *: \A \ (((K i a) \<^bold>\ conjunct (map (K i) G))\<^bold>\ (K i a) \<^bold>\ K i (conjunct G))\ + by (metis Cons.hyps K_imply_Cons K_imply_head K_imply_multi K_multi_imply imply.simps(1) imply.simps(2)) + then have \A \ (((K i a) \<^bold>\ K i (conjunct G))\<^bold>\ K i (conjunct (a#G)))\ + by (simp add: K_conjunction_out) + then show ?case + using "*" K_imp_trans by auto +qed + +subsection \More on mcs's properties\ + +lemma mcs_conjunction: + assumes \consistent A V\ and \maximal A V\ + shows \p \ V \ q \ V \ (p \<^bold>\ q) \ V\ +proof - + have \tautology (p \<^bold>\ q \<^bold>\ (p\<^bold>\q))\ + by force + then have \(p \<^bold>\ q \<^bold>\ (p\<^bold>\q)) \ V\ + using A1 assms(1) assms(2) deriv_in_maximal by blast + then have \p \ V \ (q \<^bold>\ (p\<^bold>\q)) \ V\ + by (meson assms(1) assms(2) consequent_in_maximal) + then show ?thesis + using assms(1) assms(2) consequent_in_maximal by blast +qed + +lemma mcs_conjunction_mult: + assumes \consistent A V\ and \maximal A V\ + shows \(set (S :: ('i fm list)) \ V \ finite (set S)) \ (conjunct S) \ V\ +proof(induct S) + case Nil + then show ?case + by (metis K_Boole assms(1) assms(2) conjunct.simps(1) consistent_def inconsistent_subset maximal_def) + case (Cons a S) + then have \set S \ set (a#S)\ + by (meson set_subset_Cons) + then have c1: \ set (a # S) \ V \ finite (set (a # S)) \ conjunct (S) \ V \ a \ V\ + using Cons by fastforce + then have \ conjunct (S) \ V \ a \ V \ (conjunct (a#S)) \ V \ + using assms(1) assms(2) mcs_conjunction by auto + then show ?case + using c1 by fastforce +qed + +lemma reach_dualK: + assumes \consistent A V\ \maximal A V\ + and \consistent A W\ \maximal A W\ \W \ reach A i V\ + shows \\p. p \ W \ (L i p) \ V\ +proof (rule ccontr) + assume \\ (\p. p \ W \ (L i p) \ V)\ + then obtain p' where *: \p' \ W \ (L i p') \ V\ + by presburger + then have \(\<^bold>\ L i p') \ V\ + using assms(1) assms(2) assms(3) assms(4) assms(5) exactly_one_in_maximal by blast + then have \K i (\<^bold>\ p') \ V\ + using assms(1) assms(2) exactly_one_in_maximal by blast + then have \(\<^bold>\ p') \ W\ + using assms(5) by blast + then show False + by (meson "*" assms(3) assms(4) exactly_one_in_maximal) +qed + +lemma dual_reach: + assumes \consistent A V\ \maximal A V\ + shows \(L i p) \ V \ (\ W. W \ reach A i V \ p \ W)\ +proof - + have \(\W. W \ {W. known V i \ W} \ p \ W) \ (\W. W \ {W. known V i \ W} \ (\<^bold>\p) \ W)\ + by blast + then have \(\W. W \ {W. known V i \ W} \ (\<^bold>\p) \ W) \ (\ W. W \ reach A i V \ (\<^bold>\p) \ W)\ + by fastforce + then have \(\ W. W \ reach A i V \ (\<^bold>\p) \ W) \ ((K i (\<^bold>\p)) \ V)\ + by blast + then have \((K i (\<^bold>\p)) \ V) \ (\((L i p) \ V))\ + using assms(1) assms(2) exactly_one_in_maximal by blast + then have \(\W. W \ {W. known V i \ W} \ p \ W) \ \((L i p) \ V)\ + by blast + then show ?thesis + by blast +qed + + +section \Ax.2\ + +definition weakly_directed :: \('i, 's) kripke \ bool\ where + \weakly_directed M \ \i. \s \ \ M. \t \ \ M. \r \ \ M. + (r \ \ M i s \ t \ \ M i s)\(\ u \ \ M. (u \ \ M i r \ u \ \ M i t))\ + +inductive Ax_2 :: \('i :: countable) fm \ bool\ where + \Ax_2 (\<^bold>\ K i (\<^bold>\ K i p) \<^bold>\ K i (\<^bold>\ K i (\<^bold>\ p)))\ + +subsection \Soundness\ + +theorem weakly_directed: + assumes \weakly_directed M\ \w \ \ M\ + shows \M, w \ (L i (K i p) \<^bold>\ K i (L i p))\ +proof + assume \M, w \ (L i (K i p))\ + then have \\v \ \ M \ \ M i w. M, v \ K i p\ + by simp + then have \\v \ \ M \ \ M i w. \u \ \ M \ \ M i v. M, u \ p\ + using \weakly_directed M\ \w \ \ M\ unfolding weakly_directed_def + by (metis IntE IntI semantics.simps(6)) + then have \\v \ \ M \ \ M i w. M, v \ L i p\ + by simp + then show \M, w \ K i (L i p)\ + by simp +qed + +lemma soundness_Ax_2: \Ax_2 p \ weakly_directed M \ w \ \ M \ M, w \ p\ + by (induct p rule: Ax_2.induct) (meson weakly_directed) + +subsection \Imply completeness\ + +lemma Ax_2_weakly_directed: + fixes A :: \(('i :: countable) fm \ bool)\ + assumes \\p. Ax_2 p \ A p\ \consistent A V\ \maximal A V\ + and \consistent A W\ \maximal A W\ \consistent A U\ \maximal A U\ + and \W \ reach A i V\ \U \ reach A i V\ + shows \\X. (consistent A X) \ (maximal A X) \ X \ (reach A i W) \ (reach A i U)\ +proof (rule ccontr) + assume \\ ?thesis\ + let ?S = \(known W i) \ (known U i)\ + have \\ consistent A ?S\ + by (smt (verit, best) Int_Collect \\X. consistent A X \ maximal A X \ X \ {Wa. known W i \ Wa} \ {W. known U i \ W}\ maximal_extension mem_Collect_eq sup.bounded_iff) + then obtain S' where *: \A \ imply S' \<^bold>\\ \set S' \ ?S\ \finite (set S')\ + unfolding consistent_def by blast + let ?U = \filter (\p. p \ (known U i)) S'\ + let ?W = \filter (\p. p \ (known W i)) S'\ + let ?p = \conjunct ?U\ and ?q = \conjunct ?W\ + have \(set ?U) \ (set ?W) = (set S')\ + using * by auto + then have \A \ imply ?U (imply ?W \<^bold>\)\ + using K_imply_weaken imply_append + by (metis (mono_tags, lifting) "*"(1) set_append subset_refl) + then have \A \ (?p \<^bold>\ (imply ?W \<^bold>\))\ + using K_imply_conjunct by blast + then have \tautology ((imply ?W \<^bold>\) \<^bold>\ (?q \<^bold>\ \<^bold>\))\ + using imply_conjunct by blast + then have \A \ ((imply ?W \<^bold>\) \<^bold>\ (?q \<^bold>\ \<^bold>\))\ + using A1 by blast + then have \A \ (?p \<^bold>\ (?q \<^bold>\ \<^bold>\))\ + using K_imp_trans \A \ (conjunct (filter (\p. p \ known U i) S') \<^bold>\ imply (filter (\p. p \ known W i) S') \<^bold>\)\ + by blast + then have o1: \A \ ((?p \<^bold>\ ?q) \<^bold>\ \<^bold>\)\ + by (meson K_multi_imply) + moreover have \set ?U \ (known U i)\ and \set ?W \ (known W i)\ + and \\ p. p \ set ?U \ (K i p) \ U\ and \\ p. p \ set ?W \ (K i p) \ W\ + by auto + then have \set (map (K i) ?U) \ U\ and c1: \set (map (K i) ?W) \ W\ + apply (metis (mono_tags, lifting) imageE set_map subsetI) + by auto + then have c2: \conjunct (map (K i) ?U) \ U\ and c2': \conjunct (map (K i) ?W) \ W\ + using assms(6) assms(7) mcs_conjunction_mult apply blast + using assms(4) assms(5) c1 mcs_conjunction_mult by blast + then have \((conjunct (map (K i) ?U)) \<^bold>\ (K i ?p)) \ U\ + and c3: \((conjunct (map (K i) ?W)) \<^bold>\ (K i ?q)) \ W\ + apply (meson K_conjunction_out_mult assms(6) assms(7) deriv_in_maximal) + by (meson K_conjunction_out_mult assms(4) assms(5) deriv_in_maximal) + then have c4: \(K i ?p) \ U\ and c4': \(K i ?q) \ W\ + using assms(6) assms(7) c2 consequent_in_maximal apply blast + using assms(4) assms(5) c2' c3 consequent_in_maximal by blast + then have \(L i (K i ?p)) \ V\ and c5: \(L i (K i ?q)) \ V\ + using assms(2) assms(3) assms(6) assms(7) assms(9) exactly_one_in_maximal apply blast + using assms(2) assms(3) assms(4) assms(5) assms(8) c4' exactly_one_in_maximal by blast + then have \(K i (L i ?p)) \ V\ + by (meson Ax_2.intros assms(1) assms(2) assms(3) ax_in_maximal consequent_in_maximal) + then have \((K i (L i ?p)) \<^bold>\ (L i (K i ?q))) \ V\ + using assms(2) assms(3) c5 mcs_conjunction by blast + then have \(L i ((L i ?p) \<^bold>\ K i ?q)) \ V\ + by (meson K_thm assms(2) assms(3) consequent_in_maximal deriv_in_maximal) + then have \(L i ((K i ?q) \<^bold>\ L i ?p)) \ V\ + by (smt (z3) \K i (L i (conjunct (filter (\p. p \ known U i) S'))) \ V\ assms(2) assms(3) assms(4) assms(5) assms(8) c4' exactly_one_in_maximal mcs_conjunction mem_Collect_eq subset_iff) + then obtain Z' where z1:\(consistent A Z') \ (maximal A Z')\ and z2:\Z' \ (reach A i V)\ + and z3: \((K i ?q) \<^bold>\ L i ?p) \ Z'\ + using \K i (L i (conjunct (filter (\p. p \ known U i) S'))) \ V\ assms(4) assms(5) assms(8) c4' mcs_conjunction by blast + then have z4: \(L i (?q \<^bold>\ ?p)) \ Z'\ + by (metis K_thm consequent_in_maximal deriv_in_maximal) + then have o2:\(L i (L i (?q \<^bold>\ ?p))) \ V\ + using assms(2) assms(3) mcs_properties(2) z1 z2 by blast + then have \A \ K i (K i (((?p \<^bold>\ ?q) \<^bold>\ \<^bold>\)))\ + by (metis R2 o1) + then have o3:\K i (K i (((?p \<^bold>\ ?q) \<^bold>\ \<^bold>\))) \ V\ + using assms(2) assms(3) deriv_in_maximal by blast + then obtain X1 where x1:\(consistent A X1) \ (maximal A X1)\ and x2:\X1 \ (reach A i V)\ + and x3: \(L i (?q \<^bold>\ ?p)) \ X1\ + using z1 z2 z4 by blast + then have x4:\(K i (((?p \<^bold>\ ?q) \<^bold>\ \<^bold>\))) \ X1\ + using o3 by blast + then have t:\\x. \y. tautology (((x\<^bold>\y)\<^bold>\\<^bold>\)\<^bold>\\<^bold>\(y\<^bold>\x))\ + by (metis eval.simps(4) eval.simps(5)) + then have \(((?p\<^bold>\?q)\<^bold>\\<^bold>\)\<^bold>\\<^bold>\(?q\<^bold>\?p)) \ X1\ + using A1 deriv_in_maximal x1 by blast + then have \K i (((?p\<^bold>\?q)\<^bold>\\<^bold>\)\<^bold>\\<^bold>\(?q\<^bold>\?p)) \ X1\ + by (meson A1 R2 deriv_in_maximal t x1) + then have \(K i ((?p\<^bold>\?q)\<^bold>\\<^bold>\)\<^bold>\ K i (\<^bold>\(?q\<^bold>\?p))) \ X1\ + by (meson K_A2' consequent_in_maximal deriv_in_maximal x1) + then have \(K i ((?p\<^bold>\?q)\<^bold>\\<^bold>\)\<^bold>\ (\<^bold>\ L i(?q\<^bold>\?p))) \ X1\ + using consequent_in_maximal exactly_one_in_maximal x1 x3 x4 by blast + then have \(\<^bold>\ L i(?q\<^bold>\?p)) \ X1 \ (L i(?q\<^bold>\?p)) \ X1\ + using consequent_in_maximal x1 x4 x3 by blast + then show False + using exactly_one_in_maximal x1 by blast +qed + +lemma mcs\<^sub>_\<^sub>2_weakly_directed: + fixes A :: \(('i :: countable) fm \ bool)\ + assumes \\p. Ax_2 p \ A p\ + shows \weakly_directed (Kripke (mcss A) pi (reach A))\ + unfolding weakly_directed_def +proof (intro allI ballI, auto) + fix i V U W + assume \consistent A V\ \maximal A V\ \consistent A U\ \maximal A U\ \consistent A W\ + \maximal A W\ \known V i \ U\ \known V i \ W\ + then have \\X. (consistent A X) \ (maximal A X) \ X \ (reach A i W) \ (reach A i U)\ + using Ax_2_weakly_directed [where A=A and V=V and W=W and U=U] assms IntD2 + by simp + then have \\X. (consistent A X) \ (maximal A X) \ X \ (reach A i W) \ X \ (reach A i U)\ + by simp + then show \\X. (consistent A X) \ (maximal A X) \ known W i \ X \ known U i \ X\ + by auto +qed + +lemma imply_completeness_K_2: + assumes valid: \\(M :: ('i :: countable, 'i fm set) kripke). \w \ \ M. + weakly_directed M \ (\q \ G. M, w \ q) \ M, w \ p\ + shows \\qs. set qs \ G \ (Ax_2 \ imply qs p)\ +proof (rule ccontr) +assume \\qs. set qs \ G \ Ax_2 \ imply qs p\ + then have *: \\qs. set qs \ G \ \ Ax_2 \ imply ((\<^bold>\ p) # qs) \<^bold>\\ + using K_Boole by blast + + let ?S = \{\<^bold>\ p} \ G\ + let ?V = \Extend Ax_2 ?S from_nat\ + let ?M = \Kripke (mcss Ax_2) pi (reach Ax_2)\ + + have \consistent Ax_2 ?S\ + using * by (metis K_imply_Cons consistent_def inconsistent_subset) + then have \?M, ?V \ (\<^bold>\ p)\ \\q \ G. ?M, ?V \ q\ \consistent Ax_2 ?V\ \maximal Ax_2 ?V\ + using canonical_model unfolding list_all_def by fastforce+ + moreover have \weakly_directed ?M\ + using mcs\<^sub>_\<^sub>2_weakly_directed [where A=Ax_2] by fast + ultimately have \?M, ?V \ p\ + using valid by auto + then show False + using \?M, ?V \ (\<^bold>\ p)\ by simp +qed + + +section \System S4.2\ + +abbreviation SystemS4_2 :: \('i :: countable) fm \ bool\ ("\\<^sub>S\<^sub>4\<^sub>2 _" [50] 50) where + \\\<^sub>S\<^sub>4\<^sub>2 p \ AxT \ Ax4 \ Ax_2 \ p\ + +abbreviation AxS4_2 :: \('i :: countable) fm \ bool\ where + \AxS4_2 \ AxT \ Ax4 \ Ax_2\ + +subsection \Soundness\ + +abbreviation w_directed_preorder :: \('i, 'w) kripke \ bool\ where + \w_directed_preorder M \ reflexive M \ transitive M \ weakly_directed M\ + +lemma soundness_AxS4_2: \AxS4_2 p \ w_directed_preorder M \ w \ \ M \ M, w \ p\ + using soundness_AxT soundness_Ax4 soundness_Ax_2 by metis + +lemma soundness\<^sub>S\<^sub>4\<^sub>2: \\\<^sub>S\<^sub>4\<^sub>2 p \ w_directed_preorder M \ w \ \ M \ M, w \ p\ + using soundness soundness_AxS4_2 . + +subsection \Completeness\ + +lemma imply_completeness_S4_2: + assumes valid: \\(M :: ('i :: countable, 'i fm set) kripke). \w \ \ M. + w_directed_preorder M \ (\q \ G. M, w \ q) \ M, w \ p\ + shows \\qs. set qs \ G \ (AxS4_2 \ imply qs p)\ +proof (rule ccontr) + assume \\qs. set qs \ G \ AxS4_2 \ imply qs p\ + then have *: \\qs. set qs \ G \ \ AxS4_2 \ imply ((\<^bold>\ p) # qs) \<^bold>\\ + using K_Boole by blast + + let ?S = \{\<^bold>\ p} \ G\ + let ?V = \Extend AxS4_2 ?S from_nat\ + let ?M = \Kripke (mcss AxS4_2) pi (reach AxS4_2)\ + + have \consistent AxS4_2 ?S\ + using * by (metis (no_types, lifting) K_imply_Cons consistent_def inconsistent_subset) + then have + \?M, ?V \ (\<^bold>\ p)\ \\q \ G. ?M, ?V \ q\ + \consistent AxS4_2 ?V\ \maximal AxS4_2 ?V\ + using canonical_model unfolding list_all_def by fastforce+ + moreover have \w_directed_preorder ?M\ + by (simp add: mcs\<^sub>T_reflexive mcs\<^sub>_\<^sub>2_weakly_directed mcs\<^sub>K\<^sub>4_transitive) + ultimately have \?M, ?V \ p\ + using valid by auto + then show False + using \?M, ?V \ (\<^bold>\ p)\ by simp +qed + +lemma completeness\<^sub>S\<^sub>4\<^sub>2: + assumes \\(M :: ('i :: countable, 'i fm set) kripke). \w \ \ M. w_directed_preorder M \ M, w \ p\ + shows \\\<^sub>S\<^sub>4\<^sub>2 p\ + using assms imply_completeness_S4_2[where G=\{}\] by auto + +abbreviation \valid\<^sub>S\<^sub>4\<^sub>2 p \ \(M :: (nat, nat fm set) kripke). \w \ \ M. w_directed_preorder M \ M, w \ p\ + +theorem main\<^sub>S\<^sub>4\<^sub>2: \valid\<^sub>S\<^sub>4\<^sub>2 p \ \\<^sub>S\<^sub>4\<^sub>2 p\ + using soundness\<^sub>S\<^sub>4\<^sub>2 completeness\<^sub>S\<^sub>4\<^sub>2 by fast + +corollary + assumes \w_directed_preorder M\ \w \ \ M\ + shows \valid\<^sub>S\<^sub>4\<^sub>2 p \ M, w \ p\ + using assms soundness\<^sub>S\<^sub>4\<^sub>2 completeness\<^sub>S\<^sub>4\<^sub>2 by fast + + +section \Topological S4 axioms\ + +abbreviation DoubleImp (infixr "\<^bold>\" 25) where + \(p\<^bold>\q) \ ((p \<^bold>\ q) \<^bold>\ (q \<^bold>\ p))\ + +inductive System_topoS4 :: \'i fm \ bool\ ("\\<^sub>T\<^sub>o\<^sub>p _" [50] 50) where + A1': \tautology p \ \\<^sub>T\<^sub>o\<^sub>p p\ +| AR: \\\<^sub>T\<^sub>o\<^sub>p ((K i (p \<^bold>\ q)) \<^bold>\ ((K i p) \<^bold>\ K i q))\ +| AT': \\\<^sub>T\<^sub>o\<^sub>p (K i p \<^bold>\ p)\ +| A4': \\\<^sub>T\<^sub>o\<^sub>p (K i p \<^bold>\ K i (K i p))\ +| AN: \\\<^sub>T\<^sub>o\<^sub>p K i \<^bold>\\ +| R1': \\\<^sub>T\<^sub>o\<^sub>p p \ \\<^sub>T\<^sub>o\<^sub>p (p \<^bold>\ q) \ \\<^sub>T\<^sub>o\<^sub>p q\ +| RM: \\\<^sub>T\<^sub>o\<^sub>p (p \<^bold>\ q) \ \\<^sub>T\<^sub>o\<^sub>p ((K i p) \<^bold>\ K i q)\ + +lemma topoS4_trans: \\\<^sub>T\<^sub>o\<^sub>p ((p \<^bold>\ q) \<^bold>\ (q \<^bold>\ r) \<^bold>\ p \<^bold>\ r)\ + by (simp add: A1') + +lemma topoS4_conjElim: \\\<^sub>T\<^sub>o\<^sub>p (p \<^bold>\ q \<^bold>\ q)\ + by (simp add: A1') + +lemma topoS4_AxK: \\\<^sub>T\<^sub>o\<^sub>p (K i p \<^bold>\ K i (p \<^bold>\ q) \<^bold>\ K i q)\ +proof - + have \\\<^sub>T\<^sub>o\<^sub>p ((p \<^bold>\ (p \<^bold>\ q)) \<^bold>\ q)\ + using A1' by force + then have *: \\\<^sub>T\<^sub>o\<^sub>p (K i (p \<^bold>\ (p \<^bold>\ q)) \<^bold>\ K i q)\ + using RM by fastforce + then have \\\<^sub>T\<^sub>o\<^sub>p (K i p \<^bold>\ K i (p \<^bold>\ q) \<^bold>\ K i (p \<^bold>\ (p \<^bold>\ q)))\ + using AR topoS4_conjElim System_topoS4.simps by fast + then show ?thesis + by (meson "*" System_topoS4.R1' topoS4_trans) +qed + +lemma topoS4_NecR: + assumes \\\<^sub>T\<^sub>o\<^sub>p p\ + shows\\\<^sub>T\<^sub>o\<^sub>p K i p\ +proof - + have \\\<^sub>T\<^sub>o\<^sub>p (\<^bold>\ \<^bold>\ p)\ + using assms by (metis System_topoS4.A1' System_topoS4.R1' conjunct.simps(1) imply.simps(1) imply_conjunct) + then have \\\<^sub>T\<^sub>o\<^sub>p (K i \<^bold>\ \<^bold>\ K i p)\ + using RM by force + then show ?thesis + by (meson AN System_topoS4.R1') +qed + +lemma S4_topoS4: \\\<^sub>S\<^sub>4 p \ \\<^sub>T\<^sub>o\<^sub>p p\ +proof (induct p rule: AK.induct) + case (A2 i p q) + then show ?case using topoS4_AxK . +next + case (Ax p) + then show ?case + using AT' A4' by (metis AxT.cases Ax4.cases) +next + case (R2 p) + then show ?case + by (simp add: topoS4_NecR) +qed (meson System_topoS4.intros)+ + +lemma topoS4_S4: + fixes p :: \('i :: countable) fm\ + shows \\\<^sub>T\<^sub>o\<^sub>p p \ \\<^sub>S\<^sub>4 p\ +proof (induct p rule: System_topoS4.induct) + case (AT' i p) + then show ?case + by (simp add: Ax AxT.intros) +next + case (A4' i p) + then show ?case + by (simp add: Ax Ax4.intros) +next + case (AR i p q) + then show ?case + by (meson K_conj_imply_factor K_conjunction_in K_conjunction_out K_imp_trans' K_imply_multi R1) +next + case (AN i) + then have *: \\\<^sub>S\<^sub>4 \<^bold>\\ + by (simp add: A1) + then show ?case + by (simp add: * R2) +next + case (RM p q i) + then have \\\<^sub>S\<^sub>4 K i (p \<^bold>\ q)\ + by (simp add: R2) + then show ?case + by (simp add: K_map RM.hyps(2)) +qed (meson AK.intros)+ + +theorem main\<^sub>S\<^sub>4': \valid\<^sub>S\<^sub>4 p \ (\\<^sub>T\<^sub>o\<^sub>p p)\ + using main\<^sub>S\<^sub>4 S4_topoS4 topoS4_S4 by blast + +end diff --git a/thys/Stalnaker_Logic/document/root.bib b/thys/Stalnaker_Logic/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Stalnaker_Logic/document/root.bib @@ -0,0 +1,60 @@ +@inproceedings{From2021, + author = {Asta Halkjær From}, + journal = {International Workshop on Logic, Language, Information, and Computation}, + pages = {1-15}, + title = {Formalized soundness and completeness of epistemic logic}, + year = {2021}, +} +@article{EpistemicLogicAFP, + author = {Asta Halkjær From}, + title = {Epistemic Logic: Completeness of Modal Logics}, + journal = {Archive of Formal Proofs}, + month = oct, + year = 2018, + note = {\url{https://isa-afp.org/entries/Epistemic_Logic.html}, + Formal proof development}, + ISSN = {2150-914x}, +} +@article{Stalnaker2006, + author = {Robert Stalnaker}, + doi = {10.1007/S11098-005-4062-Y}, + issn = {00318116}, + issue = {1}, + journal = {Philosophical Studies}, + month = {3}, + pages = {169-199}, + title = {On logics of knowledge and belief}, + volume = {128}, + year = {2006}, +} +@book{lectureNotesStalnaker, + author = {Robert Stalnaker}, + title = {Lecture Notes | Modal Logic | Linguistics and Philosophy | MIT OpenCourseWare}, + url = {https://dspace.mit.edu/bitstream/handle/1721.1/100157/24-244-fall-2009/contents/lecture-notes/index.htm}, + year = {2009}, +} +@article{Aiello2003, + author = {Aiello, M.}, + doi = {10.1093/logcom/13.6.889}, + issn = {0955-792X}, + journal = {Journal of Logic and Computation}, + keywords = {Modal logic,Serial set,Spatial reasoning,Topo-bisimulation,Topological interpretation}, + month = {dec}, + number = {6}, + pages = {889--920}, + publisher = {Oxford Academic}, + title = {{Reasoning About Space: The Modal Way}}, + url = {https://academic.oup.com/logcom/article-lookup/doi/10.1093/logcom/13.6.889}, + volume = {13}, + year = {2003} +} +@book{chagrov1997modal, + title={Modal Logic}, + author={Chagrov, A. and Chagrov, P.M.A. and Zakharyaschev, M.}, + isbn={9780198537793}, + lccn={97185365}, + series={Oxford logic guides}, + url={https://books.google.com/books?id=dhgi5NF4RtcC}, + year={1997}, + publisher={Clarendon Press} +} diff --git a/thys/Stalnaker_Logic/document/root.tex b/thys/Stalnaker_Logic/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Stalnaker_Logic/document/root.tex @@ -0,0 +1,65 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} + %for \, \, \, \, \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{Stalnaker's Epistemic Logic} +\author{Laura P. Gamboa Guzman} +\maketitle + +\begin{abstract} + This work is a formalization of the knowledge fragment Stalnaker's epistemic logic with countably many agents and its soundness and completeness theorems \cite{Stalnaker2006, lectureNotesStalnaker, chagrov1997modal}, as well as the equivalence between the axiomatization of S4 available in the Epistemic Logic theory and the topological one \cite{Aiello2003}. It builds on the Epistemic Logic theory, as this includes the formalization of the completeness by canonicity proof for normal modal logics \cite{EpistemicLogicAFP, From2021}. +\end{abstract} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +\bibliographystyle{abbrv} +\nocite{*} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: