theory topo_alexandrov imports sse_operation_positive_quantification begin nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*) section ‹Generalized specialization orderings and Alexandrov topologies› text‹\noindent{A topology is called 'Alexandrov' (after the Russian mathematician Pavel Alexandrov) if the intersection (resp. union) of any (finite or infinite) family of open (resp. closed) sets is open (resp. closed); in algebraic terms, this means that the set of fixed points of the interior (closure) operation is closed under infinite meets (joins). Another common algebraic formulation requires the closure (interior) operation to satisfy the infinitary variants of additivity (multiplicativity), i.e. iADDI (iMULT) as introduced before. In the literature, the well-known Kuratowski conditions for the closure (resp. interior) operation are assumed, namely: ADDI, EXP, NOR, IDEM (resp. MULT, dEXP, dNOR, IDEM). This makes both formulations equivalent. However, this is not the case in general if those conditions become negotiable.}› text‹\noindent{Alexandrov topologies have interesting properties relating them to the semantics of modal logic. Assuming Kuratowski conditions, Alexandrov topological operations defined on subsets of S are in one-to-one correspondence with preorders on S; in topological terms, Alexandrov topologies are uniquely determined by their specialization preorders. Since we do not presuppose any Kuratowski conditions to begin with, the preorders in question are in general not even transitive. Here we just call them 'specialization relations'. We will still call (generalized) closure/interior-like operations as such (for lack of a better name). We explore minimal conditions under which some relevant results for the semantics of modal logic obtain.}› subsection ‹Specialization relations› text‹\noindent{Specialization relations (among worlds/points) are particular cases of propositional functions with type @{text "w⇒σ"}.}› text‹\noindent{Define some relevant properties of relations: }› abbreviation "serial R ≡ ∀x. ∃y. R x y" abbreviation "reflexive R ≡ ∀x. R x x" abbreviation "transitive R ≡ ∀x y z. R x y ∧ R y z ⟶ R x z" abbreviation "antisymmetric R ≡ ∀x y. R x y ∧ R y x ⟶ x = y" abbreviation "symmetric R ≡ ∀x y. R x y ⟶ R y x" text‹\noindent{Closure/interior operations can be derived from an arbitrary relation as operations returning down-/up-sets.}› definition Cl_rel::"(w⇒σ)⇒(σ⇒σ)" ("𝒞⇩_{R}") where "𝒞⇩_{R}R ≡ λA. λw. ∃v. R w v ∧ A v" definition Int_rel::"(w⇒σ)⇒(σ⇒σ)" ("ℐ⇩_{R}") where "ℐ⇩_{R}R ≡ λA. λw. ∀v. R w v ⟶ A v" text‹\noindent{Duality between interior and closure follows directly:}› lemma dual_rel1: "∀A. (𝒞⇩_{R}R) A ❙≈(ℐ⇩_{R}R)⇧^{d}A" unfolding Cl_rel_def Int_rel_def dual_def conn by simp lemma dual_rel2: "∀A. (ℐ⇩_{R}R) A ❙≈(𝒞⇩_{R}R)⇧^{d}A" unfolding Cl_rel_def Int_rel_def dual_def conn by simp text‹\noindent{We explore minimal conditions of the specialization relation under which some operation's conditions obtain.}› lemma rC1: "ADDI (𝒞⇩_{R}R)" unfolding Cl_rel_def ADDI_def conn by blast lemma rC1i:"iADDI (𝒞⇩_{R}R)" by (smt Cl_rel_def Ra_restr_ex iADDI_def supremum_def) lemma rC2: "reflexive R ⟶ EXP (𝒞⇩_{R}R)" unfolding EXP_def Cl_rel_def by auto lemma rC3: "NOR (𝒞⇩_{R}R)" unfolding Cl_rel_def NOR_def conn by blast lemma rC4: "reflexive R ∧ transitive R ⟶ IDEM (𝒞⇩_{R}R)" unfolding Cl_rel_def IDEM_def by smt lemma rC_Barcan: "∀π. (𝒞⇩_{R}R)(❙∃x. π x) ❙≼(❙∃x. (𝒞⇩_{R}R)(π x))" unfolding Cl_rel_def by auto lemma rI1: "MULT (ℐ⇩_{R}R)" unfolding Int_rel_def MULT_def conn by blast lemma rI1i:"iMULT (ℐ⇩_{R}R)" by (smt Int_rel_def Ra_restr_all iMULT_def infimum_def) lemma rI2: "reflexive R ⟹ dEXP (ℐ⇩_{R}R)" unfolding Int_rel_def dEXP_def Int_rel_def by auto lemma rI3: "dNOR (ℐ⇩_{R}R)" unfolding Int_rel_def dNOR_def conn by simp lemma rI4: "reflexive R ⟹ transitive R ⟹ IDEM (ℐ⇩_{R}R)" unfolding IDEM_def Int_rel_def by smt lemma rI_Barcan: "∀π. (❙∀x. (ℐ⇩_{R}R)(π x)) ❙≼(ℐ⇩_{R}R)(❙∀x. π x)" unfolding Int_rel_def by simp text‹\noindent{A specialization relation can be derived from a given operation (intended as a closure-like operation).}› definition sp_rel::"(σ⇒σ)⇒(w⇒σ)" ("ℛ⇧^{C}") where "ℛ⇧^{C}𝒞 ≡ λw v. 𝒞 (λu. u=v) w" text‹\noindent{Preorder properties of the specialization relation follow directly from the corresponding operation's conditions.}› lemma sp_rel_reflex: "EXP 𝒞 ⟹ reflexive (ℛ⇧^{C}𝒞)" by (simp add: EXP_def sp_rel_def) lemma sp_rel_trans: "MONO 𝒞 ⟹ IDEM 𝒞 ⟹ transitive (ℛ⇧^{C}𝒞)" by (smt IDEM_def MONO_def sp_rel_def) text‹\noindent{However, we can obtain finite countermodels for antisymmetry and symmetry given all relevant conditions. We will revisit this issue later and examine their relation with the topological separation axioms T0 and T1 resp.}› lemma "iADDI 𝒞 ⟹ EXP 𝒞 ⟹ NOR 𝒞 ⟹ IDEM 𝒞 ⟹ antisymmetric (ℛ⇧^{C}𝒞)" nitpick oops (*counterexample*) lemma "iADDI 𝒞 ⟹ EXP 𝒞 ⟹ NOR 𝒞 ⟹ IDEM 𝒞 ⟹ symmetric (ℛ⇧^{C}𝒞)" nitpick oops (*counterexample*) subsection ‹Alexandrov topology› text‹\noindent{As mentioned previously, Alexandrov closure (and by duality interior) operations correspond to specialization relations. It is worth mentioning that in Alexandrov topologies every point has a minimal/smallest neighborhood, namely the set of points related to it by the specialization (aka. accessibility) relation. Alexandrov spaces are thus also called 'finitely generated'. We examine below minimal conditions under which these relations obtain.}› lemma sp_rel_a: "MONO 𝒞 ⟹ ∀A. (𝒞⇩_{R}(ℛ⇧^{C}𝒞)) A ❙≼𝒞 A" by (smt Cl_rel_def MONO_def sp_rel_def) lemma sp_rel_b: "iADDI_a 𝒞 ⟹ ∀A. (𝒞⇩_{R}(ℛ⇧^{C}𝒞)) A ❙≽𝒞 A" proof - assume iaddia: "iADDI_a 𝒞" { fix A let ?S="λB::σ. ∃w::w. A w ∧ B=(λu. u=w)" have "A ❙≈(❙⋁?S)" using supremum_def by auto hence "𝒞(A) ❙≈𝒞(❙⋁?S)" by (smt eq_ext) moreover have "❙⋁Ra[𝒞|?S] ❙≈(𝒞⇩_{R}(ℛ⇧^{C}𝒞)) A" by (smt Cl_rel_def Ra_restr_ex sp_rel_def) moreover from iaddia have "𝒞(❙⋁?S) ❙≼❙⋁Ra[𝒞|?S]" unfolding iADDI_a_def by simp ultimately have "𝒞 A ❙≼(𝒞⇩_{R}(ℛ⇧^{C}𝒞)) A" by simp } thus ?thesis by simp qed lemma sp_rel: "iADDI 𝒞 ⟹ ∀A. 𝒞 A ❙≈(𝒞⇩_{R}(ℛ⇧^{C}𝒞)) A" by (metis MONO_iADDIb iADDI_a_def iADDI_b_def iADDI_def sp_rel_a sp_rel_b) text‹\noindent{It is instructive to expand the definitions in the above lemma:}› lemma "iADDI 𝒞 ⟹ ∀A. ∀w. (𝒞 A) w ⟷ (∃v. A v ∧ (𝒞 (λu. u=v)) w)" using Cl_rel_def sp_rel by fastforce text‹\noindent{We now turn to the more traditional characterization of Alexandrov topologies in terms of closure under infinite joins/meets.}› text‹\noindent{Fixed points of operations satisfying ADDI (MULT) are not in general closed under infinite joins (meets). For the given conditions countermodels are expected to be infinite. We (sanity) check that nitpick cannot find any.}› lemma "ADDI(φ) ⟹ supremum_closed (fp φ)" (*nitpick*) oops (*cannot find finite countermodels*) lemma "MULT(φ) ⟹ infimum_closed (fp φ)" (*nitpick*) oops (*cannot find finite countermodels*) text‹\noindent{By contrast, we can show that this obtains if assuming the corresponding infinitary variants (iADDI/iMULT).}› lemma "iADDI(φ) ⟹ supremum_closed (fp φ)" by (metis (full_types) Ra_restr_ex iADDI_def supremum_def) lemma "iMULT(φ) ⟹ infimum_closed (fp φ)" by (metis (full_types) Ra_restr_all iMULT_def infimum_def) text‹\noindent{As shown above, closure (interior) operations derived from relations readily satisfy iADDI (iMULT), being thus closed under infinite joins (meets).}› lemma "supremum_closed (fp (𝒞⇩_{R}R))" by (smt Cl_rel_def supremum_def) lemma "infimum_closed (fp (ℐ⇩_{R}R))" by (smt Int_rel_def infimum_def) subsection ‹(Anti)symmetry and the separation axioms T0 and T1› text‹\noindent{We can now revisit the relationship between (anti)symmetry and the separation axioms T1 and T0.}› text‹\noindent{T0: any two distinct points in the space can be separated by an open set (i.e. containing one point and not the other).}› abbreviation "T0_sep 𝒞 ≡ ∀w v. w ≠ v ⟶ (∃G. (fp 𝒞⇧^{d})(G) ∧ (G w ≠ G v))" text‹\noindent{T1: any two distinct points can be separated by (two not necessarily disjoint) open sets, i.e. all singletons are closed.}› abbreviation "T1_sep 𝒞 ≡ ∀w. (fp 𝒞)(λu. u = w)" text‹\noindent{We can (sanity) check that T1 entails T0 but not viceversa.}› lemma "T0_sep 𝒞 ⟹ T1_sep 𝒞" nitpick oops (*counterexample*) lemma "T1_sep 𝒞 ⟹ T0_sep 𝒞" by (smt compl_def dual_def dual_symm) text‹\noindent{Under appropriate conditions, T0-separation corresponds to antisymmetry of the specialization relation (here an ordering).}› lemma "T0_sep 𝒞 ⟷ antisymmetric (ℛ⇧^{C}𝒞)" nitpick oops (*counterexample*) lemma T0_antisymm_a: "MONO 𝒞 ⟹ T0_sep 𝒞 ⟶ antisymmetric (ℛ⇧^{C}𝒞)" by (smt Cl_rel_def compl_def dual_def sp_rel_a) lemma T0_antisymm_b: "EXP 𝒞 ⟹ IDEM 𝒞 ⟹ antisymmetric (ℛ⇧^{C}𝒞) ⟶ T0_sep 𝒞" by (metis (full_types) EXP_dual1 IDEM_def IDEM_dual2 IDEMa_def IDEMb_def compl_def dEXP_def dual_def dual_symm sp_rel_def) lemma T0_antisymm: "MONO 𝒞 ⟹ EXP 𝒞 ⟹ IDEM 𝒞 ⟹ T0_sep 𝒞 = antisymmetric (ℛ⇧^{C}𝒞)" by (metis T0_antisymm_a T0_antisymm_b) text‹\noindent{Also, under the appropriate conditions, T1-separation corresponds to symmetry of the specialization relation.}› lemma T1_symm_a: "T1_sep 𝒞 ⟶ symmetric (ℛ⇧^{C}𝒞)" using sp_rel_def by auto lemma T1_symm_b: "MONO 𝒞 ⟹ EXP 𝒞 ⟹ T0_sep 𝒞 ⟹ symmetric (ℛ⇧^{C}𝒞) ⟶ T1_sep 𝒞" by (metis T0_antisymm_a sp_rel_def sp_rel_reflex) lemma T1_symm: "MONO 𝒞 ⟹ EXP 𝒞 ⟹ T0_sep 𝒞 ⟹ symmetric (ℛ⇧^{C}𝒞) = T1_sep 𝒞" by (metis T1_symm_a T1_symm_b) end