diff --git a/thys/Topological_Semantics/ROOT b/thys/Topological_Semantics/ROOT --- a/thys/Topological_Semantics/ROOT +++ b/thys/Topological_Semantics/ROOT @@ -1,28 +1,25 @@ chapter AFP -session "Topological_Semantics" = "HOL" + +session "Topological_Semantics" (AFP) = "HOL" + options [timeout = 600] theories - sse_boolean_algebra - sse_boolean_algebra_quantification - sse_operation_positive - sse_operation_positive_quantification - sse_operation_negative - sse_operation_negative_quantification - topo_operators_basic - topo_operators_derivative - topo_alexandrov - topo_frontier_algebra - topo_negation_conditions - topo_negation_fixedpoints - ex_LFIs - topo_strict_implication - ex_subminimal_logics - topo_derivative_algebra - ex_LFUs - topo_border_algebra - topo_closure_algebra - topo_interior_algebra + boolean_algebra + boolean_algebra_infinitary + boolean_algebra_operators + conditions_positive + conditions_positive_infinitary + conditions_negative + conditions_negative_infinitary + conditions_relativized + conditions_relativized_infinitary + logics_consequence + logics_operators + logics_negation + logics_quantifiers + logics_quantifiers_example + logics_LFI + logics_LFU + document_files "root.tex" "root.bib" diff --git a/thys/Topological_Semantics/boolean_algebra.thy b/thys/Topological_Semantics/boolean_algebra.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/boolean_algebra.thy @@ -0,0 +1,203 @@ +theory boolean_algebra + imports Main +begin + +(*-----------------------------------*) +text\Technical configuration\ +declare[[smt_timeout=30]] +declare[[show_types]] +(* declare[[syntax_ambiguity_warning=false]] *) +sledgehammer_params[isar_proof=false] +nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3, atoms=a b c d] (*default Nitpick settings*) +text\We hide some Isabelle/HOL notation from the libraries (which we don't use) to avoid overloading\ +hide_const(open) List.list.Nil no_notation List.list.Nil ("[]") (*We have no use for lists... *) +hide_const(open) Relation.converse no_notation Relation.converse ("(_\)" [1000] 999) (*..nor for relations in this work*) +hide_const(open) Fun.comp no_notation Fun.comp (infixl "\" 55) (*we redefine function composition below*) +hide_const(open) Groups.plus_class.plus no_notation Groups.plus_class.plus (infixl "+" 65) (*we don't use this*) +hide_const(open) Groups.times_class.times no_notation Groups.times_class.times (infixl "*" 70) (*we don't use this*) +hide_const(open) Groups.minus_class.minus no_notation Groups.minus_class.minus (infixl "-" 65) (*we don't use this*) +hide_const(open) Groups.uminus_class.uminus no_notation Groups.uminus_class.uminus ("- _" [81] 80) (*we don't use this*) +(*-----------------------------------*) + +section \Shallow semantical embedding of (a logic of) Boolean algebras\ + +text\We encode Boolean algebras via their (Stone) representation as algebras of sets ('fields of sets'). +This means that each element of (the carrier of) the algebra will be a set of 'points'. +Inspired by the 'propositions as sets of worlds' paradigm from modal logic, we may think of points +as being 'worlds', and thus of the elements of our Boolean algebras as 'propositions'. +Of course, this is just one among many possible interpretations, and nothing stops us from thinking +of points as any other kind of object (e.g., they can be sets, functions, sets of functions, etc.). +\ + +text\We utilize a particular naming convention: The type parameter 'w is employed for the +domain/universe of 'points'. We conveniently introduce the (parametric) type-alias ('w)\ +as shorthand for 'w\bool. Hence, the elements of our algebra are objects of type ('w)\, +and thus correspond to (characteristic functions of) sets of 'points'. +Set-valued (resp. set-domain) functions are thus functions that have sets as their codomain (resp. domain), +they are basically anything with a (parametric) type 'a\('w)\ (resp. ('w)\\'a).\ + +text\Type for (characteristic functions of) sets (of 'points')\ +type_synonym 'w \ = \'w \ bool\ + +text\In the sequel, we will (try to) enforce the following naming convention:\ + +text\(i) Upper-case latin letters (A, B, D, M, P, S, X, etc.) denote arbitrary sets (type ('w)\). +We will employ lower-case letters (p, q, x, w, etc.) to denote variables playing the role of 'points'. +In some contexts, the letters S and D will be employed to denote sets/domains of sets (of 'points').\ + +text\(ii) Greek letters denote arbitrary set-valued functions (type 'a\('w)\). +We employ the letters \, \ and \ to denote arbitrary unary operations +(with type ('w)\\('w)\).\ + +text\(iii) Upper-case calligraphic letters (\, \, \, \, etc.) are reserved for unary operations that are +intended to act as 'topological operators' in the given context.\ + +subsection \Encoding Boolean operations\ + +text\Standard inclusion-based order structure on sets.\ +definition subset::"'w \ \ 'w \ \ bool" (infixr "\<^bold>\" 45) + where "A \<^bold>\ B \ \p. A p \ B p" +definition setequ::"'w \ \ 'w \ \ bool" (infixr "\<^bold>=" 45) + where "A \<^bold>= B \ \p. A p \ B p" + +named_theorems order (*to group together order-related definitions*) +declare setequ_def[order] subset_def[order] + +lemma subset_char1: "(A \<^bold>\ B) = (\C. B \<^bold>\ C \ A \<^bold>\ C)" by (metis subset_def) +lemma subset_char2: "(A \<^bold>\ B) = (\C. C \<^bold>\ A \ C \<^bold>\ B)" by (metis subset_def) + +text\These (trivial) lemmas are intended to help automated tools.\ +lemma setequ_char: "(A \<^bold>= B) = (A \<^bold>\ B \ B \<^bold>\ A)" unfolding order by blast +lemma setequ_ext: "(A \<^bold>= B) = (A = B)" unfolding order by blast + +text\We now encode connectives for (distributive and complemented) bounded lattices, mostly +by reusing their counterpart meta-logical HOL connectives.\ +definition meet::"'w \ \ 'w \ \ 'w \" (infixr "\<^bold>\" 54) + where "A \<^bold>\ B \ \p. (A p) \ (B p)" \\ intersection \ +definition join::"'w \ \ 'w \ \ 'w \" (infixr "\<^bold>\" 53) + where "A \<^bold>\ B \ \p. (A p) \ (B p)" \\ union \ +definition top::"'w \" ("\<^bold>\") + where "\<^bold>\ \ \w. True" \\ universe \ +definition bottom::"'w \" ("\<^bold>\") + where "\<^bold>\ \ \w. False" \\ empty-set \ + +text\And introduce further operations to obtain a Boolean algebra (of sets).\ +definition compl::"'w \ \ 'w \" ("\<^bold>\_" [57]58) + where "\<^bold>\A \ \p. \(A p)" \\ (set-)complement \ +definition impl::"'w \ \ 'w \ \ 'w \" (infixr "\<^bold>\" 51) + where "A \<^bold>\ B \ \p. (A p) \ (B p)" \\ (set-)implication \ +definition diff::"'w \ \ 'w \ \ 'w \" (infixr "\<^bold>\" 51) + where "A \<^bold>\ B \ \p. (A p) \ \(B p)" \\ (set-)difference \ +definition dimpl::"'w \ \ 'w \ \ 'w \" (infixr "\<^bold>\" 51) + where "A \<^bold>\ B \ \p. (A p) = (B p)" \\ double implication \ +definition sdiff::"'w \ \ 'w \ \ 'w \" (infixr "\<^bold>\" 51) + where "A \<^bold>\ B \ \p. (A p) \ (B p)" \\ symmetric difference (aka. xor) \ + +named_theorems conn (*to group together definitions for algebraic connectives*) +declare meet_def[conn] join_def[conn] top_def[conn] bottom_def[conn] + impl_def[conn] dimpl_def[conn] diff_def[conn] sdiff_def[conn] compl_def[conn] + +text\Verify characterization for some connectives.\ +lemma compl_char: "\<^bold>\A = A \<^bold>\ \<^bold>\" unfolding conn by simp +lemma impl_char: "A \<^bold>\ B = \<^bold>\A \<^bold>\ B" unfolding conn by simp +lemma dimpl_char: "A \<^bold>\ B = (A \<^bold>\ B) \<^bold>\ (B \<^bold>\ A)" unfolding conn by blast +lemma diff_char1: "A \<^bold>\ B = A \<^bold>\ \<^bold>\B" unfolding conn by simp +lemma diff_char2: "A \<^bold>\ B = \<^bold>\(A \<^bold>\ B)" unfolding conn by simp +lemma sdiff_char1: "A \<^bold>\ B = (A \<^bold>\ B) \<^bold>\ (B \<^bold>\ A)" unfolding conn by blast +lemma sdiff_char2: "A \<^bold>\ B = \<^bold>\(A \<^bold>\ B)" unfolding conn by simp + +text\We can verify that (quite trivially) this algebra satisfies some properties of lattices.\ +lemma L1: "A \<^bold>= A \<^bold>\ A" unfolding conn order by simp +lemma L2: "A \<^bold>= A \<^bold>\ A" unfolding conn order by simp +lemma L3: "A \<^bold>\ A \<^bold>\ B" unfolding conn order by simp +lemma L4: "A \<^bold>\ B \<^bold>\ A" unfolding conn order by simp +lemma L5: "(A \<^bold>\ B) \<^bold>\ B \<^bold>= B" unfolding setequ_char conn order by simp +lemma L6: "A \<^bold>\ (A \<^bold>\ B) \<^bold>= A" unfolding setequ_char conn order by simp +lemma L7: "A \<^bold>\ C \ B \<^bold>\ C \ A \<^bold>\ B \<^bold>\ C" unfolding conn order by simp +lemma L8: "C \<^bold>\ A \ C \<^bold>\ B \ C \<^bold>\ A \<^bold>\ B" unfolding conn order by simp +lemma L9: "A \<^bold>\ B \ (A \<^bold>\ B) \<^bold>= B" unfolding setequ_char conn order by simp +lemma L10: "B \<^bold>\ A \ (A \<^bold>\ B) \<^bold>= B" unfolding setequ_char conn order by simp +lemma L11: "A \<^bold>\ B \ C \<^bold>\ D \ A \<^bold>\ C \<^bold>\ B \<^bold>\ D" unfolding conn order by simp +lemma L12: "A \<^bold>\ B \ C \<^bold>\ D \ A \<^bold>\ C \<^bold>\ B \<^bold>\ D" unfolding conn order by simp +lemma L13: "A \<^bold>\ \<^bold>\ \<^bold>= A" unfolding conn order by simp +lemma L14: "A \<^bold>\ \<^bold>\ \<^bold>= A" unfolding conn order by simp +lemma L15: "A \<^bold>\ B \ (\C. C \<^bold>\ A \<^bold>\ C \<^bold>\ B)" by (metis L3 L4 L5 L8 setequ_char subset_char1) +lemma L16: "A \<^bold>\ B \ (\C. C \<^bold>\ A \<^bold>\ C \<^bold>\ B)" by (metis L11 L4 L5 setequ_char setequ_ext) + +text\These properties below hold in particular also for Boolean algebras.\ +lemma BA_impl: "A \<^bold>\ B \ A \<^bold>\ B \<^bold>= \<^bold>\" unfolding conn order by simp +lemma BA_distr1: "(A \<^bold>\ (B \<^bold>\ C)) \<^bold>= ((A \<^bold>\ B) \<^bold>\ (A \<^bold>\ C))" unfolding setequ_char conn order by simp +lemma BA_distr2: "(A \<^bold>\ (B \<^bold>\ C)) \<^bold>= ((A \<^bold>\ B) \<^bold>\ (A \<^bold>\ C))" unfolding conn order by blast +lemma BA_cp: "A \<^bold>\ B \ \<^bold>\B \<^bold>\ \<^bold>\A" unfolding conn order by blast +lemma BA_deMorgan1: "\<^bold>\(A \<^bold>\ B) \<^bold>= (\<^bold>\A \<^bold>\ \<^bold>\B)" unfolding conn order by simp +lemma BA_deMorgan2: "\<^bold>\(A \<^bold>\ B) \<^bold>= (\<^bold>\A \<^bold>\ \<^bold>\B)" unfolding conn order by simp +lemma BA_dn: "\<^bold>\\<^bold>\A \<^bold>= A" unfolding conn order by simp +lemma BA_cmpl_equ: "(\<^bold>\A \<^bold>= B) = (A \<^bold>= \<^bold>\B)" unfolding conn order by blast + + +text\We conveniently introduce these properties of sets of sets (of points).\ +definition meet_closed::"('w \)\ \ bool" + where "meet_closed S \ \X Y. (S X \ S Y) \ S(X \<^bold>\ Y)" +definition join_closed::"('w \)\ \ bool" + where "join_closed S \ \X Y. (S X \ S Y) \ S(X \<^bold>\ Y)" + +definition upwards_closed::"('w \)\ \ bool" + where "upwards_closed S \ \X Y. S X \ X \<^bold>\ Y \ S Y" +definition downwards_closed::"('w \)\ \ bool" + where "downwards_closed S \ \X Y. S X \ Y \<^bold>\ X \ S Y" + + +subsection \Atomicity and primitive equality\ + +text\We can verify indeed that the algebra is atomic (in three different ways) by relying on the +presence of primitive equality in HOL.\ + +lemma atomic1: "\w. \Q. Q w \ (\P. P w \ Q \<^bold>\ P)" unfolding order using the_sym_eq_trivial by metis + +definition "atom A \ \(A \<^bold>= \<^bold>\) \ (\P. A \<^bold>\ P \ A \<^bold>\ \<^bold>\P)" + +lemma atomic2: "\w. \Q. Q w \ atom Q" unfolding atom_def order conn using the_sym_eq_trivial by metis +lemma atomic3: "\P. \(P \<^bold>= \<^bold>\) \ (\Q. atom Q \ Q \<^bold>\ P)" unfolding atom_def order conn by fastforce + +text\Now with interactive proof:\ +lemma "\P. \(P \<^bold>= \<^bold>\) \ (\Q. atom Q \ Q \<^bold>\ P)" +proof - + { fix P::"'w \" + { assume "\(P \<^bold>= \<^bold>\)" + hence "\v. P v" unfolding conn order by simp + then obtain w where 1:"P w" by (rule exE) + let ?Q="\v. v = w" \\ using HOL primitive equality \ + have 2: "atom ?Q" unfolding atom_def unfolding conn order by simp + have "\v. ?Q v \ P v" using 1 by simp + hence 3: "?Q \<^bold>\ P" unfolding order by simp + from 2 3 have "\Q. atom Q \ Q \<^bold>\ P" by blast + } hence "\(P \<^bold>= \<^bold>\) \ (\Q. atom Q \ Q \<^bold>\ P)" by (rule impI) + } thus ?thesis by (rule allI) +qed + +subsection \Miscellaneous notions\ + +text\We add some miscellaneous notions that will be useful later.\ + +abbreviation "isEmpty S \ \x. \S x" +abbreviation "nonEmpty S \ \x. S x" + +text\Function composition.\ +definition fun_comp :: "('b \ 'c) \ ( 'a \ 'b) \ 'a \ 'c" (infixl "\" 75) + where "\ \ \ \ \x. \ (\ x)" + +text\Inverse projection maps a unary function to a 'projected' binary function wrt. its 1st argument.\ +abbreviation inv_proj::\('a \ 'c) \ ('a \ 'b \ 'c)\ ("(_)\") + where "D\ \ \A B. D A" + +text\Image of a mapping \, with range as an special case.\ +definition image::"('a \ 'b) \ ('a \ bool) \ ('b \ bool)" ("\_ _\") + where "\\ S\ \ \y. \x. (S x) \ (\ x) = y" +definition range::"('a \ 'b) \ ('b \ bool)" ("\_'_\") + where "\\ _\ \ \Y. \x. (\ x) = Y" +lemma range_char1: "\\ _\ = \\ (\x. True)\" by (simp add: image_def range_def) +lemma range_char2: "\\ _\ = (\X. \S. \\ S\ X)" unfolding range_def image_def by blast + +lemma image_comp: "\(f \ g) S\ = \f \g S\\" unfolding fun_comp_def image_def by metis + +end diff --git a/thys/Topological_Semantics/boolean_algebra_infinitary.thy b/thys/Topological_Semantics/boolean_algebra_infinitary.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/boolean_algebra_infinitary.thy @@ -0,0 +1,130 @@ +theory boolean_algebra_infinitary + imports boolean_algebra_operators +begin + +subsection \Encoding infinitary Boolean operations\ + +text\Our aim is to encode complete Boolean algebras (of sets) which we can later be used to +interpret quantified formulas (somewhat in the spirit of Boolean-valued models for set theory).\ + +text\We start by defining infinite meet (infimum) and infinite join (supremum) operations.\ +definition infimum:: "('w \)\ \ 'w \" ("\<^bold>\_") + where "\<^bold>\S \ \w. \X. S X \ X w" +definition supremum::"('w \)\ \ 'w \" ("\<^bold>\_") + where "\<^bold>\S \ \w. \X. S X \ X w" + +declare infimum_def[conn] supremum_def[conn] (*add infimum and supremum to definition set of algebra connectives*) + +text\Infimum and supremum satisfy an infinite variant of the De Morgan laws.\ +lemma iDM_a: "\<^bold>\(\<^bold>\S) \<^bold>= \<^bold>\(S\<^sup>d\<^sup>-)" unfolding order conn conn2 by force +lemma iDM_b:" \<^bold>\(\<^bold>\S) \<^bold>= \<^bold>\(S\<^sup>d\<^sup>-)" unfolding order conn conn2 by force + +text\We show that our encoded Boolean algebras are lattice-complete. +The functions below return the set of upper-/lower-bounds of a set of sets S (wrt. domain D).\ +definition upper_bounds::"('w \)\ \ ('w \)\" ("ub") + where "ub S \ \U. \X. S X \ X \<^bold>\ U" +definition upper_bounds_restr::"('w \)\ \ ('w \)\ \ ('w \)\" ("ub\<^sup>_") + where "ub\<^sup>D S \ \U. D U \ (\X. S X \ X \<^bold>\ U)" +definition lower_bounds::"('w \)\ \ ('w \)\" ("lb") + where "lb S \ \L. \X. S X \ L \<^bold>\ X" +definition lower_bounds_restr::"('w \)\ \ ('w \)\ \ ('w \)\" ("lb\<^sup>_") + where "lb\<^sup>D S \ \L. D L \ (\X. S X \ L \<^bold>\ X)" + +lemma ub_char: "ub S = (let D=\<^bold>\ in ub\<^sup>D S) " by (simp add: top_def upper_bounds_def upper_bounds_restr_def) +lemma lb_char: "lb S = (let D=\<^bold>\ in lb\<^sup>D S) " by (simp add: top_def lower_bounds_def lower_bounds_restr_def) + +text\Similarly, the functions below return the set of least/greatest upper-/lower-bounds for S (wrt. D).\ +definition lub::"('w \)\ \ ('w \)\" ("lub") + where "lub S \ \U. ub S U \ (\X. ub S X \ U \<^bold>\ X)" +definition lub_restr::"('w \)\ \ ('w \)\ \ ('w \)\" ("lub\<^sup>_") + where "lub\<^sup>D S \ \U. ub\<^sup>D S U \ (\X. ub\<^sup>D S X \ U \<^bold>\ X)" +definition glb::"('w \)\ \ ('w \)\" ("glb") + where "glb S \ \L. lb S L \ (\X. lb S X \ X \<^bold>\ L)" +definition glb_restr::"('w \)\ \ ('w \)\ \ ('w \)\" ("glb\<^sup>_") + where "glb\<^sup>D S \ \L. lb\<^sup>D S L \ (\X. lb\<^sup>D S X \ X \<^bold>\ L)" + +text\Both pairs of definitions above are suitably related. +(Note that the term \ below denotes the top element in the algebra of sets of sets (i.e. the powerset).)\ +lemma lub_char: "lub S = (let D=\<^bold>\ in lub\<^sup>D S) " by (simp add: lub_def lub_restr_def ub_char) +lemma glb_char: "glb S = (let D=\<^bold>\ in glb\<^sup>D S) " by (simp add: glb_def glb_restr_def lb_char) + +text\Clearly, the notions of infimum/supremum correspond to least/greatest upper-/lower-bound.\ +lemma sup_lub: "lub S \<^bold>\S" unfolding lub_def upper_bounds_def supremum_def subset_def by blast +lemma sup_exist_unique: "\S. \!X. lub S X" by (meson lub_def setequ_char setequ_ext sup_lub) +lemma inf_glb: "glb S \<^bold>\S" unfolding glb_def lower_bounds_def infimum_def subset_def by blast +lemma inf_exist_unique: "\S. \!X. glb S X" by (meson glb_def inf_glb setequ_char setequ_ext) + +text\The property of being closed under arbitrary (resp. nonempty) supremum/infimum.\ +definition infimum_closed :: "('w \)\ \ bool" + where "infimum_closed S \ \D. D \<^bold>\ S \ S(\<^bold>\D)" (*observe that D can be empty*) +definition supremum_closed :: "('w \)\ \ bool" + where "supremum_closed S \ \D. D \<^bold>\ S \ S(\<^bold>\D)" (*observe that D can be empty*) +definition infimum_closed' :: "('w \)\ \ bool" + where"infimum_closed' S \ \D. nonEmpty D \ D \<^bold>\ S \ S(\<^bold>\D)" +definition supremum_closed' :: "('w \)\ \ bool" + where "supremum_closed' S \ \D. nonEmpty D \ D \<^bold>\ S \ S(\<^bold>\D)" + +lemma inf_empty: "isEmpty S \ \<^bold>\S \<^bold>= \<^bold>\" unfolding order conn by simp +lemma sup_empty: "isEmpty S \ \<^bold>\S \<^bold>= \<^bold>\" unfolding order conn by simp + +text\Note that arbitrary infimum- (resp. supremum-) closed sets include the top (resp. bottom) element.\ +lemma "infimum_closed S \ S \<^bold>\" unfolding infimum_closed_def conn order by force +lemma "supremum_closed S \ S \<^bold>\" unfolding supremum_closed_def conn order by force +text\However, the above does not hold for non-empty infimum- (resp. supremum-) closed sets.\ +lemma "infimum_closed' S \ S \<^bold>\" nitpick oops \\ countermodel \ +lemma "supremum_closed' S \ S \<^bold>\" nitpick oops \\ countermodel \ + +text\We have in fact the following characterizations for the notions above.\ +lemma inf_closed_char: "infimum_closed S = (infimum_closed' S \ S \<^bold>\)" + unfolding infimum_closed'_def infimum_closed_def by (metis bottom_def infimum_closed_def infimum_def setequ_char setequ_ext subset_def top_def) +lemma sup_closed_char: "supremum_closed S = (supremum_closed' S \ S \<^bold>\)" + unfolding supremum_closed'_def supremum_closed_def by (metis (no_types, opaque_lifting) L14 L9 bottom_def setequ_ext subset_def supremum_def) + +lemma inf_sup_closed_dc: "infimum_closed S = supremum_closed S\<^sup>d\<^sup>-" by (smt (verit) BA_dn iDM_a iDM_b infimum_closed_def setequ_ext sdfun_dcompl_def subset_def supremum_closed_def) +lemma inf_sup_closed_dc': "infimum_closed' S = supremum_closed' S\<^sup>d\<^sup>-" by (smt (verit) dualcompl_invol iDM_a infimum_closed'_def sdfun_dcompl_def setequ_ext subset_def supremum_closed'_def) + +text\We check some further properties.\ +lemma fp_inf_sup_closed_dual: "infimum_closed (fp \) = supremum_closed (fp \\<^sup>d)" + by (simp add: fp_dual inf_sup_closed_dc) +lemma fp_inf_sup_closed_dual': "infimum_closed' (fp \) = supremum_closed' (fp \\<^sup>d)" + by (simp add: fp_dual inf_sup_closed_dc') + +text\We verify that being infimum-closed' (resp. supremum-closed') entails being meet-closed (resp. join-closed).\ +lemma inf_meet_closed: "\S. infimum_closed' S \ meet_closed S" proof - + { fix S::"'w \ \ bool" + { assume inf_closed: "infimum_closed' S" + hence "meet_closed S" proof - + { fix X::"'w \" and Y::"'w \" + let ?D="\Z. Z=X \ Z=Y" + { assume "S X \ S Y" + hence "?D \<^bold>\ S" using subset_def by blast + moreover have "nonEmpty ?D" by auto + ultimately have "S(\<^bold>\?D)" using inf_closed infimum_closed'_def by (smt (z3)) + hence "S(\w. \Z. (Z=X \ Z=Y) \ Z w)" unfolding infimum_def by simp + moreover have "(\w. \Z. (Z=X \ Z=Y) \ Z w) = (\w. X w \ Y w)" by auto + ultimately have "S(\w. X w \ Y w)" by simp + } hence "(S X \ S Y) \ S(X \<^bold>\ Y)" unfolding conn by (rule impI) + } thus ?thesis unfolding meet_closed_def by simp qed + } hence "infimum_closed' S \ meet_closed S" by simp + } thus ?thesis by (rule allI) +qed +lemma sup_join_closed: "\P. supremum_closed' P \ join_closed P" proof - + { fix S::"'w \ \ bool" + { assume sup_closed: "supremum_closed' S" + hence "join_closed S" proof - + { fix X::"'w \" and Y::"'w \" + let ?D="\Z. Z=X \ Z=Y" + { assume "S X \ S Y" + hence "?D \<^bold>\ S" using subset_def by blast + moreover have "nonEmpty ?D" by auto + ultimately have "S(\<^bold>\?D)" using sup_closed supremum_closed'_def by (smt (z3)) + hence "S(\w. \Z. (Z=X \ Z=Y) \ Z w)" unfolding supremum_def by simp + moreover have "(\w. \Z. (Z=X \ Z=Y) \ Z w) = (\w. X w \ Y w)" by auto + ultimately have "S(\w. X w \ Y w)" by simp + } hence "(S X \ S Y) \ S(X \<^bold>\ Y)" unfolding conn by (rule impI) + } thus ?thesis unfolding join_closed_def by simp qed + } hence "supremum_closed' S \ join_closed S" by simp + } thus ?thesis by (rule allI) +qed + +end diff --git a/thys/Topological_Semantics/boolean_algebra_operators.thy b/thys/Topological_Semantics/boolean_algebra_operators.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/boolean_algebra_operators.thy @@ -0,0 +1,155 @@ +theory boolean_algebra_operators + imports boolean_algebra +begin + +subsection \Operations on set-valued functions\ + +text\Functions with sets in their codomain will be called here 'set-valued functions'. + We conveniently define some (2nd-order) Boolean operations on them.\ + +text\The 'meet' and 'join' of two set-valued functions.\ +definition svfun_meet::"('a \ 'w \) \ ('a \ 'w \) \ ('a \ 'w \)" (infixr "\<^bold>\\<^sup>:" 62) + where "\ \<^bold>\\<^sup>: \ \ \x. (\ x) \<^bold>\ (\ x)" +definition svfun_join::"('a \ 'w \) \ ('a \ 'w \) \ ('a \ 'w \)" (infixr "\<^bold>\\<^sup>:" 61) + where "\ \<^bold>\\<^sup>: \ \ \x. (\ x) \<^bold>\ (\ x)" +text\Analogously, we can define an 'implication' and a 'complement'.\ +definition svfun_impl::"('a \ 'w \) \ ('a \ 'w \) \ ('a \ 'w \)" (infixr "\<^bold>\\<^sup>:" 61) + where "\ \<^bold>\\<^sup>: \ \ \x. (\ x) \<^bold>\ (\ x)" +definition svfun_compl::"('a \ 'w \) \ ('a \ 'w \)" ("(_\<^sup>-)") + where "\\<^sup>- \ \x. \<^bold>\(\ x)" +text\There are two natural 0-ary connectives (aka. constants). \ +definition svfun_top::"'a \ 'w \" ("\<^bold>\\<^sup>:") + where "\<^bold>\\<^sup>: \ \x. \<^bold>\" +definition svfun_bot::"'a \ 'w \" ("\<^bold>\\<^sup>:") + where "\<^bold>\\<^sup>: \ \x. \<^bold>\" + +named_theorems conn2 (*to group together definitions for 2nd-order algebraic connectives*) +declare svfun_meet_def[conn2] svfun_join_def[conn2] svfun_impl_def[conn2] + svfun_compl_def[conn2] svfun_top_def[conn2] svfun_bot_def[conn2] + +text\And, of course, set-valued functions are naturally ordered in the expected way:\ +definition svfun_sub::"('a \ 'w \) \ ('a \ 'w \) \ bool" (infixr "\<^bold>\\<^sup>:" 55) + where "\ \<^bold>\\<^sup>: \ \ \x. (\ x) \<^bold>\ (\ x)" +definition svfun_equ::"('a \ 'w \) \ ('a \ 'w \) \ bool" (infixr "\<^bold>=\<^sup>:" 55) + where "\ \<^bold>=\<^sup>: \ \ \x. (\ x) \<^bold>= (\ x)" + +named_theorems order2 (*to group together definitions for 2nd-order algebraic connectives*) +declare svfun_sub_def[order2] svfun_equ_def[order2] + +text\These (trivial) lemmas are intended to help automated tools.\ +lemma svfun_sub_char: "(\ \<^bold>\\<^sup>: \) = (\ \<^bold>\\<^sup>: \ \<^bold>=\<^sup>: \<^bold>\\<^sup>:)" by (simp add: BA_impl svfun_equ_def svfun_impl_def svfun_sub_def svfun_top_def) +lemma svfun_equ_char: "(\ \<^bold>=\<^sup>: \) = (\ \<^bold>\\<^sup>: \ \ \ \<^bold>\\<^sup>: \)" unfolding order2 setequ_char by blast +lemma svfun_equ_ext: "(\ \<^bold>=\<^sup>: \) = (\ = \)" by (meson ext setequ_ext svfun_equ_def) + +text\Clearly, set-valued functions form a Boolean algebra. We can prove some interesting relationships:\ +lemma svfun_compl_char: "\\<^sup>- = (\ \<^bold>\\<^sup>: \<^bold>\\<^sup>:)" unfolding conn conn2 by simp +lemma svfun_impl_char1: "(\ \<^bold>\\<^sup>: \) = (\\<^sup>- \<^bold>\\<^sup>: \)" unfolding conn conn2 by simp +lemma svfun_impl_char2: "(\ \<^bold>\\<^sup>: \) = (\ \<^bold>\\<^sup>: (\\<^sup>-))\<^sup>-" unfolding conn conn2 by simp +lemma svfun_deMorgan1: "(\ \<^bold>\\<^sup>: \)\<^sup>- = (\\<^sup>-) \<^bold>\\<^sup>: (\\<^sup>-)" unfolding conn conn2 by simp +lemma svfun_deMorgan2: "(\ \<^bold>\\<^sup>: \)\<^sup>- = (\\<^sup>-) \<^bold>\\<^sup>: (\\<^sup>-)" unfolding conn conn2 by simp + + +subsection \Operators and their transformations\ + +text\Dual to set-valued functions we can have set-domain functions. For them we can define the 'dual-complement'.\ +definition sdfun_dcompl::"('w \ \ 'a) \ ('w \ \ 'a)" ("(_\<^sup>d\<^sup>-)") + where "\\<^sup>d\<^sup>- \ \X. \(\<^bold>\X)" +lemma sdfun_dcompl_char: "\\<^sup>d\<^sup>- = (\X. \Y. (\ Y) \ (X = \<^bold>\Y))" by (metis BA_dn setequ_ext sdfun_dcompl_def) + +text\Operators are a particularly important kind of functions. They are both set-valued and set-domain. +Thus our algebra of operators inherits the connectives defined above plus the ones below. \ + +text\We conveniently define the 'dual' of an operator.\ +definition op_dual::"('w \ \ 'w \) \ ('w \ \ 'w \)" ("(_\<^sup>d)") + where "\\<^sup>d \ \X. \<^bold>\(\(\<^bold>\X))" + +text\The following two 0-ary connectives (i.e. operator 'constants') exist already (but somehow implicitly). + We just make them explicit by introducing some convenient notation.\ +definition id_op::"'w \ \ 'w \" ("\<^bold>e") + where "\<^bold>e \ \X. X" (*introduces notation to refer to 'identity' operator*) +definition compl_op::"'w \ \ 'w \" ("\<^bold>n") + where "\<^bold>n \ \X. \<^bold>\X" (*to refer to 'complement' operator*) + +declare sdfun_dcompl_def[conn2] op_dual_def[conn2] id_op_def[conn2] compl_op_def[conn2] + +text\We now prove some lemmas (some of them might help provers in their hard work).\ +lemma dual_compl_char1: "\\<^sup>d\<^sup>- = (\\<^sup>d)\<^sup>-" unfolding conn2 conn order by simp +lemma dual_compl_char2: "\\<^sup>d\<^sup>- = (\\<^sup>-)\<^sup>d" unfolding conn2 conn order by simp +lemma sfun_compl_invol: "\\<^sup>-\<^sup>- = \" unfolding conn2 conn order by simp +lemma dual_invol: "\\<^sup>d\<^sup>d = \" unfolding conn2 conn order by simp +lemma dualcompl_invol: "(\\<^sup>d\<^sup>-)\<^sup>d\<^sup>- = \" unfolding conn2 conn order by simp + +lemma op_prop1: "\<^bold>e\<^sup>d = \<^bold>e" unfolding conn2 conn by simp +lemma op_prop2: "\<^bold>n\<^sup>d = \<^bold>n" unfolding conn2 conn by simp +lemma op_prop3: "\<^bold>e\<^sup>- = \<^bold>n" unfolding conn2 conn by simp +lemma op_prop4: "(\ \<^bold>\\<^sup>: \)\<^sup>d = (\\<^sup>d) \<^bold>\\<^sup>: (\\<^sup>d)" unfolding conn2 conn by simp +lemma op_prop5: "(\ \<^bold>\\<^sup>: \)\<^sup>- = (\\<^sup>-) \<^bold>\\<^sup>: (\\<^sup>-)" unfolding conn2 conn by simp +lemma op_prop6: "(\ \<^bold>\\<^sup>: \)\<^sup>d = (\\<^sup>d) \<^bold>\\<^sup>: (\\<^sup>d)" unfolding conn2 conn by simp +lemma op_prop7: "(\ \<^bold>\\<^sup>: \)\<^sup>- = (\\<^sup>-) \<^bold>\\<^sup>: (\\<^sup>-)" unfolding conn2 conn by simp +lemma op_prop8: "\<^bold>\\<^sup>: = \<^bold>n \<^bold>\\<^sup>: \<^bold>e" unfolding conn2 conn by simp +lemma op_prop9: "\<^bold>\\<^sup>: = \<^bold>n \<^bold>\\<^sup>: \<^bold>e" unfolding conn2 conn by simp + +text\The notion of a fixed-point is fundamental. We speak of sets being fixed-points of operators. +We define a function that given an operator returns the set of all its fixed-points.\ +definition fixpoints::"('w \ \ 'w \) \ ('w \)\" ("fp") + where "fp \ \ \X. (\ X) \<^bold>= X" +text\We can in fact 'operationalize' the function above, thus obtaining a 'fixed-point operation'.\ +definition op_fixpoint::"('w \ \ 'w \) \ ('w \ \ 'w \)" ("(_\<^sup>f\<^sup>p)") + where "\\<^sup>f\<^sup>p \ \X. (\ X) \<^bold>\ X" + +declare fixpoints_def[conn2] op_fixpoint_def[conn2] + +text\Interestingly, the fixed-point operation (or transformation) is definable in terms of the others.\ +lemma op_fixpoint_char: "\\<^sup>f\<^sup>p = (\ \<^bold>\\<^sup>: \<^bold>e) \<^bold>\\<^sup>: (\\<^sup>- \<^bold>\\<^sup>: \<^bold>n)" unfolding conn2 order conn by blast + +text\Given an operator \ the fixed-points of \'s dual is the set of complements of \'s fixed-points.\ +lemma fp_dual: "fp \\<^sup>d = (fp \)\<^sup>d\<^sup>-" unfolding order conn conn2 by blast +text\The fixed-points of \'s complement is the set of complements of the fixed-points of \'s dual-complement.\ +lemma fp_compl: "fp \\<^sup>- = (fp (\\<^sup>d\<^sup>-))\<^sup>d\<^sup>-" by (simp add: dual_compl_char2 dualcompl_invol fp_dual) +text\The fixed-points of \'s dual-complement is the set of complements of the fixed-points of \'s complement.\ +lemma fp_dcompl: "fp (\\<^sup>d\<^sup>-) = (fp \\<^sup>-)\<^sup>d\<^sup>-" by (simp add: dualcompl_invol fp_compl) + +text\The fixed-points function and the fixed-point operation are essentially related.\ +lemma fp_rel: "fp \ A \ (\\<^sup>f\<^sup>p A) \<^bold>= \<^bold>\" unfolding conn2 order conn by simp +lemma fp_d_rel: "fp \\<^sup>d A \ \\<^sup>f\<^sup>p(\<^bold>\A) \<^bold>= \<^bold>\" unfolding conn2 order conn by blast +lemma fp_c_rel: "fp \\<^sup>- A \ \\<^sup>f\<^sup>p A \<^bold>= \<^bold>\" unfolding conn2 order conn by blast +lemma fp_dc_rel: "fp (\\<^sup>d\<^sup>-) A \ \\<^sup>f\<^sup>p(\<^bold>\A) \<^bold>= \<^bold>\" unfolding conn2 order conn by simp + +text\The fixed-point operation is involutive.\ +lemma ofp_invol: "(\\<^sup>f\<^sup>p)\<^sup>f\<^sup>p = \" unfolding conn2 order conn by blast +text\And commutes the dual with the dual-complement operations.\ +lemma ofp_comm_dc1: "(\\<^sup>d)\<^sup>f\<^sup>p = (\\<^sup>f\<^sup>p)\<^sup>d\<^sup>-" unfolding conn2 order conn by blast +lemma ofp_comm_dc2:"(\\<^sup>d\<^sup>-)\<^sup>f\<^sup>p = (\\<^sup>f\<^sup>p)\<^sup>d" unfolding conn2 order conn by simp + +text\The fixed-point operation commutes with the complement.\ +lemma ofp_comm_compl: "(\\<^sup>-)\<^sup>f\<^sup>p = (\\<^sup>f\<^sup>p)\<^sup>-" unfolding conn2 order conn by blast +text\The above motivates the following alternative definition for a 'complemented-fixed-point' operation.\ +lemma ofp_fixpoint_compl_def: "\\<^sup>f\<^sup>p\<^sup>- = (\X. (\ X) \<^bold>\ X)" unfolding conn2 conn by simp +text\Analogously, the 'complemented fixed-point' operation is also definable in terms of the others.\ +lemma op_fixpoint_compl_char: "\\<^sup>f\<^sup>p\<^sup>- = (\ \<^bold>\\<^sup>: \<^bold>e) \<^bold>\\<^sup>: (\\<^sup>- \<^bold>\\<^sup>: \<^bold>n)" unfolding conn2 conn by blast + +text\In fact, function composition can be seen as an additional binary connective for operators. + We show below some interesting relationships that hold. \ +lemma op_prop10: "\ = (\<^bold>e \ \)" unfolding conn2 fun_comp_def by simp +lemma op_prop11: "\ = (\ \ \<^bold>e)" unfolding conn2 fun_comp_def by simp +lemma op_prop12: "\<^bold>e = (\<^bold>n \ \<^bold>n)" unfolding conn2 conn fun_comp_def by simp +lemma op_prop13: "\\<^sup>- = (\<^bold>n \ \)" unfolding conn2 fun_comp_def by simp +lemma op_prop14: "\\<^sup>d\<^sup>- = (\ \ \<^bold>n)" unfolding conn2 fun_comp_def by simp +lemma op_prop15: "\\<^sup>d = (\<^bold>n \ \ \ \<^bold>n)" unfolding conn2 fun_comp_def by simp + +text\There are also some useful properties regarding the images of operators.\ +lemma im_prop1: "\\ D\\<^sup>d\<^sup>- = \\\<^sup>d D\<^sup>d\<^sup>-\" unfolding image_def op_dual_def sdfun_dcompl_def by (metis BA_dn setequ_ext) +lemma im_prop2: "\\\<^sup>- D\\<^sup>d\<^sup>- = \\ D\" unfolding image_def svfun_compl_def sdfun_dcompl_def by (metis BA_dn setequ_ext) +lemma im_prop3: "\\\<^sup>d D\\<^sup>d\<^sup>- = \\ D\<^sup>d\<^sup>-\" unfolding image_def op_dual_def sdfun_dcompl_def by (metis BA_dn setequ_ext) +lemma im_prop4: "\\\<^sup>d\<^sup>- D\\<^sup>d\<^sup>- = \\\<^sup>d D\" unfolding image_def op_dual_def sdfun_dcompl_def by (metis BA_dn setequ_ext) +lemma im_prop5: "\\\<^sup>- D\<^sup>d\<^sup>-\ = \\\<^sup>d\<^sup>- D\\<^sup>d\<^sup>-" unfolding image_def svfun_compl_def sdfun_dcompl_def by (metis (no_types, opaque_lifting) BA_dn setequ_ext) +lemma im_prop6: "\\\<^sup>d\<^sup>- D\<^sup>d\<^sup>-\ = \\ D\" unfolding image_def sdfun_dcompl_def by (metis BA_dn setequ_ext) + + +text\Observe that all results obtained by assuming fixed-point predicates extend to their associated operators.\ +lemma "\\<^sup>f\<^sup>p(A) \<^bold>\ \(A) \<^bold>\ \(A) \ (fp \)(A) \ \(A) \<^bold>\ \(A)" + by (simp add: fp_rel meet_def setequ_ext subset_def top_def) +lemma "\\<^sup>f\<^sup>p(A) \<^bold>\ \\<^sup>f\<^sup>p(B) \<^bold>\ (\ A B) \<^bold>\ (\ A B) \ (fp \)(A) \ (fp \)(B) \ (\ A B) \<^bold>\ (\ A B)" + by (simp add: fp_rel meet_def setequ_ext subset_def top_def) + +end diff --git a/thys/Topological_Semantics/conditions_negative.thy b/thys/Topological_Semantics/conditions_negative.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/conditions_negative.thy @@ -0,0 +1,149 @@ +theory conditions_negative + imports conditions_positive +begin + +subsection \Negative Conditions\ + +text\We continue defining and interrelating axiomatic conditions on unary operations (operators). + We now move to conditions commonly satisfied by negation-like logical operations.\ + +text\Anti-tonicity (ANTI).\ +definition ANTI::"('w \ \ 'w \) \ bool" ("ANTI") + where "ANTI \ \ \A B. A \<^bold>\ B \ \ B \<^bold>\ \ A" + +declare ANTI_def[cond] + +text\ANTI is self-dual.\ +lemma ANTI_dual: "ANTI \ = ANTI \\<^sup>d" by (smt (verit) BA_cp ANTI_def dual_invol op_dual_def) +text\ANTI is the 'complement' of MONO.\ +lemma ANTI_MONO: "MONO \ = ANTI \\<^sup>-" by (metis ANTI_def BA_cp MONO_def svfun_compl_def) + + +text\Anti-expansive/extensive (nEXPN) and its dual anti-contractive (nCNTR).\ +definition nEXPN::"('w \ \ 'w \) \ bool" ("nEXPN") + where "nEXPN \ \ \A. \ A \<^bold>\ \<^bold>\A" +definition nCNTR::"('w \ \ 'w \) \ bool" ("nCNTR") + where "nCNTR \ \ \A. \<^bold>\A \<^bold>\ \ A" + +declare nEXPN_def[cond] nCNTR_def[cond] + +text\nEXPN and nCNTR are dual to each other.\ +lemma nEXPN_nCNTR_dual1: "nEXPN \ = nCNTR \\<^sup>d" unfolding cond by (metis BA_cp BA_dn op_dual_def setequ_ext) +lemma nEXPN_nCNTR_dual2: "nCNTR \ = nEXPN \\<^sup>d" by (simp add: dual_invol nEXPN_nCNTR_dual1) + +text\nEXPN and nCNTR are the 'complements' of EXPN and CNTR respectively.\ +lemma nEXPN_CNTR_compl: "EXPN \ = nEXPN \\<^sup>-" by (metis BA_cp EXPN_def nEXPN_def svfun_compl_def) +lemma nCNTR_EXPN_compl: "CNTR \ = nCNTR \\<^sup>-" by (metis EXPN_CNTR_dual2 dual_compl_char1 dual_compl_char2 nEXPN_CNTR_compl nEXPN_nCNTR_dual2) + +text\Anti-Normality (nNORM) and its dual (nDNRM).\ +definition nNORM::"('w \ \ 'w \) \ bool" ("nNORM") + where "nNORM \ \ (\ \<^bold>\) \<^bold>= \<^bold>\" +definition nDNRM::"('w \ \ 'w \) \ bool" ("nDNRM") + where "nDNRM \ \ (\ \<^bold>\) \<^bold>= \<^bold>\" + +declare nNORM_def[cond] nDNRM_def[cond] + +text\nNORM and nDNRM are dual to each other.\ +lemma nNOR_dual1: "nNORM \ = nDNRM \\<^sup>d" unfolding cond by (simp add: bottom_def compl_def op_dual_def setequ_def top_def) +lemma nNOR_dual2: "nDNRM \ = nNORM \\<^sup>d" by (simp add: dual_invol nNOR_dual1) + +text\nNORM and nDNRM are the 'complements' of NORM and DNRM respectively.\ +lemma nNORM_NORM_compl: "NORM \ = nNORM \\<^sup>-" by (simp add: NORM_def bottom_def compl_def nNORM_def setequ_def svfun_compl_def top_def) +lemma nDNRM_DNRM_compl: "DNRM \ = nDNRM \\<^sup>-" by (simp add: DNRM_def bottom_def compl_def nDNRM_def setequ_def svfun_compl_def top_def) + +text\nEXPN (nCNTR) entail nDNRM (nNORM).\ +lemma nEXPN_impl_nDNRM: "nEXPN \ \ nDNRM \" unfolding cond by (metis bottom_def compl_def setequ_def subset_def top_def) +lemma nCNTR_impl_nNORM: "nCNTR \ \ nNORM \" by (simp add: nEXPN_impl_nDNRM nEXPN_nCNTR_dual2 nNOR_dual1) + + +text\Anti-Idempotence (nIDEM).\ +definition nIDEM::"('w \ \ 'w \) \ bool" ("nIDEM") + where "nIDEM \ \ \A. \(\<^bold>\(\ A)) \<^bold>= (\ A)" +definition nIDEM_a::"('w \ \ 'w \) \ bool" ("nIDEM\<^sup>a") + where "nIDEM_a \ \ \A. (\ A) \<^bold>\ \(\<^bold>\(\ A))" +definition nIDEM_b::"('w \ \ 'w \) \ bool" ("nIDEM\<^sup>b") + where "nIDEM_b \ \ \A. \(\<^bold>\(\ A)) \<^bold>\ (\ A)" + +declare nIDEM_def[cond] nIDEM_a_def[cond] nIDEM_b_def[cond] + +text\nIDEM-a and nIDEM-b are dual to each other.\ +lemma nIDEM_dual1: "nIDEM\<^sup>a \ = nIDEM\<^sup>b \\<^sup>d" unfolding cond by (metis BA_cp BA_dn op_dual_def setequ_ext) +lemma nIDEM_dual2: "nIDEM\<^sup>b \ = nIDEM\<^sup>a \\<^sup>d" by (simp add: dual_invol nIDEM_dual1) + +lemma nIDEM_char: "nIDEM \ = (nIDEM\<^sup>a \ \ nIDEM\<^sup>b \)" unfolding cond setequ_char by blast +lemma nIDEM_dual: "nIDEM \ = nIDEM \\<^sup>d" using nIDEM_char nIDEM_dual1 nIDEM_dual2 by blast + +text\nIDEM(a/b) and IDEM(a/b) are the 'complements' each other.\ +lemma nIDEM_a_compl: "IDEM\<^sup>a \ = nIDEM\<^sup>a \\<^sup>-" by (metis (no_types, lifting) BA_cp IDEM_a_def nIDEM_a_def sfun_compl_invol svfun_compl_def) +lemma nIDEM_b_compl: "IDEM\<^sup>b \ = nIDEM\<^sup>b \\<^sup>-" by (metis IDEM_dual2 dual_compl_char1 dual_compl_char2 nIDEM_a_compl nIDEM_dual2) +lemma nIDEM_compl: "nIDEM \ = IDEM \\<^sup>-" by (simp add: IDEM_char nIDEM_a_compl nIDEM_b_compl nIDEM_char sfun_compl_invol) + +text\nEXPN (nCNTR) entail nIDEM-a (nIDEM-b).\ +lemma nEXPN_impl_nIDEM_a: "nEXPN \ \ nIDEM\<^sup>b \" by (metis nEXPN_def nIDEM_b_def sfun_compl_invol svfun_compl_def) +lemma nCNTR_impl_nIDEM_b: "nCNTR \ \ nIDEM\<^sup>a \" by (simp add: nEXPN_impl_nIDEM_a nEXPN_nCNTR_dual2 nIDEM_dual1) + + +text\Anti-distribution over joins or anti-additivity (nADDI) and its dual.\ +definition nADDI::"('w \ \ 'w \) \ bool" ("nADDI") + where "nADDI \ \ \A B. \(A \<^bold>\ B) \<^bold>= (\ A) \<^bold>\ (\ B)" +definition nADDI_a::"('w \ \ 'w \) \ bool" ("nADDI\<^sup>a") + where "nADDI\<^sup>a \ \ \A B. (\ A) \<^bold>\ (\ B) \<^bold>\ \(A \<^bold>\ B)" +definition nADDI_b::"('w \ \ 'w \) \ bool" ("nADDI\<^sup>b") + where "nADDI\<^sup>b \ \ \A B. \(A \<^bold>\ B) \<^bold>\ (\ A) \<^bold>\ (\ B)" + +text\Anti-distribution over meets or anti-multiplicativity (nMULT).\ +definition nMULT::"('w \ \ 'w \) \ bool" ("nMULT") + where "nMULT \ \ \A B. \(A \<^bold>\ B) \<^bold>= (\ A) \<^bold>\ (\ B)" +definition nMULT_a::"('w \ \ 'w \) \ bool" ("nMULT\<^sup>a") + where "nMULT\<^sup>a \ \ \A B. (\ A) \<^bold>\ (\ B) \<^bold>\ \(A \<^bold>\ B)" +definition nMULT_b::"('w \ \ 'w \) \ bool" ("nMULT\<^sup>b") + where "nMULT\<^sup>b \ \ \A B. \(A \<^bold>\ B) \<^bold>\ (\ A) \<^bold>\ (\ B)" + +declare nADDI_def[cond] nADDI_a_def[cond] nADDI_b_def[cond] + nMULT_def[cond] nMULT_a_def[cond] nMULT_b_def[cond] + +lemma nADDI_char: "nADDI \ = (nADDI\<^sup>a \ \ nADDI\<^sup>b \)" unfolding cond using setequ_char by blast +lemma nMULT_char: "nMULT \ = (nMULT\<^sup>a \ \ nMULT\<^sup>b \)" unfolding cond using setequ_char by blast + +text\ANTI, nMULT-a and nADDI-b are equivalent.\ +lemma ANTI_nMULTa: "nMULT\<^sup>a \ = ANTI \" unfolding cond by (smt (z3) L10 L7 join_def meet_def setequ_ext subset_def) +lemma ANTI_nADDIb: "nADDI\<^sup>b \ = ANTI \" unfolding cond by (smt (verit) BA_cp BA_deMorgan1 L10 L3 L5 L8 L9 setequ_char setequ_ext) + +text\Below we prove several duality relationships between nADDI(a/b) and nMULT(a/b).\ + +text\Duality between nMULT-a and nADDI-b (an easy corollary from the self-duality of ANTI).\ +lemma nMULTa_nADDIb_dual1: "nMULT\<^sup>a \ = nADDI\<^sup>b \\<^sup>d" using ANTI_nADDIb ANTI_nMULTa ANTI_dual by blast +lemma nMULTa_nADDIb_dual2: "nADDI\<^sup>b \ = nMULT\<^sup>a \\<^sup>d" by (simp add: dual_invol nMULTa_nADDIb_dual1) +text\Duality between nADDI-a and nMULT-b.\ +lemma nADDIa_nMULTb_dual1: "nADDI\<^sup>a \ = nMULT\<^sup>b \\<^sup>d" unfolding cond by (metis (no_types, lifting) BA_cp BA_deMorgan1 BA_dn op_dual_def setequ_ext) +lemma nADDIa_nMULTb_dual2: "nMULT\<^sup>b \ = nADDI\<^sup>a \\<^sup>d" by (simp add: dual_invol nADDIa_nMULTb_dual1) +text\Duality between ADDI and MULT.\ +lemma nADDI_nMULT_dual1: "nADDI \ = nMULT \\<^sup>d" using nADDI_char nADDIa_nMULTb_dual1 nMULT_char nMULTa_nADDIb_dual2 by blast +lemma nADDI_nMULT_dual2: "nMULT \ = nADDI \\<^sup>d" by (simp add: dual_invol nADDI_nMULT_dual1) + +text\nADDI and nMULT are the 'complements' of ADDI and MULT respectively.\ +lemma nADDIa_compl: "ADDI\<^sup>a \ = nADDI\<^sup>a \\<^sup>-" by (metis ADDI_a_def BA_cp BA_deMorgan1 nADDI_a_def setequ_ext svfun_compl_def) +lemma nADDIb_compl: "ADDI\<^sup>b \ = nADDI\<^sup>b \\<^sup>-" by (simp add: ANTI_nADDIb ANTI_MONO MONO_ADDIb sfun_compl_invol) +lemma nADDI_compl: "ADDI \ = nADDI \\<^sup>-" by (simp add: ADDI_char nADDI_char nADDIa_compl nADDIb_compl) +lemma nMULTa_compl: "MULT\<^sup>a \ = nMULT\<^sup>a \\<^sup>-" by (simp add: ANTI_MONO ANTI_nMULTa MONO_MULTa sfun_compl_invol) +lemma nMULTb_compl: "MULT\<^sup>b \ = nMULT\<^sup>b \\<^sup>-" by (metis BA_cp BA_deMorgan2 MULT_b_def nMULT_b_def setequ_ext svfun_compl_def) +lemma nMULT_compl: "MULT \ = nMULT \\<^sup>-" by (simp add: MULT_char nMULT_char nMULTa_compl nMULTb_compl) + + +text\We verify properties regarding closure over meets/joins for fixed-points.\ + +text\nMULT for an operator implies join-closedness of the set of fixed-points of its dual-complement.\ +lemma nMULT_joinclosed: "nMULT \ \ join_closed (fp (\\<^sup>d\<^sup>-))" by (smt (verit, del_insts) ADDI_MULT_dual2 ADDI_joinclosed BA_deMorgan1 MULT_def dual_compl_char2 nMULT_def setequ_ext svfun_compl_def) +lemma "join_closed (fp (\\<^sup>d\<^sup>-)) \ nMULT \" nitpick oops \\ countermodel found: needs further assumptions \ +lemma joinclosed_nMULT: "ANTI \ \ nCNTR \ \ nIDEM\<^sup>b \ \ join_closed (fp (\\<^sup>d\<^sup>-)) \ nMULT \" by (metis ANTI_MONO ANTI_dual IDEM_char IDEM_dual dual_compl_char1 dual_compl_char2 joinclosed_ADDI nADDI_compl nADDI_nMULT_dual2 nCNTR_impl_nIDEM_b nEXPN_CNTR_compl nEXPN_nCNTR_dual2 nIDEM_char nIDEM_compl sfun_compl_invol) + +text\nADDI for an operator implies meet-closedness of the set of fixed-points of its dual-complement.\ +lemma nADDI_meetclosed: "nADDI \ \ meet_closed (fp (\\<^sup>d\<^sup>-))" by (smt (verit, ccfv_threshold) ADDI_MULT_dual1 ADDI_def BA_deMorgan2 MULT_meetclosed dual_compl_char2 nADDI_def setequ_ext svfun_compl_def) +lemma "meet_closed (fp (\\<^sup>d\<^sup>-)) \ nADDI \" nitpick oops \\ countermodel found: needs further assumptions \ +lemma meetclosed_nADDI: "ANTI \ \ nEXPN \ \ nIDEM\<^sup>a \ \ meet_closed (fp (\\<^sup>d\<^sup>-)) \ nADDI \" by (metis ADDI_MULT_dual2 ADDI_joinclosed ANTI_MONO ANTI_dual dual_compl_char1 dual_compl_char2 joinclosed_nMULT meetclosed_MULT nADDI_nMULT_dual1 nCNTR_EXPN_compl nEXPN_nCNTR_dual1 nIDEM_b_compl nIDEM_dual1 sfun_compl_invol) + +text\Assuming ANTI, we have that nEXPN (nCNTR) implies meet-closed (join-closed) for the set of fixed-points.\ +lemma nEXPN_meetclosed: "ANTI \ \ nEXPN \ \ meet_closed (fp \)" by (metis (full_types) L10 compl_def fixpoints_def meet_closed_def nEXPN_def setequ_ext subset_def) +lemma nCNTR_joinclosed: "ANTI \ \ nCNTR \ \ join_closed (fp \)" by (smt (verit, ccfv_threshold) BA_impl L9 fixpoints_def impl_char join_closed_def nCNTR_def setequ_char setequ_ext) + +end diff --git a/thys/Topological_Semantics/conditions_negative_infinitary.thy b/thys/Topological_Semantics/conditions_negative_infinitary.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/conditions_negative_infinitary.thy @@ -0,0 +1,96 @@ +theory conditions_negative_infinitary + imports conditions_negative conditions_positive_infinitary +begin + +subsection \Infinitary Negative Conditions\ + +text\We define and interrelate infinitary variants for some previously introduced + axiomatic conditions on operators.\ + +text\Anti-distribution over infinite joins (suprema) or infinite anti-additivity (inADDI).\ +definition inADDI::"('w \ \ 'w \) \ bool" ("inADDI") + where "inADDI \ \ \S. \(\<^bold>\S) \<^bold>= \<^bold>\\\ S\" +definition inADDI_a::"('w \ \ 'w \) \ bool" ("inADDI\<^sup>a") + where "inADDI\<^sup>a \ \ \S. \<^bold>\\\ S\ \<^bold>\ \(\<^bold>\S) " +definition inADDI_b::"('w \ \ 'w \) \ bool" ("inADDI\<^sup>b") + where "inADDI\<^sup>b \ \ \S. \(\<^bold>\S) \<^bold>\ \<^bold>\\\ S\" + +text\Anti-distribution over infinite meets (infima) or infinite anti-multiplicativity (inMULT).\ +definition inMULT::"('w \ \ 'w \) \ bool" ("inMULT") + where "inMULT \ \ \S. \(\<^bold>\S) \<^bold>= \<^bold>\\\ S\" +definition inMULT_a::"('w \ \ 'w \) \ bool" ("inMULT\<^sup>a") + where "inMULT\<^sup>a \ \ \S. \<^bold>\\\ S\ \<^bold>\ \(\<^bold>\S)" +definition inMULT_b::"('w \ \ 'w \) \ bool" ("inMULT\<^sup>b") + where "inMULT\<^sup>b \ \ \S. \(\<^bold>\S) \<^bold>\ \<^bold>\\\ S\" + +declare inADDI_def[cond] inADDI_a_def[cond] inADDI_b_def[cond] + inMULT_def[cond] inMULT_a_def[cond] inMULT_b_def[cond] + +lemma inADDI_char: "inADDI \ = (inADDI\<^sup>a \ \ inADDI\<^sup>b \)" unfolding cond using setequ_char by blast +lemma inMULT_char: "inMULT \ = (inMULT\<^sup>a \ \ inMULT\<^sup>b \)" unfolding cond using setequ_char by blast + +text\nADDI-b and inADDI-b are in fact equivalent.\ +lemma inADDIb_equ: "inADDI\<^sup>b \ = nADDI\<^sup>b \" proof - + have lr: "inADDI\<^sup>b \ \ nADDI\<^sup>b \" proof - (*prove as a one-liner by instantiating inADDI_b_def with S=(\Z. Z=A \ Z=B)*) + assume inaddib: "inADDI\<^sup>b \" + { fix A::"'a \" and B::"'a \" (* for some reason Isabelle doesn't like other letters as type variable. Why?*) + let ?S="\Z. Z=A \ Z=B" + have "\<^bold>\?S = A \<^bold>\ B" unfolding supremum_def join_def by blast + hence p1: "\(\<^bold>\?S) = \(A \<^bold>\ B)" by simp + have "\\ ?S\ = (\Z. Z=(\ A) \ Z=(\ B))" unfolding image_def by metis + hence p2: "\<^bold>\\\ ?S\ = (\ A) \<^bold>\ (\ B)" unfolding infimum_def meet_def by auto + have "\(\<^bold>\?S) \<^bold>\ \<^bold>\\\ ?S\" using inaddib inADDI_b_def by blast + hence "\(A \<^bold>\ B) \<^bold>\ (\ A) \<^bold>\ (\ B)" using p1 p2 by simp + } thus ?thesis by (simp add: nADDI_b_def) qed + have rl: "nADDI\<^sup>b \ \ inADDI\<^sup>b \" unfolding inADDI_b_def ANTI_nADDIb ANTI_def image_def + by (smt (verit) glb_def inf_glb lower_bounds_def lub_def sup_lub upper_bounds_def) + from lr rl show ?thesis by auto +qed +text\nMULT-a and inMULT-a are also equivalent.\ +lemma inMULTa_equ: "inMULT\<^sup>a \ = nMULT\<^sup>a \" proof - + have lr: "inMULT\<^sup>a \ \ nMULT\<^sup>a \" proof - (*prove as a one-liner by instantiating inMULT_a_def with S=(\Z. Z=A \ Z=B)*) + assume inmulta: "inMULT\<^sup>a \" + { fix A::"'a \" and B::"'a \" + let ?S="\Z. Z=A \ Z=B" + have "\<^bold>\?S = A \<^bold>\ B" unfolding infimum_def meet_def by blast + hence p1: "\(\<^bold>\?S) = \(A \<^bold>\ B)" by simp + have "\\ ?S\ = (\Z. Z=(\ A) \ Z=(\ B))" unfolding image_def by metis + hence p2: "\<^bold>\\\ ?S\ = (\ A) \<^bold>\ (\ B)" unfolding supremum_def join_def by auto + have "\<^bold>\\\ ?S\ \<^bold>\ \(\<^bold>\?S)" using inmulta inMULT_a_def by blast + hence "(\ A) \<^bold>\ (\ B) \<^bold>\ \(A \<^bold>\ B)" using p1 p2 by simp + } thus ?thesis by (simp add: nMULT_a_def) qed + have rl: "nMULT\<^sup>a \ \ inMULT\<^sup>a \" unfolding inMULT_a_def ANTI_nMULTa ANTI_def image_def + by (smt (verit) glb_def inf_glb lower_bounds_def lub_def sup_lub upper_bounds_def) + from lr rl show ?thesis by blast +qed + +text\Thus we have that ANTI, nADDI-b/inADDI-b and nMULT-a/inMULT-a are all equivalent.\ +lemma ANTI_inADDIb: "inADDI\<^sup>b \ = ANTI \" unfolding ANTI_nADDIb inADDIb_equ by simp +lemma ANTI_inMULTa: "inMULT\<^sup>a \ = ANTI \" unfolding ANTI_nMULTa inMULTa_equ by simp + + +text\Below we prove several duality relationships between inADDI(a/b) and inMULT(a/b).\ + +text\Duality between inMULT-a and inADDI-b (an easy corollary from the previous equivalence).\ +lemma inMULTa_inADDIb_dual1: "inMULT\<^sup>a \ = inADDI\<^sup>b \\<^sup>d" by (simp add: nMULTa_nADDIb_dual1 inADDIb_equ inMULTa_equ) +lemma inMULTa_inADDIb_dual2: "inADDI\<^sup>b \ = inMULT\<^sup>a \\<^sup>d" by (simp add: nMULTa_nADDIb_dual2 inADDIb_equ inMULTa_equ) +text\Duality between inADDI-a and inMULT-b.\ +lemma inADDIa_inMULTb_dual1: "inADDI\<^sup>a \ = inMULT\<^sup>b \\<^sup>d" by (smt (z3) BA_cmpl_equ BA_cp dualcompl_invol inADDI_a_def iDM_a inMULT_b_def im_prop1 op_dual_def setequ_ext) +lemma inADDIa_inMULTb_dual2: "inMULT\<^sup>b \ = inADDI\<^sup>a \\<^sup>d" by (simp add: dual_invol inADDIa_inMULTb_dual1) +text\Duality between inADDI and inMULT.\ +lemma inADDI_inMULT_dual1: "inADDI \ = inMULT \\<^sup>d" using inADDI_char inADDIa_inMULTb_dual1 inMULT_char inMULTa_inADDIb_dual2 by blast +lemma inADDI_inMULT_dual2: "inMULT \ = inADDI \\<^sup>d" by (simp add: dual_invol inADDI_inMULT_dual1) + +text\inADDI and inMULT are the 'complements' of iADDI and iMULT respectively.\ +lemma inADDIa_compl: "iADDI\<^sup>a \ = inADDI\<^sup>a \\<^sup>-" by (metis BA_cmpl_equ BA_cp iADDI_a_def iDM_a im_prop2 inADDI_a_def setequ_ext svfun_compl_def) +lemma inADDIb_compl: "iADDI\<^sup>b \ = inADDI\<^sup>b \\<^sup>-" by (simp add: ANTI_MONO ANTI_inADDIb MONO_iADDIb) +lemma inADDI_compl: "iADDI \ = inADDI \\<^sup>-" by (simp add: iADDI_char inADDI_char inADDIa_compl inADDIb_compl) +lemma inMULTa_compl: "iMULT\<^sup>a \ = inMULT\<^sup>a \\<^sup>-" by (simp add: ANTI_MONO ANTI_inMULTa MONO_iMULTa) +lemma inMULTb_compl: "iMULT\<^sup>b \ = inMULT\<^sup>b \\<^sup>-" by (metis dual_compl_char1 dual_compl_char2 iADDIa_iMULTb_dual2 inADDIa_compl inADDIa_inMULTb_dual2) +lemma inMULT_compl: "iMULT \ = inMULT \\<^sup>-" by (simp add: iMULT_char inMULT_char inMULTa_compl inMULTb_compl) + +text\In fact, infinite anti-additivity (anti-multiplicativity) entails (dual) anti-normality:\ +lemma inADDI_nNORM: "inADDI \ \ nNORM \" by (metis bottom_def inADDI_def inf_empty image_def nNORM_def setequ_ext sup_empty) +lemma inMULT_nDNRM: "inMULT \ \ nDNRM \" by (simp add: inADDI_inMULT_dual2 inADDI_nNORM nNOR_dual2) + +end diff --git a/thys/Topological_Semantics/conditions_positive.thy b/thys/Topological_Semantics/conditions_positive.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/conditions_positive.thy @@ -0,0 +1,140 @@ +theory conditions_positive + imports boolean_algebra_operators +begin + +section \Topological Conditions\ + +text\We define and interrelate some useful axiomatic conditions on unary operations (operators) +having a 'w-parametric type ('w)\\('w)\. +Boolean algebras extended with such operators give us different sorts of topological Boolean algebras.\ + +subsection \Positive Conditions\ + +text\Monotonicity (MONO).\ +definition MONO::"('w \ \ 'w \) \ bool" ("MONO") + where "MONO \ \ \A B. A \<^bold>\ B \ \ A \<^bold>\ \ B" + +named_theorems cond (*to group together axiomatic conditions*) +declare MONO_def[cond] + +text\MONO is self-dual.\ +lemma MONO_dual: "MONO \ = MONO \\<^sup>d" by (smt (verit) BA_cp MONO_def dual_invol op_dual_def) + + +text\Expansive/extensive (EXPN) and its dual contractive (CNTR).\ +definition EXPN::"('w \ \ 'w \) \ bool" ("EXPN") + where "EXPN \ \ \A. A \<^bold>\ \ A" +definition CNTR::"('w \ \ 'w \) \ bool" ("CNTR") + where "CNTR \ \ \A. \ A \<^bold>\ A" + +declare EXPN_def[cond] CNTR_def[cond] + +text\EXPN and CNTR are dual to each other.\ +lemma EXPN_CNTR_dual1: "EXPN \ = CNTR \\<^sup>d" unfolding cond by (metis BA_cp BA_dn op_dual_def setequ_ext) +lemma EXPN_CNTR_dual2: "CNTR \ = EXPN \\<^sup>d" by (simp add: EXPN_CNTR_dual1 dual_invol) + + +text\Normality (NORM) and its dual (DNRM).\ +definition NORM::"('w \ \ 'w \) \ bool" ("NORM") + where "NORM \ \ (\ \<^bold>\) \<^bold>= \<^bold>\" +definition DNRM::"('w \ \ 'w \) \ bool" ("DNRM") + where "DNRM \ \ (\ \<^bold>\) \<^bold>= \<^bold>\" + +declare NORM_def[cond] DNRM_def[cond] + +text\NORM and DNRM are dual to each other.\ +lemma NOR_dual1: "NORM \ = DNRM \\<^sup>d" unfolding cond by (simp add: bottom_def compl_def op_dual_def setequ_def top_def) +lemma NOR_dual2: "DNRM \ = NORM \\<^sup>d" by (simp add: NOR_dual1 dual_invol) + +text\EXPN (CNTR) entails DNRM (NORM).\ +lemma EXPN_impl_DNRM: "EXPN \ \ DNRM \" unfolding cond by (simp add: setequ_def subset_def top_def) +lemma CNTR_impl_NORM: "CNTR \ \ NORM \" by (simp add: EXPN_CNTR_dual2 EXPN_impl_DNRM NOR_dual1 dual_invol) + + +text\Idempotence (IDEM).\ +definition IDEM::"('w \ \ 'w \) \ bool" ("IDEM") + where "IDEM \ \ \A. \(\ A) \<^bold>= (\ A)" +definition IDEM_a::"('w \ \ 'w \) \ bool" ("IDEM\<^sup>a") + where "IDEM\<^sup>a \ \ \A. \(\ A) \<^bold>\ (\ A)" +definition IDEM_b::"('w \ \ 'w \) \ bool" ("IDEM\<^sup>b") + where "IDEM\<^sup>b \ \ \A. (\ A) \<^bold>\ \(\ A)" + +declare IDEM_def[cond] IDEM_a_def[cond] IDEM_b_def[cond] + +text\IDEM-a and IDEM-b are dual to each other.\ +lemma IDEM_dual1: "IDEM\<^sup>a \ = IDEM\<^sup>b \\<^sup>d" unfolding cond by (metis (mono_tags, opaque_lifting) BA_cp BA_dn op_dual_def setequ_ext) +lemma IDEM_dual2: "IDEM\<^sup>b \ = IDEM\<^sup>a \\<^sup>d" by (simp add: IDEM_dual1 dual_invol) + +lemma IDEM_char: "IDEM \ = (IDEM\<^sup>a \ \ IDEM\<^sup>b \)" unfolding cond setequ_char by blast +lemma IDEM_dual: "IDEM \ = IDEM \\<^sup>d" using IDEM_char IDEM_dual1 IDEM_dual2 by blast + + +text\EXPN (CNTR) entail IDEM-b (IDEM-a).\ +lemma EXPN_impl_IDEM_b: "EXPN \ \ IDEM\<^sup>b \" by (simp add: EXPN_def IDEM_b_def) +lemma CNTR_impl_IDEM_a: "CNTR \ \ IDEM\<^sup>a \" by (simp add: CNTR_def IDEM_a_def) + +text\Moreover, IDEM has some other interesting characterizations. For example, via function composition:\ +lemma IDEM_fun_comp_char: "IDEM \ = (\ = \ \ \)" unfolding cond fun_comp_def by (metis setequ_ext) +text\Or having the property of collapsing the range and the set of fixed-points of an operator:\ +lemma IDEM_range_fp_char: "IDEM \ = (\\ _\ = fp \)" unfolding cond range_def fixpoints_def by (metis setequ_ext) + +text\Distribution over joins or additivity (ADDI).\ +definition ADDI::"('w \ \ 'w \) \ bool" ("ADDI") + where "ADDI \ \ \A B. \(A \<^bold>\ B) \<^bold>= (\ A) \<^bold>\ (\ B)" +definition ADDI_a::"('w \ \ 'w \) \ bool" ("ADDI\<^sup>a") + where "ADDI\<^sup>a \ \ \A B. \(A \<^bold>\ B) \<^bold>\ (\ A) \<^bold>\ (\ B)" +definition ADDI_b::"('w \ \ 'w \) \ bool" ("ADDI\<^sup>b") + where "ADDI\<^sup>b \ \ \A B. (\ A) \<^bold>\ (\ B) \<^bold>\ \(A \<^bold>\ B)" + +text\Distribution over meets or multiplicativity (MULT).\ +definition MULT::"('w \ \ 'w \) \ bool" ("MULT") + where "MULT \ \ \A B. \(A \<^bold>\ B) \<^bold>= (\ A) \<^bold>\ (\ B)" +definition MULT_a::"('w \ \ 'w \) \ bool" ("MULT\<^sup>a") + where "MULT\<^sup>a \ \ \A B. \(A \<^bold>\ B) \<^bold>\ (\ A) \<^bold>\ (\ B)" +definition MULT_b::"('w \ \ 'w \) \ bool" ("MULT\<^sup>b") + where "MULT\<^sup>b \ \ \A B. (\ A) \<^bold>\ (\ B) \<^bold>\ \(A \<^bold>\ B)" + +declare ADDI_def[cond] ADDI_a_def[cond] ADDI_b_def[cond] + MULT_def[cond] MULT_a_def[cond] MULT_b_def[cond] + +lemma ADDI_char: "ADDI \ = (ADDI\<^sup>a \ \ ADDI\<^sup>b \)" unfolding cond using setequ_char by blast +lemma MULT_char: "MULT \ = (MULT\<^sup>a \ \ MULT\<^sup>b \)" unfolding cond using setequ_char by blast + +text\MONO, MULT-a and ADDI-b are equivalent.\ +lemma MONO_MULTa: "MULT\<^sup>a \ = MONO \" unfolding cond by (metis L10 L3 L4 L5 L8 setequ_char setequ_ext) +lemma MONO_ADDIb: "ADDI\<^sup>b \ = MONO \" unfolding cond by (metis (mono_tags, lifting) L7 L9 join_def setequ_ext subset_def) + +text\Below we prove several duality relationships between ADDI(a/b) and MULT(a/b).\ + +text\Duality between MULT-a and ADDI-b (an easy corollary from the self-duality of MONO).\ +lemma MULTa_ADDIb_dual1: "MULT\<^sup>a \ = ADDI\<^sup>b \\<^sup>d" by (metis MONO_ADDIb MONO_MULTa MONO_dual) +lemma MULTa_ADDIb_dual2: "ADDI\<^sup>b \ = MULT\<^sup>a \\<^sup>d" by (simp add: MULTa_ADDIb_dual1 dual_invol) +text\Duality between ADDI-a and MULT-b.\ +lemma ADDIa_MULTb_dual1: "ADDI\<^sup>a \ = MULT\<^sup>b \\<^sup>d" unfolding cond op_dual_def by (metis BA_cp BA_deMorgan1 BA_dn setequ_ext) +lemma ADDIa_MULTb_dual2: "MULT\<^sup>b \ = ADDI\<^sup>a \\<^sup>d" by (simp add: ADDIa_MULTb_dual1 dual_invol) +text\Duality between ADDI and MULT.\ +lemma ADDI_MULT_dual1: "ADDI \ = MULT \\<^sup>d" using ADDI_char ADDIa_MULTb_dual1 MULT_char MULTa_ADDIb_dual2 by blast +lemma ADDI_MULT_dual2: "MULT \ = ADDI \\<^sup>d" by (simp add: ADDI_MULT_dual1 dual_invol) + + +text\We verify properties regarding closure over meets/joins for fixed-points.\ + +text\MULT implies meet-closedness of the set of fixed-points (the converse requires additional assumptions).\ +lemma MULT_meetclosed: "MULT \ \ meet_closed (fp \)" by (simp add: MULT_def fixpoints_def meet_closed_def setequ_ext) +lemma "meet_closed (fp \) \ MULT \" nitpick oops \\ countermodel found: needs further assumptions. \ +lemma meetclosed_MULT: "MONO \ \ CNTR \ \ IDEM\<^sup>b \ \ meet_closed (fp \) \ MULT \" by (smt (z3) CNTR_def IDEM_b_def MONO_MULTa MONO_def MULT_a_def MULT_def fixpoints_def meet_closed_def meet_def setequ_char setequ_ext subset_def) + +text\ADDI implies join-closedness of the set of fixed-points (the converse requires additional assumptions).\ +lemma ADDI_joinclosed: "ADDI \ \ join_closed (fp \)" by (simp add: ADDI_def fixpoints_def join_closed_def setequ_ext) +lemma "join_closed (fp \) \ ADDI \" nitpick oops \\ countermodel found: needs further assumptions \ +lemma joinclosed_ADDI: "MONO \ \ EXPN \ \ IDEM\<^sup>a \ \ join_closed (fp \) \ ADDI \" by (smt (verit, ccfv_threshold) ADDI_MULT_dual1 BA_deMorgan2 EXPN_CNTR_dual1 IDEM_dual1 MONO_dual fp_dual join_closed_def meet_closed_def meetclosed_MULT sdfun_dcompl_def setequ_ext) + +text\Assuming MONO, we have that EXPN (CNTR) implies meet-closed (join-closed) for the set of fixed-points.\ +lemma EXPN_meetclosed: "MONO \ \ EXPN \ \ meet_closed (fp \)" by (smt (verit) EXPN_def MONO_MULTa MULT_a_def fixpoints_def meet_closed_def setequ_char setequ_ext) +lemma CNTR_joinclosed: "MONO \ \ CNTR \ \ join_closed (fp \)" by (smt (verit, best) ADDI_b_def CNTR_def MONO_ADDIb fixpoints_def join_closed_def setequ_char setequ_ext) + +text\Further assuming IDEM the above results can be stated to the whole range of an operator.\ +lemma "MONO \ \ EXPN \ \ IDEM \ \ meet_closed (\\ _\)" by (simp add: EXPN_meetclosed IDEM_range_fp_char) +lemma "MONO \ \ CNTR \ \ IDEM \ \ join_closed (\\ _\)" by (simp add: CNTR_joinclosed IDEM_range_fp_char) + +end diff --git a/thys/Topological_Semantics/conditions_positive_infinitary.thy b/thys/Topological_Semantics/conditions_positive_infinitary.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/conditions_positive_infinitary.thy @@ -0,0 +1,248 @@ +theory conditions_positive_infinitary + imports conditions_positive boolean_algebra_infinitary +begin + +subsection \Infinitary Positive Conditions\ + +text\We define and interrelate infinitary variants for some previously introduced + axiomatic conditions on operators.\ + +text\Distribution over infinite joins (suprema) or infinite additivity (iADDI).\ +definition iADDI::"('w \ \ 'w \) \ bool" ("iADDI") + where "iADDI \ \ \S. \(\<^bold>\S) \<^bold>= \<^bold>\\\ S\" +definition iADDI_a::"('w \ \ 'w \) \ bool" ("iADDI\<^sup>a") + where "iADDI\<^sup>a \ \ \S. \(\<^bold>\S) \<^bold>\ \<^bold>\\\ S\" +definition iADDI_b::"('w \ \ 'w \) \ bool" ("iADDI\<^sup>b") + where "iADDI\<^sup>b \ \ \S. \<^bold>\\\ S\ \<^bold>\ \(\<^bold>\S)" +text\Distribution over infinite meets (infima) or infinite multiplicativity (iMULT).\ +definition iMULT::"('w \ \ 'w \) \ bool" ("iMULT") + where "iMULT \ \ \S. \(\<^bold>\S) \<^bold>= \<^bold>\\\ S\" +definition iMULT_a::"('w \ \ 'w \) \ bool" ("iMULT\<^sup>a") + where "iMULT\<^sup>a \ \ \S. \(\<^bold>\S) \<^bold>\ \<^bold>\\\ S\" +definition iMULT_b::"('w \ \ 'w \) \ bool" ("iMULT\<^sup>b") + where "iMULT\<^sup>b \ \ \S. \<^bold>\\\ S\ \<^bold>\ \(\<^bold>\S)" + +declare iADDI_def[cond] iADDI_a_def[cond] iADDI_b_def[cond] + iMULT_def[cond] iMULT_a_def[cond] iMULT_b_def[cond] + +lemma iADDI_char: "iADDI \ = (iADDI\<^sup>a \ \ iADDI\<^sup>b \)" unfolding cond using setequ_char by blast +lemma iMULT_char: "iMULT \ = (iMULT\<^sup>a \ \ iMULT\<^sup>b \)" unfolding cond using setequ_char by blast + +text\ADDI-b and iADDI-b are in fact equivalent.\ +lemma iADDIb_equ: "iADDI\<^sup>b \ = ADDI\<^sup>b \" proof - + have lr: "iADDI\<^sup>b \ \ ADDI\<^sup>b \" proof - + assume iaddib: "iADDI\<^sup>b \" + { fix A::"'a \" and B::"'a \" (*Isabelle forces us to use 'a as type variable name*) + let ?S="\Z. Z=A \ Z=B" + have "\<^bold>\?S = A \<^bold>\ B" unfolding supremum_def join_def by blast + hence p1: "\(\<^bold>\?S) = \(A \<^bold>\ B)" by simp + have "\\ ?S\ = (\Z. Z=(\ A) \ Z=(\ B))" unfolding image_def by metis + hence p2: "\<^bold>\\\ ?S\ = (\ A) \<^bold>\ (\ B)" unfolding supremum_def join_def by auto + have " \<^bold>\\\ ?S\ \<^bold>\ \(\<^bold>\?S)" using iaddib iADDI_b_def by blast + hence "(\ A) \<^bold>\ (\ B) \<^bold>\ \(A \<^bold>\ B)" using p1 p2 by simp + } thus ?thesis by (simp add: ADDI_b_def) qed + have rl: "ADDI\<^sup>b \ \ iADDI\<^sup>b \" unfolding iADDI_b_def by (smt (verit) MONO_ADDIb MONO_def lub_def image_def sup_lub upper_bounds_def) + from lr rl show ?thesis by auto +qed +text\MULT-a and iMULT-a are also equivalent.\ +lemma iMULTa_equ: "iMULT\<^sup>a \ = MULT\<^sup>a \" proof - + have lr: "iMULT\<^sup>a \ \ MULT\<^sup>a \" proof - + assume imulta: "iMULT\<^sup>a \" + { fix A::"'a \" and B::"'a \" (*Isabelle forces us to use 'a as type variable name*) + let ?S="\Z. Z=A \ Z=B" + have "\<^bold>\?S = A \<^bold>\ B" unfolding infimum_def meet_def by blast + hence p1: "\(\<^bold>\?S) = \(A \<^bold>\ B)" by simp + have "\\ ?S\ = (\Z. Z=(\ A) \ Z=(\ B))" unfolding image_def by metis + hence p2: "\<^bold>\\\ ?S\ = (\ A) \<^bold>\ (\ B)" unfolding infimum_def meet_def by auto + have "\(\<^bold>\?S) \<^bold>\ \<^bold>\\\ ?S\" using imulta iMULT_a_def by blast + hence "\(A \<^bold>\ B) \<^bold>\ (\ A) \<^bold>\ (\ B)" using p1 p2 by simp + } thus ?thesis by (simp add: MULT_a_def) qed + have rl: "MULT\<^sup>a \ \ iMULT\<^sup>a \" by (smt (verit) MONO_MULTa MONO_def glb_def iMULT_a_def inf_glb lower_bounds_def image_def) + from lr rl show ?thesis by blast +qed + +text\Thus we have that MONO, ADDI-b/iADDI-b and MULT-a/iMULT-a are all equivalent.\ +lemma MONO_iADDIb: "iADDI\<^sup>b \ = MONO \" unfolding MONO_ADDIb iADDIb_equ by simp +lemma MONO_iMULTa: "iMULT\<^sup>a \ = MONO \" unfolding MONO_MULTa iMULTa_equ by simp + + +text\Below we prove several duality relationships between iADDI(a/b) and iMULT(a/b).\ + +text\Duality between iMULT-a and iADDI-b (an easy corollary from the previous equivalence).\ +lemma iMULTa_iADDIb_dual1: "iMULT\<^sup>a \ = iADDI\<^sup>b \\<^sup>d" by (simp add: MULTa_ADDIb_dual1 iADDIb_equ iMULTa_equ) +lemma iMULTa_iADDIb_dual2: "iADDI\<^sup>b \ = iMULT\<^sup>a \\<^sup>d" by (simp add: MULTa_ADDIb_dual2 iADDIb_equ iMULTa_equ) +text\Duality between iADDI-a and iMULT-b.\ +lemma iADDIa_iMULTb_dual1: "iADDI\<^sup>a \ = iMULT\<^sup>b \\<^sup>d" by (smt (z3) BA_cmpl_equ BA_cp dualcompl_invol iADDI_a_def iDM_a iMULT_b_def im_prop1 op_dual_def setequ_ext) +lemma iADDIa_iMULTb_dual2: "iMULT\<^sup>b \ = iADDI\<^sup>a \\<^sup>d" by (simp add: dual_invol iADDIa_iMULTb_dual1) +text\Duality between iADDI and iMULT.\ +lemma iADDI_iMULT_dual1: "iADDI \ = iMULT \\<^sup>d" using iADDI_char iADDIa_iMULTb_dual1 iMULT_char iMULTa_iADDIb_dual2 by blast +lemma iADDI_iMULT_dual2: "iMULT \ = iADDI \\<^sup>d" by (simp add: dual_invol iADDI_iMULT_dual1) + +text\In fact, infinite additivity (multiplicativity) entails (dual) normality:\ +lemma iADDI_NORM: "iADDI \ \ NORM \" unfolding cond by (metis bottom_def image_def setequ_ext sup_empty) +lemma iMULT_DNRM: "iMULT \ \ DNRM \" by (simp add: NOR_dual2 iADDI_NORM iADDI_iMULT_dual2) + +text\Suitable conditions on an operation can make the set of its fixed-points closed under infinite meets/joins.\ + +lemma fp_sup_closed_cond1: "iADDI \ \ supremum_closed (fp \)" unfolding cond order supremum_closed_def fixpoints_def image_def by (smt (verit) supremum_def) +lemma fp_sup_closed_cond2: "iADDI\<^sup>a \ \ EXPN \ \ supremum_closed (fp \)" unfolding cond by (smt (z3) fixpoints_def image_def setequ_char subset_def supremum_closed_def supremum_def) +lemma fp_sup_closed_cond3: "MONO \ \ CNTR \ \ supremum_closed (fp \)" unfolding cond by (smt (verit, del_insts) fixpoints_def lub_def setequ_char setequ_ext subset_def sup_lub supremum_closed_def upper_bounds_def) + +lemma fp_inf_closed_cond1: "iMULT \ \ infimum_closed (fp \)" by (metis fp_dual fp_sup_closed_cond1 iADDI_iMULT_dual2 inf_sup_closed_dc) +lemma fp_inf_closed_cond2: "iMULT\<^sup>b \ \ CNTR \ \ infimum_closed (fp \)" by (metis EXPN_CNTR_dual2 fp_dual fp_sup_closed_cond2 iADDIa_iMULTb_dual2 inf_sup_closed_dc) +lemma fp_inf_closed_cond3: "MONO \ \ EXPN \ \ infimum_closed (fp \)" by (metis EXPN_CNTR_dual1 MONO_dual fp_dual fp_sup_closed_cond3 inf_sup_closed_dc) + +text\OTOH, the converse conjectures have (finite) countermodels. They need additional assumptions.\ +lemma "infimum_closed (fp \) \ iMULT \" nitpick oops \\ countermodel found: needs further assumptions \ +lemma "supremum_closed (fp \) \ iADDI \" nitpick oops \\ countermodel found: needs further assumptions \ +lemma fp_inf_closed_iMULT: "MONO \ \ CNTR \ \ IDEM\<^sup>b \ \ infimum_closed (fp \) \ iMULT \" +proof - +assume mono: "MONO \" and cntr: "CNTR \" and idem:"IDEM\<^sup>b \" { + assume ic:"infimum_closed (fp \)" { + fix S + from ic have "\D. D \<^bold>\ (fp \) \ (fp \)(\<^bold>\D)" unfolding infimum_closed_def by simp + hence "let D=\\ S\ in (\X. D X \ (X \<^bold>= \ X)) \ \<^bold>\D \<^bold>= \ \<^bold>\D" by (simp add: fixpoints_def setequ_ext subset_def) + moreover from idem have "(\X. \\ S\ X \ (X \<^bold>= \ X))" by (metis (mono_tags, lifting) CNTR_def IDEM_b_def cntr image_def setequ_char) + ultimately have aux: "\<^bold>\(\\ S\) \<^bold>= \(\<^bold>\\\ S\)" by meson + from cntr have "\<^bold>\\\ S\ \<^bold>\ \<^bold>\S" by (smt (verit, best) CNTR_def image_def infimum_def subset_def) + hence "\(\<^bold>\\\ S\) \<^bold>\ \(\<^bold>\S)" using mono by (simp add: MONO_def) + from this aux have "\<^bold>\\\ S\ \<^bold>\ \(\<^bold>\S)" by (simp add: setequ_ext) + } hence "infimum_closed (fp \) \ iMULT \" by (simp add: MONO_iMULTa iMULT_b_def iMULT_char mono) +} thus ?thesis by simp +qed +lemma fp_sup_closed_iADDI: "MONO \ \ EXPN \ \ IDEM\<^sup>a \ \ supremum_closed (fp \) \ iADDI \" + (* by (metis EXPN_CNTR_dual1 IDEM_dual2 MONO_dual dual_invol fp_inf_closed_iMULT fp_inf_sup_closed_dual iADDI_iMULT_dual1) *) +proof - +assume mono: "MONO \" and expn: "EXPN \" and idem:"IDEM\<^sup>a \" { + assume sc:"supremum_closed (fp \)" { + fix S + from sc have "\D. D \<^bold>\ (fp \) \ (fp \)(\<^bold>\D)" unfolding supremum_closed_def by simp + hence "let D=\\ S\ in (\X. D X \ (X \<^bold>= \ X)) \ \<^bold>\D \<^bold>= \ \<^bold>\D" by (simp add: fixpoints_def setequ_ext subset_def) + moreover have "(\X. \\ S\ X \ (X \<^bold>= \ X))" by (metis (mono_tags, lifting) EXPN_def IDEM_a_def expn idem image_def setequ_char) + ultimately have aux: "\<^bold>\(\\ S\) \<^bold>= \(\<^bold>\\\ S\)" by meson + have "\<^bold>\S \<^bold>\ \<^bold>\\\ S\" by (metis EXPN_CNTR_dual1 EXPN_def IDEM_dual1 MONO_dual dual_invol expn fp_inf_closed_iMULT fp_inf_sup_closed_dual iADDI_def iADDI_iMULT_dual1 idem mono sc setequ_ext) + hence "\(\<^bold>\S) \<^bold>\ \(\<^bold>\\\ S\)" using mono by (simp add: MONO_def) + from this aux have "\(\<^bold>\S) \<^bold>\ \<^bold>\\\ S\" by (metis setequ_ext) + } hence "supremum_closed (fp \) \ iADDI \" by (simp add: MONO_ADDIb iADDI_a_def iADDI_char iADDIb_equ mono) +} thus ?thesis by simp +qed + +section \Alexandrov topologies and (generalized) specialization preorders\ + +text\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, EXPN, NORM, IDEM (resp. MULT, CNTR, DNRM, IDEM). This makes both formulations equivalent. +However, this is not the case in general if those conditions become negotiable.\ + +text\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 'reachability 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.\ + +text\Closure/interior(-like) operators can be derived from an arbitrary relation (as in modal logic).\ +definition Cl_rel::"('w \ 'w \ bool) \ ('w \ \ 'w \)" ("\[_]") + where "\[R] \ \A. \w. \v. R w v \ A v" +definition Int_rel::"('w \ 'w \ bool) \ ('w \ \ 'w \)" ("\[_]") + where "\[R] \ \A. \w. \v. R w v \ A v" + +text\Duality between interior and closure follows directly:\ +lemma dual_CI: "\[R] = \[R]\<^sup>d" by (simp add: Cl_rel_def Int_rel_def compl_def op_dual_def setequ_char) + +text\We explore minimal conditions of the reachability relation under which some operation's conditions obtain.\ +text\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" + +lemma rC1: "iADDI \[R]" unfolding iADDI_def Cl_rel_def image_def supremum_def using setequ_def by fastforce +lemma rC2: "reflexive R = EXPN \[R]" by (metis (full_types) CNTR_def EXPN_CNTR_dual2 Int_rel_def dual_CI subset_def) +lemma rC3: "NORM \[R]" by (simp add: iADDI_NORM rC1) +lemma rC4: "transitive R = IDEM\<^sup>a \[R]" proof - + have l2r: "transitive R \ IDEM\<^sup>a \[R]" by (smt (verit, best) Cl_rel_def IDEM_a_def subset_def) + have r2l: "IDEM\<^sup>a \[R] \ transitive R" unfolding Cl_rel_def IDEM_a_def subset_def using compl_def by force + from l2r r2l show ?thesis by blast +qed + + +text\A reachability (specialization) relation (preorder) can be derived from a given operation (intended as a closure-like operation).\ +definition \::"('w \ \ 'w \) \ ('w \ 'w \ bool)" ("\[_]") + where "\[\] \ \w v. \ (\x. x = v) w" + +text\Preorder properties of the reachability relation follow from the corresponding operation's conditions.\ +lemma rel_refl: "EXPN \ \ reflexive \[\]" by (simp add: EXPN_def \_def subset_def) +lemma rel_trans: "MONO \ \ IDEM\<^sup>a \ \ transitive \[\]" by (smt (verit, best) IDEM_a_def MONO_def \_def subset_def) +lemma "IDEM\<^sup>a \ \ transitive \[\]" nitpick oops \\ counterexample \ + +(*The converse directions do not hold*) +lemma "reflexive \[\] \ EXPN \" nitpick oops \\ counterexample \ +lemma "transitive \[\] \ IDEM\<^sup>a \" nitpick oops \\ counterexample \ +lemma "transitive \[\] \ MONO \" nitpick oops \\ counterexample \ + +text\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 \ \ EXPN \ \ IDEM\<^sup>a \ \ antisymmetric \[\]" nitpick oops \\ counterexample \ +lemma "iADDI \ \ EXPN \ \ IDEM\<^sup>a \ \ symmetric \[\]" nitpick oops \\ counterexample \ + +text\As mentioned previously, Alexandrov closure (and by duality interior) operations correspond to +specialization orderings (reachability 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 preorder (reachability relation). +We examine below minimal conditions under which these relations obtain.\ + +lemma Cl_rel'_a: "MONO \ \ (\A. \[\[\]] A \<^bold>\ \ A)" unfolding Cl_rel_def MONO_def \_def by (smt (verit, ccfv_SIG) subset_def) +lemma Cl_rel'_b: "iADDI\<^sup>a \ \ (\A. \ A \<^bold>\ \[\[\]] A)" proof - +{ assume iaddia: "iADDI\<^sup>a \" + { fix A::"'a \" + let ?S="\B. \w. A w \ B=(\u. u=w)" + have "A \<^bold>= (\<^bold>\?S)" unfolding supremum_def setequ_def by auto + hence "\(A) \<^bold>= \(\<^bold>\?S)" by (simp add: setequ_ext) + moreover have "\<^bold>\\\ ?S\ \<^bold>= \[\[\]] A" by (smt (verit) Cl_rel_def \_def image_def setequ_def supremum_def) + moreover from iaddia have "\(\<^bold>\?S) \<^bold>\ \<^bold>\\\ ?S\" unfolding iADDI_a_def by simp + ultimately have "\ A \<^bold>\ \[\[\]] A" by (simp add: setequ_ext) +} } thus ?thesis by simp +qed +lemma Cl_rel': "iADDI \ \ \ \<^bold>=\<^sup>: \[\[\]]" by (simp add: MONO_iADDIb iADDI_char setequ_char Cl_rel'_a Cl_rel'_b svfun_equ_def) +lemma Cl_rel: "iADDI \ \ \ = \[\[\]]" using Cl_rel' by (metis rC1 svfun_equ_ext) + +text\It is instructive to expand the definitions in the above result:\ +lemma "iADDI \ \ (\A. \w. (\ A) w \ (\v. A v \ \ (\x. x=v) w))" oops + +text\Closure (interior) operations derived from relations are thus closed under infinite joins (meets).\ +lemma "supremum_closed (fp \[R])" by (simp add: fp_sup_closed_cond1 rC1) +lemma "infimum_closed (fp \[R])" by (metis dual_CI fp_inf_closed_cond1 iADDI_iMULT_dual2 rC1) + + +text\We can now revisit the relationship between (anti)symmetry and the separation axioms T1 and T0.\ + +text\T0: any two distinct points in the space can be separated by a closed (or open) set (i.e. containing one point and not the other).\ +abbreviation "T0 \ \ (\p q. p \ q \ (\G. (fp \) G \ \(G p \ G q)))" +text\T1: any two distinct points can be separated by (two not necessarily disjoint) closed (or open) sets.\ +abbreviation "T1 \ \ (\p q. p \ q \ (\G H. (fp \) G \ (fp \) H \ G p \ \G q \ H q \ \H p))" + +text\We can (sanity) check that T1 entails T0 but not viceversa.\ +lemma "T1 \ \ T0 \" by meson +lemma "T0 \ \ T1 \" nitpick oops \\ counterexample \ + + +text\Under appropriate conditions, T0-separation corresponds to antisymmetry of the specialization relation (here an ordering).\ +lemma "T0 \ \ antisymmetric \[\]" nitpick oops (*counterexample*) +lemma T0_antisymm_a: "MONO \ \ T0 \ \ antisymmetric \[\]" by (smt (verit, best) Cl_rel'_a Cl_rel_def fixpoints_def setequ_ext subset_def) +lemma T0_antisymm_b: "EXPN \ \ IDEM\<^sup>a \ \ antisymmetric \[\] \ T0 \" by (metis EXPN_impl_IDEM_b IDEM_char IDEM_def \_def fixpoints_def rel_refl) +lemma T0_antisymm: "MONO \ \ EXPN \ \ IDEM\<^sup>a \ \ T0 \ = antisymmetric \[\]" using T0_antisymm_a T0_antisymm_b by fastforce + +text\Also, under the appropriate conditions, T1-separation corresponds to symmetry of the specialization relation.\ +lemma T1_symm_a: "MONO \ \ T1 \ \ symmetric \[\]" by (metis (mono_tags, opaque_lifting) Cl_rel'_a Cl_rel_def fixpoints_def setequ_ext subset_def) +lemma T1_symm_b: "MONO \ \ EXPN \ \ T0 \ \ symmetric \[\] \ T1 \" by (smt (verit, ccfv_SIG) T0_antisymm_a \_def fixpoints_def rel_refl setequ_def) +lemma T1_symm: "MONO \ \ EXPN \ \ T0 \ \ symmetric \[\] = T1 \" using T1_symm_a T1_symm_b by (smt (verit, ccfv_threshold)) + +end diff --git a/thys/Topological_Semantics/conditions_relativized.thy b/thys/Topological_Semantics/conditions_relativized.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/conditions_relativized.thy @@ -0,0 +1,284 @@ +theory conditions_relativized + imports conditions_negative +begin + +subsection \Relativized Conditions\ + +text\We continue defining and interrelating axiomatic conditions on unary operations (operators). + This time we consider their 'relativized' variants.\ + +text\Relativized order and equality relations.\ +definition subset_in::\'p \ \ 'p \ \ 'p \ \ bool\ ("_\<^bold>\\<^sub>__") + where \A \<^bold>\\<^sub>U B \ \x. U x \ (A x \ B x)\ +definition subset_out::\'p \ \ 'p \ \ 'p \ \ bool\ ("_\<^bold>\\<^sup>__") + where \A \<^bold>\\<^sup>U B \ \x. \U x \ (A x \ B x)\ +definition setequ_in::\'p \ \ 'p \ \ 'p \ \ bool\ ("_\<^bold>=\<^sub>__") + where \A \<^bold>=\<^sub>U B \ \x. U x \ (A x \ B x)\ +definition setequ_out::\'p \ \ 'p \ \ 'p \ \ bool\ ("_\<^bold>=\<^sup>__") + where \A \<^bold>=\<^sup>U B \ \x. \U x \ (A x \ B x)\ + +declare subset_in_def[order] subset_out_def[order] setequ_in_def[order] setequ_out_def[order] + +lemma subset_in_out: "(let U=C in (A \<^bold>\\<^sub>U B)) = (let U=\<^bold>\C in (A \<^bold>\\<^sup>U B))" by (simp add: compl_def subset_in_def subset_out_def) +lemma setequ_in_out: "(let U=C in (A \<^bold>=\<^sub>U B)) = (let U=\<^bold>\C in (A \<^bold>=\<^sup>U B))" by (simp add: compl_def setequ_in_def setequ_out_def) + +lemma subset_in_char: "(A \<^bold>\\<^sub>U B) = (U \<^bold>\ A \<^bold>\ U \<^bold>\ B)" unfolding order conn by blast +lemma subset_out_char: "(A \<^bold>\\<^sup>U B) = (U \<^bold>\ A \<^bold>\ U \<^bold>\ B)" unfolding order conn by blast +lemma setequ_in_char: "(A \<^bold>=\<^sub>U B) = (U \<^bold>\ A \<^bold>= U \<^bold>\ B)" unfolding order conn by blast +lemma setequ_out_char: "(A \<^bold>=\<^sup>U B) = (U \<^bold>\ A \<^bold>= U \<^bold>\ B)" unfolding order conn by blast + +text\Relativization cannot be meaningfully applied to conditions (n)NORM or (n)DNRM.\ +lemma "NORM \ = (let U = \<^bold>\ in ((\ \<^bold>\) \<^bold>=\<^sub>U \<^bold>\))" by (simp add: NORM_def setequ_def setequ_in_def top_def) +lemma "(let U = \<^bold>\ in ((\ \<^bold>\) \<^bold>=\<^sub>U \<^bold>\))" by (simp add: bottom_def setequ_in_def) + +text\Relativization ('in' resp. 'out') leaves (n)EXPN/(n)CNTR unchanged or trivializes them.\ +lemma "EXPN \ = (\A. A \<^bold>\\<^sub>A \ A)" by (simp add: EXPN_def subset_def subset_in_def) +lemma "CNTR \ = (\A. (\ A) \<^bold>\\<^sup>A A)" by (metis (mono_tags, lifting) CNTR_def subset_def subset_out_def) +lemma "\A. A \<^bold>\\<^sup>A \ A" by (simp add: subset_out_def) +lemma "\A. (\ A) \<^bold>\\<^sub>A A" by (simp add: subset_in_def) + + +text\Relativized ADDI variants.\ +definition ADDIr::"('w \ \ 'w \) \ bool" ("ADDIr") + where "ADDIr \ \ \A B. let U = (A \<^bold>\ B) in (\(A \<^bold>\ B) \<^bold>=\<^sup>U (\ A) \<^bold>\ (\ B))" +definition ADDIr_a::"('w \ \ 'w \) \ bool" ("ADDIr\<^sup>a") + where "ADDIr\<^sup>a \ \ \A B. let U = (A \<^bold>\ B) in (\(A \<^bold>\ B) \<^bold>\\<^sup>U (\ A) \<^bold>\ (\ B))" +definition ADDIr_b::"('w \ \ 'w \) \ bool" ("ADDIr\<^sup>b") + where "ADDIr\<^sup>b \ \ \A B. let U = (A \<^bold>\ B) in ((\ A) \<^bold>\ (\ B) \<^bold>\\<^sup>U \(A \<^bold>\ B))" + +declare ADDIr_def[cond] ADDIr_a_def[cond] ADDIr_b_def[cond] + +lemma ADDIr_char: "ADDIr \ = (ADDIr\<^sup>a \ \ ADDIr\<^sup>b \)" unfolding cond by (meson setequ_char setequ_out_char subset_out_char) + +lemma ADDIr_a_impl: "ADDI\<^sup>a \ \ ADDIr\<^sup>a \" by (simp add: ADDI_a_def ADDIr_a_def subset_def subset_out_def) +lemma ADDIr_a_equ: "EXPN \ \ ADDIr\<^sup>a \ = ADDI\<^sup>a \" unfolding cond by (smt (verit, del_insts) join_def subset_def subset_out_def) +lemma ADDIr_a_equ':"nEXPN \ \ ADDIr\<^sup>a \ = ADDI\<^sup>a \" unfolding cond by (smt (verit, ccfv_threshold) compl_def subset_def subset_out_def) + +lemma ADDIr_b_impl: "ADDI\<^sup>b \ \ ADDIr\<^sup>b \" by (simp add: ADDI_b_def ADDIr_b_def subset_def subset_out_def) +lemma "nEXPN \ \ ADDIr\<^sup>b \ \ ADDI\<^sup>b \" nitpick oops \\ countermodel \ +lemma ADDIr_b_equ: "EXPN \ \ ADDIr\<^sup>b \ = ADDI\<^sup>b \" unfolding cond by (smt (z3) subset_def subset_out_def) + + +text\Relativized MULT variants.\ +definition MULTr::"('w \ \ 'w \) \ bool" ("MULTr") + where "MULTr \ \ \A B. let U = (A \<^bold>\ B) in (\(A \<^bold>\ B) \<^bold>=\<^sub>U (\ A) \<^bold>\ (\ B))" +definition MULTr_a::"('w \ \ 'w \) \ bool" ("MULTr\<^sup>a") + where "MULTr\<^sup>a \ \ \A B. let U = (A \<^bold>\ B) in (\(A \<^bold>\ B) \<^bold>\\<^sub>U (\ A) \<^bold>\ (\ B))" +definition MULTr_b::"('w \ \ 'w \) \ bool" ("MULTr\<^sup>b") + where "MULTr\<^sup>b \ \ \A B. let U = (A \<^bold>\ B) in ((\ A) \<^bold>\ (\ B) \<^bold>\\<^sub>U \(A \<^bold>\ B))" + +declare MULTr_def[cond] MULTr_a_def[cond] MULTr_b_def[cond] + +lemma MULTr_char: "MULTr \ = (MULTr\<^sup>a \ \ MULTr\<^sup>b \)" unfolding cond by (meson setequ_char setequ_in_char subset_in_char) + +lemma MULTr_a_impl: "MULT\<^sup>a \ \ MULTr\<^sup>a \" by (simp add: MULT_a_def MULTr_a_def subset_def subset_in_def) +lemma "nCNTR \ \ MULTr\<^sup>a \ \ MULT\<^sup>a \" nitpick oops \\ countermodel \ +lemma MULTr_a_equ: "CNTR \ \ MULTr\<^sup>a \ = MULT\<^sup>a \" unfolding cond by (smt (verit, del_insts) subset_def subset_in_def) + +lemma MULTr_b_impl: "MULT\<^sup>b \ \ MULTr\<^sup>b \" by (simp add: MULT_b_def MULTr_b_def subset_def subset_in_def) +lemma "MULTr\<^sup>b \ \ MULT\<^sup>b \" nitpick oops \\ countermodel \ +lemma MULTr_b_equ: "CNTR \ \ MULTr\<^sup>b \ = MULT\<^sup>b \" unfolding cond by (smt (verit, del_insts) meet_def subset_def subset_in_def) +lemma MULTr_b_equ':"nCNTR \ \ MULTr\<^sup>b \ = MULT\<^sup>b \" unfolding cond by (smt (z3) compl_def subset_def subset_in_def) + +text\Weak variants of monotonicity.\ +definition MONOw1::"('w \ \ 'w \) \ bool" ("MONOw\<^sup>1") + where "MONOw\<^sup>1 \ \ \A B. A \<^bold>\ B \ (\ A) \<^bold>\ B \<^bold>\ (\ B)" +definition MONOw2::"('w \ \ 'w \) \ bool" ("MONOw\<^sup>2") + where "MONOw\<^sup>2 \ \ \A B. A \<^bold>\ B \ A \<^bold>\ (\ A) \<^bold>\ (\ B)" + +declare MONOw1_def[cond] MONOw2_def[cond] + +lemma MONOw1_ADDIr_b: "MONOw\<^sup>1 \ = ADDIr\<^sup>b \" proof - + have l2r: "MONOw\<^sup>1 \ \ ADDIr\<^sup>b \" unfolding cond subset_out_char by (metis (mono_tags, opaque_lifting) L7 join_def subset_def) + have r2l: "ADDIr\<^sup>b \ \ MONOw\<^sup>1 \" unfolding cond subset_out_char by (metis (full_types) L9 join_def setequ_ext subset_def) + show ?thesis using l2r r2l by blast +qed +lemma MONOw2_MULTr_a: "MONOw\<^sup>2 \ = MULTr\<^sup>a \" proof - + have l2r: "MONOw\<^sup>2 \ \ MULTr\<^sup>a \" unfolding cond subset_in_char by (meson L4 L5 L8 L9) + have r2l:"MULTr\<^sup>a \ \ MONOw\<^sup>2 \" unfolding cond subset_in_char by (metis BA_distr1 L2 L5 L6 L9 setequ_ext) + show ?thesis using l2r r2l by blast +qed + +lemma MONOw1_impl: "MONO \ \ MONOw\<^sup>1 \" by (simp add: ADDIr_b_impl MONO_ADDIb MONOw1_ADDIr_b) +lemma "MONOw\<^sup>1 \ \ MONO \" nitpick oops \\ countermodel \ +lemma MONOw2_impl: "MONO \ \ MONOw\<^sup>2 \" by (simp add: MONO_MULTa MONOw2_MULTr_a MULTr_a_impl) +lemma "MONOw\<^sup>2 \ \ MONO \" nitpick oops \\ countermodel \ + + +text\We have in fact that (n)CNTR (resp. (n)EXPN) implies MONOw-1/ADDIr-b (resp. MONOw-2/MULTr-a).\ +lemma CNTR_MONOw1_impl: "CNTR \ \ MONOw\<^sup>1 \" by (metis CNTR_def L3 MONOw1_def subset_char1) +lemma nCNTR_MONOw1_impl: "nCNTR \ \ MONOw\<^sup>1 \" by (smt (verit, ccfv_threshold) MONOw1_def compl_def join_def nCNTR_def subset_def) +lemma EXPN_MONOw2_impl: "EXPN \ \ MONOw\<^sup>2 \" by (metis EXPN_def L4 MONOw2_def subset_char1) +lemma nEXPN_MONOw2_impl: "nEXPN \ \ MONOw\<^sup>2 \" by (smt (verit) MONOw2_def compl_def meet_def nEXPN_def subset_def) + +text\Relativized nADDI variants.\ +definition nADDIr::"('w \ \ 'w \) \ bool" ("nADDIr") + where "nADDIr \ \ \A B. let U = (A \<^bold>\ B) in (\(A \<^bold>\ B) \<^bold>=\<^sup>U (\ A) \<^bold>\ (\ B))" +definition nADDIr_a::"('w \ \ 'w \) \ bool" ("nADDIr\<^sup>a") + where "nADDIr\<^sup>a \ \ \A B. let U = (A \<^bold>\ B) in ((\ A) \<^bold>\ (\ B) \<^bold>\\<^sup>U \(A \<^bold>\ B))" +definition nADDIr_b::"('w \ \ 'w \) \ bool" ("nADDIr\<^sup>b") + where "nADDIr\<^sup>b \ \ \A B. let U = (A \<^bold>\ B) in (\(A \<^bold>\ B) \<^bold>\\<^sup>U (\ A) \<^bold>\ (\ B))" + +declare nADDIr_def[cond] nADDIr_a_def[cond] nADDIr_b_def[cond] + +lemma nADDIr_char: "nADDIr \ = (nADDIr\<^sup>a \ \ nADDIr\<^sup>b \)" unfolding cond by (meson setequ_char setequ_out_char subset_out_char) + +lemma nADDIr_a_impl: "nADDI\<^sup>a \ \ nADDIr\<^sup>a \" unfolding cond by (simp add: subset_def subset_out_def) +lemma "nADDIr\<^sup>a \ \ nADDI\<^sup>a \" nitpick oops \\ countermodel \ +lemma nADDIr_a_equ: "EXPN \ \ nADDIr\<^sup>a \ = nADDI\<^sup>a \" unfolding cond by (smt (z3) subset_def subset_out_def) +lemma nADDIr_a_equ':"nEXPN \ \ nADDIr\<^sup>a \ = nADDI\<^sup>a \" unfolding cond by (smt (z3) compl_def join_def meet_def subset_def subset_out_def) + +lemma nADDIr_b_impl: "nADDI\<^sup>b \ \ nADDIr\<^sup>b \" by (simp add: nADDI_b_def nADDIr_b_def subset_def subset_out_def) +lemma "EXPN \ \ nADDIr\<^sup>b \ \ nADDI\<^sup>b \" nitpick oops \\ countermodel \ +lemma nADDIr_b_equ: "nEXPN \ \ nADDIr\<^sup>b \ = nADDI\<^sup>b \" unfolding cond by (smt (z3) compl_def subset_def subset_out_def) + + +text\Relativized nMULT variants.\ +definition nMULTr::"('w \ \ 'w \) \ bool" ("nMULTr") + where "nMULTr \ \ \A B. let U = (A \<^bold>\ B) in (\(A \<^bold>\ B) \<^bold>=\<^sub>U (\ A) \<^bold>\ (\ B))" +definition nMULTr_a::"('w \ \ 'w \) \ bool" ("nMULTr\<^sup>a") + where "nMULTr\<^sup>a \ \ \A B. let U = (A \<^bold>\ B) in ((\ A) \<^bold>\ (\ B) \<^bold>\\<^sub>U \(A \<^bold>\ B))" +definition nMULTr_b::"('w \ \ 'w \) \ bool" ("nMULTr\<^sup>b") + where "nMULTr\<^sup>b \ \ \A B. let U = (A \<^bold>\ B) in (\(A \<^bold>\ B) \<^bold>\\<^sub>U (\ A) \<^bold>\ (\ B))" + +declare nMULTr_def[cond] nMULTr_a_def[cond] nMULTr_b_def[cond] + +lemma nMULTr_char: "nMULTr \ = (nMULTr\<^sup>a \ \ nMULTr\<^sup>b \)" unfolding cond by (meson setequ_char setequ_in_char subset_in_char) + +lemma nMULTr_a_impl: "nMULT\<^sup>a \ \ nMULTr\<^sup>a \" by (simp add: nMULT_a_def nMULTr_a_def subset_def subset_in_def) +lemma "CNTR \ \ nMULTr\<^sup>a \ \ nMULT\<^sup>a \" nitpick oops \\ countermodel \ +lemma nMULTr_a_equ: "nCNTR \ \ nMULTr\<^sup>a \ = nMULT\<^sup>a \" unfolding cond by (smt (z3) compl_def subset_def subset_in_def) + +lemma nMULTr_b_impl: "nMULT\<^sup>b \ \ nMULTr\<^sup>b \" by (simp add: nMULT_b_def nMULTr_b_def subset_def subset_in_def) +lemma "nMULTr\<^sup>b \ \ nMULT\<^sup>b \" nitpick oops \\ countermodel \ +lemma nMULTr_b_equ: "CNTR \ \ nMULTr\<^sup>b \ = nMULT\<^sup>b \" unfolding cond by (smt (z3) compl_def join_def meet_def subset_def subset_in_def) +lemma nMULTr_b_equ':"nCNTR \ \ nMULTr\<^sup>b \ = nMULT\<^sup>b \" unfolding cond by (smt (z3) compl_def join_def meet_def subset_def subset_in_def) + + +text\Weak variants of antitonicity.\ +definition ANTIw1::"('w \ \ 'w \) \ bool" ("ANTIw\<^sup>1") + where "ANTIw\<^sup>1 \ \ \A B. A \<^bold>\ B \ (\ B) \<^bold>\ B \<^bold>\ (\ A)" +definition ANTIw2::"('w \ \ 'w \) \ bool" ("ANTIw\<^sup>2") + where "ANTIw\<^sup>2 \ \ \A B. A \<^bold>\ B \ A \<^bold>\ (\ B) \<^bold>\ (\ A)" + +declare ANTIw1_def[cond] ANTIw2_def[cond] + +lemma ANTIw1_nADDIr_b: "ANTIw\<^sup>1 \ = nADDIr\<^sup>b \" proof - + have l2r: "ANTIw\<^sup>1 \ \ nADDIr\<^sup>b \" unfolding cond subset_out_char by (smt (verit, ccfv_SIG) BA_distr2 L8 join_def setequ_ext subset_def) + have r2l: "nADDIr\<^sup>b \ \ ANTIw\<^sup>1 \" unfolding cond subset_out_def by (metis (full_types) L9 join_def meet_def setequ_ext subset_def) + show ?thesis using l2r r2l by blast +qed +lemma ANTIw2_nMULTr_a: "ANTIw\<^sup>2 \ = nMULTr\<^sup>a \" proof - + have l2r: "ANTIw\<^sup>2 \ \ nMULTr\<^sup>a \" unfolding cond subset_in_char by (metis BA_distr1 L3 L4 L5 L7 L8 setequ_ext) + have r2l: "nMULTr\<^sup>a \ \ ANTIw\<^sup>2 \" unfolding cond subset_in_def by (metis (full_types) L10 join_def meet_def setequ_ext subset_def) + show ?thesis using l2r r2l by blast +qed + +lemma "ANTI \ \ ANTIw\<^sup>1 \" by (simp add: ANTI_nADDIb ANTIw1_nADDIr_b nADDIr_b_impl) +lemma "ANTIw\<^sup>1 \ \ ANTI \" nitpick oops \\ countermodel \ +lemma "ANTI \ \ ANTIw\<^sup>2 \" by (simp add: ANTI_nMULTa ANTIw2_nMULTr_a nMULTr_a_impl) +lemma "ANTIw\<^sup>2 \ \ ANTI \" nitpick oops \\ countermodel \ + +text\We have in fact that (n)CNTR (resp. (n)EXPN) implies ANTIw-1/nADDIr-b (resp. ANTIw-2/nMULTr-a).\ +lemma CNTR_ANTIw1_impl: "CNTR \ \ ANTIw\<^sup>1 \" unfolding cond using L3 subset_char1 by blast +lemma nCNTR_ANTIw1_impl: "nCNTR \ \ ANTIw\<^sup>1 \" unfolding cond by (metis (full_types) compl_def join_def subset_def) +lemma EXPN_ANTIw2_impl: "EXPN \ \ ANTIw\<^sup>2 \" unfolding cond using L4 subset_char1 by blast +lemma nEXPN_ANTIw2_impl: "nEXPN \ \ ANTIw\<^sup>2 \" unfolding cond by (metis (full_types) compl_def meet_def subset_def) + +text\Dual interrelations.\ +lemma ADDIr_dual1: "ADDIr\<^sup>a \ = MULTr\<^sup>b \\<^sup>d" unfolding cond subset_in_char subset_out_char by (smt (z3) BA_cp BA_deMorgan1 BA_dn op_dual_def setequ_ext) +lemma ADDIr_dual2: "ADDIr\<^sup>b \ = MULTr\<^sup>a \\<^sup>d" unfolding cond subset_in_char subset_out_char by (smt (verit, ccfv_threshold) BA_cp BA_deMorgan1 BA_dn op_dual_def setequ_ext) +lemma ADDIr_dual: "ADDIr \ = MULTr \\<^sup>d" using ADDIr_char ADDIr_dual1 ADDIr_dual2 MULTr_char by blast + +lemma nADDIr_dual1: "nADDIr\<^sup>a \ = nMULTr\<^sup>b \\<^sup>d" unfolding cond subset_in_char subset_out_char by (smt (verit, del_insts) BA_cp BA_deMorgan1 BA_dn op_dual_def setequ_ext) +lemma nADDIr_dual2: "nADDIr\<^sup>b \ = nMULTr\<^sup>a \\<^sup>d" by (smt (z3) BA_deMorgan1 BA_dn compl_def nADDIr_b_def nMULTr_a_def op_dual_def setequ_ext subset_in_def subset_out_def) +lemma nADDIr_dual: "nADDIr \ = nMULTr \\<^sup>d" using nADDIr_char nADDIr_dual1 nADDIr_dual2 nMULTr_char by blast + + +text\Complement interrelations.\ +lemma ADDIr_a_cmpl: "ADDIr\<^sup>a \ = nADDIr\<^sup>a \\<^sup>-" unfolding cond by (smt (verit, del_insts) BA_deMorgan1 compl_def setequ_ext subset_out_def svfun_compl_def) +lemma ADDIr_b_cmpl: "ADDIr\<^sup>b \ = nADDIr\<^sup>b \\<^sup>-" unfolding cond by (smt (verit, del_insts) BA_deMorgan1 compl_def setequ_ext subset_out_def svfun_compl_def) +lemma ADDIr_cmpl: "ADDIr \ = nADDIr \\<^sup>-" by (simp add: ADDIr_a_cmpl ADDIr_b_cmpl ADDIr_char nADDIr_char) +lemma MULTr_a_cmpl: "MULTr\<^sup>a \ = nMULTr\<^sup>a \\<^sup>-" unfolding cond by (smt (verit, del_insts) BA_deMorgan2 compl_def setequ_ext subset_in_def svfun_compl_def) +lemma MULTr_b_cmpl: "MULTr\<^sup>b \ = nMULTr\<^sup>b \\<^sup>-" unfolding cond by (smt (verit, ccfv_threshold) BA_deMorgan2 compl_def setequ_ext subset_in_def svfun_compl_def) +lemma MULTr_cmpl: "MULTr \ = nMULTr \\<^sup>-" by (simp add: MULTr_a_cmpl MULTr_b_cmpl MULTr_char nMULTr_char) + + +text\Fixed-point interrelations.\ +lemma EXPN_fp: "EXPN \ = EXPN \\<^sup>f\<^sup>p" by (simp add: EXPN_def dimpl_def op_fixpoint_def subset_def) +lemma EXPN_fpc: "EXPN \ = nEXPN \\<^sup>f\<^sup>p\<^sup>-" using EXPN_fp nEXPN_CNTR_compl by blast +lemma CNTR_fp: "CNTR \ = nCNTR \\<^sup>f\<^sup>p" by (metis EXPN_CNTR_dual1 EXPN_fp dual_compl_char2 dual_invol nCNTR_EXPN_compl ofp_comm_dc1 sfun_compl_invol) +lemma CNTR_fpc: "CNTR \ = CNTR \\<^sup>f\<^sup>p\<^sup>-" by (metis CNTR_fp nCNTR_EXPN_compl ofp_comm_compl ofp_invol) + +lemma nNORM_fp: "NORM \ = nNORM \\<^sup>f\<^sup>p" by (metis NORM_def fixpoints_def fp_rel nNORM_def) +lemma NORM_fpc: "NORM \ = NORM \\<^sup>f\<^sup>p\<^sup>-" by (simp add: NORM_def bottom_def ofp_fixpoint_compl_def sdiff_def) +lemma DNRM_fp: "DNRM \ = DNRM \\<^sup>f\<^sup>p" by (simp add: DNRM_def dimpl_def op_fixpoint_def top_def) +lemma DNRM_fpc: "DNRM \ = nDNRM \\<^sup>f\<^sup>p\<^sup>-" using DNRM_fp nDNRM_DNRM_compl by blast + +lemma ADDIr_a_fpc: "ADDIr\<^sup>a \ = ADDIr\<^sup>a \\<^sup>f\<^sup>p\<^sup>-" unfolding cond subset_out_def by (simp add: join_def ofp_fixpoint_compl_def sdiff_def) +lemma ADDIr_a_fp: "ADDIr\<^sup>a \ = nADDIr\<^sup>a \\<^sup>f\<^sup>p" by (metis ADDIr_a_cmpl ADDIr_a_fpc sfun_compl_invol) +lemma ADDIr_b_fpc: "ADDIr\<^sup>b \ = ADDIr\<^sup>b \\<^sup>f\<^sup>p\<^sup>-" unfolding cond subset_out_def by (simp add: join_def ofp_fixpoint_compl_def sdiff_def) +lemma ADDIr_b_fp: "ADDIr\<^sup>b \ = nADDIr\<^sup>b \\<^sup>f\<^sup>p" by (metis ADDIr_b_cmpl ADDIr_b_fpc sfun_compl_invol) + +lemma MULTr_a_fp: "MULTr\<^sup>a \ = MULTr\<^sup>a \\<^sup>f\<^sup>p" unfolding cond subset_in_def by (simp add: dimpl_def meet_def op_fixpoint_def) +lemma MULTr_a_fpc: "MULTr\<^sup>a \ = nMULTr\<^sup>a \\<^sup>f\<^sup>p\<^sup>-" using MULTr_a_cmpl MULTr_a_fp by blast +lemma MULTr_b_fp: "MULTr\<^sup>b \ = MULTr\<^sup>b \\<^sup>f\<^sup>p" unfolding cond subset_in_def by (simp add: dimpl_def meet_def op_fixpoint_def) +lemma MULTr_b_fpc: "MULTr\<^sup>b \ = nMULTr\<^sup>b \\<^sup>f\<^sup>p\<^sup>-" using MULTr_b_cmpl MULTr_b_fp by blast + + +text\Relativized IDEM variants.\ +definition IDEMr_a::"('w \ \ 'w \) \ bool" ("IDEMr\<^sup>a") + where "IDEMr\<^sup>a \ \ \A. \(A \<^bold>\ \ A) \<^bold>\\<^sup>A (\ A)" +definition IDEMr_b::"('w \ \ 'w \) \ bool" ("IDEMr\<^sup>b") + where "IDEMr\<^sup>b \ \ \A. (\ A) \<^bold>\\<^sub>A \(A \<^bold>\ \ A)" +declare IDEMr_a_def[cond] IDEMr_b_def[cond] + +text\Relativized nIDEM variants.\ +definition nIDEMr_a::"('w \ \ 'w \) \ bool" ("nIDEMr\<^sup>a") + where "nIDEMr\<^sup>a \ \ \A. (\ A) \<^bold>\\<^sup>A \(A \<^bold>\ \<^bold>\(\ A))" +definition nIDEMr_b::"('w \ \ 'w \) \ bool" ("nIDEMr\<^sup>b") + where "nIDEMr\<^sup>b \ \ \A. \(A \<^bold>\ \<^bold>\(\ A)) \<^bold>\\<^sub>A (\ A)" + +declare nIDEMr_a_def[cond] nIDEMr_b_def[cond] + + +text\Complement interrelations.\ +lemma IDEMr_a_cmpl: "IDEMr\<^sup>a \ = nIDEMr\<^sup>a \\<^sup>-" unfolding cond subset_in_def subset_out_def by (metis compl_def sfun_compl_invol svfun_compl_def) +lemma IDEMr_b_cmpl: "IDEMr\<^sup>b \ = nIDEMr\<^sup>b \\<^sup>-" unfolding cond subset_in_def subset_out_def by (metis compl_def sfun_compl_invol svfun_compl_def) + +text\Dual interrelation.\ +lemma IDEMr_dual: "IDEMr\<^sup>a \ = IDEMr\<^sup>b \\<^sup>d" unfolding cond subset_in_def subset_out_def op_dual_def by (metis (mono_tags, opaque_lifting) BA_dn compl_def diff_char1 diff_char2 impl_char setequ_ext) +lemma nIDEMr_dual: "nIDEMr\<^sup>a \ = nIDEMr\<^sup>b \\<^sup>d" by (metis IDEMr_dual IDEMr_a_cmpl IDEMr_b_cmpl dual_compl_char1 dual_compl_char2 sfun_compl_invol) + +text\Fixed-point interrelations.\ +lemma nIDEMr_a_fpc: "nIDEMr\<^sup>a \ = nIDEMr\<^sup>a \\<^sup>f\<^sup>p\<^sup>-" proof - + have "\A. (\p. A p \ \\ A p) = (\p. A p \ \ A p = A p)" by blast + thus ?thesis unfolding cond subset_out_def ofp_fixpoint_compl_def conn order by simp +qed +lemma IDEMr_a_fp: "IDEMr\<^sup>a \ = nIDEMr\<^sup>a \\<^sup>f\<^sup>p" by (metis IDEMr_a_cmpl nIDEMr_a_fpc ofp_invol) +lemma IDEMr_a_fpc: "IDEMr\<^sup>a \ = IDEMr\<^sup>a \\<^sup>f\<^sup>p\<^sup>-" by (metis IDEMr_a_cmpl nIDEMr_a_fpc ofp_comm_compl) +lemma IDEMr_b_fp: "IDEMr\<^sup>b \ = IDEMr\<^sup>b \\<^sup>f\<^sup>p" by (metis IDEMr_a_fpc IDEMr_dual dual_compl_char1 dual_invol ofp_comm_compl ofp_comm_dc2) +lemma IDEMr_b_fpc: "IDEMr\<^sup>b \ = nIDEMr\<^sup>b \\<^sup>f\<^sup>p\<^sup>-" using IDEMr_b_fp IDEMr_b_cmpl by blast + + +text\The original border condition B1' (by Zarycki) is equivalent to the conjuntion of nMULTr and CNTR.\ +abbreviation "B1' \ \ \A B. \(A \<^bold>\ B) \<^bold>= (A \<^bold>\ \ B) \<^bold>\ (\ A \<^bold>\ B)" + +lemma "B1' \ = (nMULTr \ \ CNTR \)" proof - + have l2ra: "B1' \ \ nMULTr \" unfolding cond by (smt (z3) join_def meet_def setequ_ext setequ_in_def) + have l2rb: "B1' \ \ CNTR \" unfolding cond by (metis L2 L4 L5 L7 L9 setequ_ext) + have r2l: "(nMULTr \ \ CNTR \) \ B1' \" unfolding cond by (smt (z3) L10 join_def meet_def setequ_def setequ_in_char) + from l2ra l2rb r2l show ?thesis by blast +qed + +text\Modulo conditions nMULTr and CNTR the border condition B4 is equivalent to nIDEMr-b.\ +abbreviation "B4 \ \ \A. \(\<^bold>\\(\<^bold>\A)) \<^bold>\ A" + +lemma "nMULTr \ \ CNTR \ \ B4 \ = nIDEMr\<^sup>b \" proof - + assume a1: "nMULTr \" and a2: "CNTR \" + have l2r: "nMULTr\<^sup>b \ \ B4 \ \ nIDEMr\<^sup>b \" unfolding cond subset_in_char subset_def by (metis BA_deMorgan1 BA_dn compl_def meet_def setequ_ext) + have r2l: "nMULTr\<^sup>a \ \ CNTR \ \ nIDEMr\<^sup>b \ \ B4 \" unfolding cond by (smt (verit) compl_def join_def meet_def subset_def subset_in_def) + from l2r r2l show ?thesis using a1 a2 nMULTr_char by blast +qed + +end diff --git a/thys/Topological_Semantics/conditions_relativized_infinitary.thy b/thys/Topological_Semantics/conditions_relativized_infinitary.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/conditions_relativized_infinitary.thy @@ -0,0 +1,80 @@ +theory conditions_relativized_infinitary + imports conditions_relativized conditions_negative_infinitary +begin + +subsection \Infinitary Relativized Conditions\ + +text\We define and interrelate infinitary variants for some previously introduced + axiomatic conditions on operators.\ + +definition iADDIr::"('w \ \ 'w \) \ bool" ("iADDIr") + where "iADDIr \ \ \S. let U=\<^bold>\S in (\(\<^bold>\S) \<^bold>=\<^sup>U \<^bold>\\\ S\)" +definition iADDIr_a::"('w \ \ 'w \) \ bool" ("iADDIr\<^sup>a") + where "iADDIr\<^sup>a \ \ \S. let U=\<^bold>\S in (\(\<^bold>\S) \<^bold>\\<^sup>U \<^bold>\\\ S\)" +definition iADDIr_b::"('w \ \ 'w \) \ bool" ("iADDIr\<^sup>b") + where "iADDIr\<^sup>b \ \ \S. let U=\<^bold>\S in (\<^bold>\\\ S\ \<^bold>\\<^sup>U \(\<^bold>\S))" + +definition inADDIr::"('w \ \ 'w \) \ bool" ("inADDIr") + where "inADDIr \ \ \S. let U=\<^bold>\S in (\(\<^bold>\S) \<^bold>=\<^sup>U \<^bold>\\\ S\)" +definition inADDIr_a::"('w \ \ 'w \) \ bool" ("inADDIr\<^sup>a") + where "inADDIr\<^sup>a \ \ \S. let U=\<^bold>\S in (\<^bold>\\\ S\ \<^bold>\\<^sup>U \(\<^bold>\S))" +definition inADDIr_b::"('w \ \ 'w \) \ bool" ("inADDIr\<^sup>b") + where "inADDIr\<^sup>b \ \ \S. let U=\<^bold>\S in (\(\<^bold>\S) \<^bold>\\<^sup>U \<^bold>\\\ S\)" + +declare iADDIr_def[cond] iADDIr_a_def[cond] iADDIr_b_def[cond] + inADDIr_def[cond] inADDIr_a_def[cond] inADDIr_b_def[cond] + +definition iMULTr::"('w \ \ 'w \) \ bool" ("iMULTr") + where "iMULTr \ \ \S. let U=\<^bold>\S in (\(\<^bold>\S) \<^bold>=\<^sub>U \<^bold>\\\ S\)" +definition iMULTr_a::"('w \ \ 'w \) \ bool" ("iMULTr\<^sup>a") + where "iMULTr\<^sup>a \ \ \S. let U=\<^bold>\S in (\(\<^bold>\S) \<^bold>\\<^sub>U \<^bold>\\\ S\)" +definition iMULTr_b::"('w \ \ 'w \) \ bool" ("iMULTr\<^sup>b") + where "iMULTr\<^sup>b \ \ \S. let U=\<^bold>\S in (\<^bold>\\\ S\ \<^bold>\\<^sub>U \(\<^bold>\S))" + +definition inMULTr::"('w \ \ 'w \) \ bool" ("inMULTr") + where "inMULTr \ \ \S. let U=\<^bold>\S in (\(\<^bold>\S) \<^bold>=\<^sub>U \<^bold>\\\ S\)" +definition inMULTr_a::"('w \ \ 'w \) \ bool" ("inMULTr\<^sup>a") + where "inMULTr\<^sup>a \ \ \S. let U=\<^bold>\S in (\<^bold>\\\ S\ \<^bold>\\<^sub>U \(\<^bold>\S))" +definition inMULTr_b::"('w \ \ 'w \) \ bool" ("inMULTr\<^sup>b") + where "inMULTr\<^sup>b \ \ \S. let U=\<^bold>\S in (\(\<^bold>\S) \<^bold>\\<^sub>U \<^bold>\\\ S\)" + +declare iMULTr_def[cond] iMULTr_a_def[cond] iMULTr_b_def[cond] + inMULTr_def[cond] inMULTr_a_def[cond] inMULTr_b_def[cond] + +lemma iADDIr_char: "iADDIr \ = (iADDIr\<^sup>a \ \ iADDIr\<^sup>b \)" unfolding cond setequ_char setequ_out_char subset_out_char by (meson setequ_char) +lemma iMULTr_char: "iMULTr \ = (iMULTr\<^sup>a \ \ iMULTr\<^sup>b \)" unfolding cond setequ_char setequ_in_char subset_in_char by (meson setequ_char) + +lemma inADDIr_char: "inADDIr \ = (inADDIr\<^sup>a \ \ inADDIr\<^sup>b \)" unfolding cond setequ_char setequ_out_char subset_out_char by (meson setequ_char) +lemma inMULTr_char: "inMULTr \ = (inMULTr\<^sup>a \ \ inMULTr\<^sup>b \)" unfolding cond setequ_char setequ_in_char subset_in_char by (meson setequ_char) + + +text\Dual interrelations.\ +lemma iADDIr_dual1: "iADDIr\<^sup>a \ = iMULTr\<^sup>b \\<^sup>d" unfolding cond by (smt (z3) BA_cmpl_equ BA_cp BA_deMorgan2 dual_invol iDM_a iDM_b im_prop1 op_dual_def setequ_ext subset_in_char subset_out_char) +lemma iADDIr_dual2: "iADDIr\<^sup>b \ = iMULTr\<^sup>a \\<^sup>d" unfolding cond by (smt (z3) BA_cmpl_equ BA_cp BA_deMorgan2 dual_invol iDM_a iDM_b im_prop1 op_dual_def setequ_ext subset_in_char subset_out_char) +lemma iADDIr_dual: "iADDIr \ = iMULTr \\<^sup>d" using iADDIr_char iADDIr_dual1 iADDIr_dual2 iMULTr_char by blast + +lemma inADDIr_dual1: "inADDIr\<^sup>a \ = inMULTr\<^sup>b \\<^sup>d" unfolding cond by (smt (z3) BA_cmpl_equ compl_def dual_invol iDM_a iDM_b im_prop3 op_dual_def setequ_ext subset_in_def subset_in_out) +lemma inADDIr_dual2: "inADDIr\<^sup>b \ = inMULTr\<^sup>a \\<^sup>d" unfolding cond by (smt (z3) BA_cmpl_equ compl_def dual_invol iDM_a iDM_b im_prop3 op_dual_def setequ_ext subset_in_def subset_in_out) +lemma inADDIr_dual: "inADDIr \ = inMULTr \\<^sup>d" using inADDIr_char inADDIr_dual1 inADDIr_dual2 inMULTr_char by blast + +text\Complement interrelations.\ +lemma iADDIr_a_cmpl: "iADDIr\<^sup>a \ = inADDIr\<^sup>a \\<^sup>-" unfolding cond by (smt (z3) compl_def dualcompl_invol iDM_b im_prop2 setequ_ext subset_out_def svfun_compl_def) +lemma iADDIr_b_cmpl: "iADDIr\<^sup>b \ = inADDIr\<^sup>b \\<^sup>-" unfolding cond by (smt (z3) compl_def iDM_b im_prop2 setequ_ext sfun_compl_invol subset_out_def svfun_compl_def) +lemma iADDIr_cmpl: "iADDIr \ = inADDIr \\<^sup>-" by (simp add: iADDIr_a_cmpl iADDIr_b_cmpl iADDIr_char inADDIr_char) + +lemma iMULTr_a_cmpl: "iMULTr\<^sup>a \ = inMULTr\<^sup>a \\<^sup>-" unfolding cond by (smt (z3) compl_def iDM_b im_prop2 setequ_ext subset_in_def svfun_compl_def) +lemma iMULTr_b_cmpl: "iMULTr\<^sup>b \ = inMULTr\<^sup>b \\<^sup>-" unfolding cond by (smt (z3) compl_def dualcompl_invol iDM_a im_prop2 setequ_ext subset_in_def svfun_compl_def) +lemma iMULTr_cmpl: "MULTr \ = nMULTr \\<^sup>-" by (simp add: MULTr_a_cmpl MULTr_b_cmpl MULTr_char nMULTr_char) + +text\Fixed-point interrelations.\ +lemma iADDIr_a_fpc: "iADDIr\<^sup>a \ = iADDIr\<^sup>a \\<^sup>f\<^sup>p\<^sup>-" unfolding cond subset_out_def image_def ofp_fixpoint_compl_def supremum_def sdiff_def by (smt (verit)) +lemma iADDIr_a_fp: "iADDIr\<^sup>a \ = inADDIr\<^sup>a \\<^sup>f\<^sup>p" by (metis iADDIr_a_cmpl iADDIr_a_fpc sfun_compl_invol) +lemma iADDIr_b_fpc: "iADDIr\<^sup>b \ = iADDIr\<^sup>b \\<^sup>f\<^sup>p\<^sup>-" unfolding cond subset_out_def image_def ofp_fixpoint_compl_def supremum_def sdiff_def by (smt (verit)) +lemma iADDIr_b_fp: "iADDIr\<^sup>b \ = inADDIr\<^sup>b \\<^sup>f\<^sup>p" by (metis iADDIr_b_cmpl iADDIr_b_fpc sfun_compl_invol) + +lemma iMULTr_a_fp: "iMULTr\<^sup>a \ = iMULTr\<^sup>a \\<^sup>f\<^sup>p" unfolding cond subset_in_def image_def by (smt (z3) dimpl_def infimum_def ofp_invol op_fixpoint_def) +lemma iMULTr_a_fpc: "iMULTr\<^sup>a \ = inMULTr\<^sup>a \\<^sup>f\<^sup>p\<^sup>-" using iMULTr_a_cmpl iMULTr_a_fp by blast +lemma iMULTr_b_fp: "iMULTr\<^sup>b \ = iMULTr\<^sup>b \\<^sup>f\<^sup>p" unfolding cond subset_in_def image_def dimpl_def infimum_def op_fixpoint_def by (smt (verit)) +lemma iMULTr_b_fpc: "iMULTr\<^sup>b \ = inMULTr\<^sup>b \\<^sup>f\<^sup>p\<^sup>-" using iMULTr_b_cmpl iMULTr_b_fp by blast + +end diff --git a/thys/Topological_Semantics/document/root.bib b/thys/Topological_Semantics/document/root.bib --- a/thys/Topological_Semantics/document/root.bib +++ b/thys/Topological_Semantics/document/root.bib @@ -1,149 +1,8 @@ -@article{J23, - keywords = {Higher Order Logic, Semantic Embedding, Modal - Logics, Henkin Semantics}, - author = {C. Benzm{\"u}ller and L.C. Paulson}, - title = {Quantified Multimodal Logics in Simple Type Theory}, - journal = {Logica Universalis (Special Issue on Multimodal - Logics)}, - year = 2013, - volume = 7, - number = 1, - pages = {7-20}, - doi = {10.1007/s11787-012-0052-y}, - Note = {Preprint: - \url{http://christoph-benzmueller.de/papers/J23.pdf}} -} - -@article{J41, - author = {Christoph Benzm{\"u}ller}, - title = {Universal (Meta-)Logical Reasoning: Recent - Successes}, - journal = {Science of Computer Programming}, - year = 2019, - volume = 172, - pages = {48-62}, - Note = {Preprint: - \url{http://doi.org/10.13140/RG.2.2.11039.61609/2}}, - doi = {10.1016/j.scico.2018.10.008}, -} - -@book{Hausdorff, - title={Grundz{\"u}ge der {M}engenlehre}, - author={Hausdorff, Felix}, - volume={7}, - year={1914}, - publisher={von Veit} -} - -@article{AOT, - title={The algebra of topology}, - author={McKinsey, John Charles Chenoweth and Tarski, Alfred}, - journal={Annals of mathematics}, - pages={141--191}, - year={1944}, - publisher={JSTOR} -} - -@article{Zarycki1, - title={Quelques notions fondamentales de l'Analysis Situs au point de vue de l'Alg{\`e}bre de la Logique}, - author={Zarycki, Miron}, - journal={Fundamenta Mathematicae}, - volume={9}, - number={1}, - pages={3--15}, - year={1927}, - publisher={Institute of Mathematics Polish Academy of Sciences}, - Note = {English translation by Mark Bowron: - \url{https://www.researchgate.net/scientific-contributions/Miron-Zarycki-2016157096}} -} - -@article{Zarycki2, - title={Allgemeine {E}igenschaften der Cantorschen {K}oh{\"a}renzen}, - author={Zarycki, Miron}, - journal={Transactions of the American Mathematical Society}, - volume={30}, - number={3}, - pages={498--506}, - year={1928}, - publisher={JSTOR}, - Note = {English translation by Mark Bowron: - \url{https://www.researchgate.net/scientific-contributions/Miron-Zarycki-2016157096}} +@article{SemanticalInvestigations, + title={Semantical Investigations on Non-Classical Logics with Recovery Operators: Negation}, + author={David Fuenmayor}, + journal = {The Logic Journal of the IGPL. Special Issue on Non-classical Modal and Predicate Logics}, + year={202X}, + publisher={Oxford University Press}, + note = {To appear (preprint: \url{https://arxiv.org/abs/2104.04284})}, } - -@article{Zarycki3, - title={Some Properties of the Derived Set Operation in Abstract Spaces.}, - author={Zarycki, Miron}, - journal={Nauk. Zap. Ser. Fiz.-Mat.}, - volume={5}, - pages={22-33}, - year={1947}, - Note = {English translation by Mark Bowron: - \url{https://www.researchgate.net/scientific-contributions/Miron-Zarycki-2016157096}} -} - -@article{Kuratowski1, - title={Sur l'op{\'e}ration \={A} de l'analysis situs}, - author={Kuratowski, Kazimierz}, - journal={Fundamenta Mathematicae}, - volume={3}, - number={1}, - pages={182--199}, - year={1922} -} - -@article{JML, - title={Der {M}inimalkalk{\"u}l, ein reduzierter intuitionistischer {F}ormalismus}, - author={Johansson, Ingebrigt}, - journal={Compositio mathematica}, - volume={4}, - pages={119--136}, - year={1937} -} - -@book{Kuratowski2, - title={Topology: Volume I}, - author={Kuratowski, Kazimierz}, - volume={1}, - year={2014}, - publisher={Elsevier} -} - -@article{Esakia, - title={Intuitionistic logic and modality via topology}, - author={Esakia, Leo}, - journal={Annals of Pure and Applied Logic}, - volume={127}, - number={1-3}, - pages={155--170}, - year={2004}, - publisher={Elsevier} -} - -@incollection{LFI, - title={Logics of formal inconsistency}, - author={Carnielli, Walter and Coniglio, Marcelo E and Marcos, Joao}, - booktitle={Handbook of philosophical logic}, - pages={1--93}, - year={2007}, - publisher={Springer} -} - -@article{RLFI, - title={Logics of Formal Inconsistency enriched with replacement: an algebraic and modal account}, - author={Walter Carnielli and Marcelo E. Coniglio and David Fuenmayor}, - year={2020}, - number={2003.09522}, - journal={arXiv}, - volume={math.LO} -} - -@article{LFU, - title={Nearly every normal modal logic is paranormal}, - author={Marcos, Joao}, - journal={Logique et Analyse}, - volume={48}, - number={189/192}, - pages={279--300}, - year={2005}, - publisher={JSTOR} -} diff --git a/thys/Topological_Semantics/document/root.tex b/thys/Topological_Semantics/document/root.tex --- a/thys/Topological_Semantics/document/root.tex +++ b/thys/Topological_Semantics/document/root.tex @@ -1,68 +1,69 @@ \documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} %\usepackage{a4wide} \usepackage{fullpage} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed \usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage{eurosym} %for \ %\usepackage[only,bigsqcap]{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{Topological semantics for paraconsistent and paracomplete logics} \author{David Fuenmayor} \maketitle \begin{abstract} - We introduce a generalized topological semantics for paraconsistent and paracomplete logics by drawing upon early works on topological Boolean algebras (cf.~works by Kuratowski, Zarycki, McKinsey \& Tarski, etc.). In particular, this work exemplarily illustrates the shallow semantical embeddings approach (SSE) employing the proof assistant Isabelle/HOL. By means of the SSE technique we can effectively harness theorem provers, model finders and `hammers' for reasoning with quantified non-classical logics. +We investigate mathematical structures that provide natural semantics for families of (quantified) non-classical logics featuring special unary connectives, known as recovery operators, that allow us to 'recover' the properties of classical logic in a controlled manner. These structures are known as topological Boolean algebras, which are Boolean algebras extended with additional operations subject to specific conditions of a topological nature. In this study we focus on the paradigmatic case of negation. We demonstrate how these algebras are well-suited to provide a semantics for some families of paraconsistent Logics of Formal Inconsistency and paracomplete Logics of Formal Undeterminedness. These logics feature recovery operators used to earmark propositions that behave 'classically' when interacting with non-classical negations. +We refer to the companion paper \cite{SemanticalInvestigations} for more information. \end{abstract} \tableofcontents \vspace*{40pt} % sane default for proof documents \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: diff --git a/thys/Topological_Semantics/logics_LFI.thy b/thys/Topological_Semantics/logics_LFI.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/logics_LFI.thy @@ -0,0 +1,131 @@ +theory logics_LFI + imports logics_consequence conditions_relativized_infinitary +begin + +subsection \Logics of Formal Inconsistency (LFIs)\ + +text\The LFIs are a family of paraconsistent logics featuring a 'consistency' operator \ +that can be used to recover some classical properties of negation (in particular ECQ). +We show a shallow semantical embedding of a family of self-extensional LFIs using the border operator +as primitive.\ + +text\Let us assume a concrete type w (for 'worlds' or 'points').\ +typedecl w +text\Let us assume the following primitive unary operation \ (intended as a border operator).\ +consts \::"w \ \ w \" + +text\From the topological cube of opposition we have that:\ +abbreviation "\ \ (\\<^sup>f\<^sup>p)\<^sup>d\<^sup>-" +abbreviation "\ \ \\<^sup>f\<^sup>p\<^sup>-" +lemma "\\<^sup>d\<^sup>- = \\<^sup>f\<^sup>p" by (simp add: dualcompl_invol) + +text\Let us recall that:\ +lemma expn_cntr: "EXPN \ = CNTR \" by (metis EXPN_CNTR_dual2 EXPN_fp ofp_comm_dc1) + +text\For LFIs we use the negation previously defined as @{text "\\<^sup>d\<^sup>- = \\<^sup>f\<^sup>p"}.\ +abbreviation neg ("\<^bold>\_"[70]71) where "neg \ \\<^sup>f\<^sup>p" + +text\In terms of the border operator the negation looks as follows (under appropriate assumptions):\ +lemma neg_char: "CNTR \ \ \<^bold>\A = (\<^bold>\A \<^bold>\ \ A)" unfolding conn by (metis CNTR_def dimpl_def op_fixpoint_def subset_def) + +text\This negation is of course boldly paraconsistent (for both local and global consequence).\ +lemma "[a, \<^bold>\a \ b]" nitpick oops \\ countermodel \ +lemma "[a, \<^bold>\a \ \<^bold>\b]" nitpick oops \\ countermodel \ +lemma "[a, \<^bold>\a \\<^sub>g b]" nitpick oops \\ countermodel \ +lemma "[a, \<^bold>\a \\<^sub>g \<^bold>\b]" nitpick oops \\ countermodel \ + +text\We define two pairs of in/consistency operators and show how they relate to each other. +Using LFIs terminology, the minimal logic so encoded corresponds to RmbC + 'ciw' axiom.\ +abbreviation op_inc_a::"w \ \ w \" ("\\<^sup>A_" [57]58) (* \ as truth-glut *) + where "\\<^sup>AA \ A \<^bold>\ \<^bold>\A" +abbreviation op_con_a::"w \ \ w \" ("\\<^sup>A_" [57]58) + where "\\<^sup>AA \ \<^bold>\\\<^sup>AA" +abbreviation op_inc_b::"w \ \ w \" ("\\<^sup>B_" [57]58) (* \ as border *) + where "\\<^sup>BA \ \ A" +abbreviation op_con_b::"w \ \ w \" ("\\<^sup>B_" [57]58) + where "\\<^sup>BA \ \\<^sup>- A" + +text\Observe that assumming CNTR \ we are allowed to exchange A and B variants.\ +lemma pincAB: "CNTR \ \ \\<^sup>AA = \\<^sup>BA" using neg_char by (metis CNTR_def CNTR_fpc L5 L6 L9 dimpl_char impl_char ofp_invol op_fixpoint_def setequ_ext svfun_compl_def) +lemma pconAB: "CNTR \ \ \\<^sup>AA = \\<^sup>BA" by (metis pincAB setequ_ext svfun_compl_def) + +text\Variants A and B give us slightly different properties (there are countermodels for those not shown).\ +lemma Prop1: "\\<^sup>BA = \\<^sup>f\<^sup>p A" by (simp add: ofp_comm_compl ofp_invol) +lemma Prop2: "\\<^sup>AA = (A \<^bold>\ \ A)" by (simp add: compl_def impl_def meet_def svfun_compl_def) +lemma Prop3: "fp \ A \ [\ \\<^sup>B\<^bold>\A]" by (simp add: fp_rel gtrue_def ofp_comm_dc2 ofp_invol op_dual_def svfun_compl_def) +lemma Prop4a: "fp \ A \ [\ \\<^sup>BA]" by (simp add: fp_rel gtrue_def ofp_comm_compl ofp_invol) +lemma Prop4b: "fp \ A \ [\ \\<^sup>AA]" by (simp add: Prop2 fixpoints_def impl_def setequ_ext) + +text\The 'principle of gentle explosion' works for both variants (both locally and globally).\ +lemma "[\\<^sup>Aa, a, \<^bold>\a \ b]" by (metis (mono_tags, lifting) compl_def meet_def subset_def) +lemma "[\\<^sup>Aa, a, \<^bold>\a \\<^sub>g b]" by (metis compl_def meet_def) +lemma "[\\<^sup>Ba, a, \<^bold>\a \ b]" by (smt (z3) meet_def ofp_fixpoint_compl_def ofp_invol sdiff_def subset_def) +lemma "[\\<^sup>Ba, a, \<^bold>\a \\<^sub>g b]" by (metis compl_def fixpoints_def fp_rel gtrue_def setequ_ext svfun_compl_def) + +abbreviation "BORDER \ \ nMULTr \ \ CNTR \ \ nDNRM \ \ nIDEMr\<^sup>b \" + +text\We show how (local) contraposition variants (among others) can be recovered using the + consistency operators.\ +lemma "[\\<^sup>Ab, a \<^bold>\ b \ \<^bold>\b \<^bold>\ \<^bold>\a]" nitpick oops \\ countermodel \ +lemma cons_lcop0_A: "CNTR \ \ [\\<^sup>Ab, a \<^bold>\ b \ \<^bold>\b \<^bold>\ \<^bold>\a]" by (smt (verit, del_insts) neg_char compl_def impl_char join_def meet_def subset_def) +lemma "[\\<^sup>Bb, a \<^bold>\ b \ \<^bold>\b \<^bold>\ \<^bold>\a]" nitpick oops \\ countermodel \ +lemma cons_lcop0_B: "CNTR \ \ [\\<^sup>Bb, a \<^bold>\ b \ \<^bold>\b \<^bold>\ \<^bold>\a]" by (metis cons_lcop0_A pconAB) +lemma "[\\<^sup>Ab, a \<^bold>\ \<^bold>\b \ b \<^bold>\ \<^bold>\a]" nitpick oops \\ countermodel \ +lemma cons_lcop1_A: "CNTR \ \ [\\<^sup>Ab, a \<^bold>\ \<^bold>\b \ b \<^bold>\ \<^bold>\a]" by (smt (verit, del_insts) neg_char compl_def impl_char join_def meet_def subset_def) +lemma "[\\<^sup>Bb, a \<^bold>\ \<^bold>\b \ b \<^bold>\ \<^bold>\a]" nitpick oops \\ countermodel \ +lemma cons_lcop1_B: "CNTR \ \ [\\<^sup>Bb, a \<^bold>\ \<^bold>\b \ b \<^bold>\ \<^bold>\a]" by (metis cons_lcop1_A pconAB) +lemma "[\\<^sup>Ab, \<^bold>\a \<^bold>\ b \ \<^bold>\b \<^bold>\ a]" nitpick oops \\ countermodel \ +lemma cons_lcop2_A: "CNTR \ \ [\\<^sup>Ab, \<^bold>\a \<^bold>\ b \ \<^bold>\b \<^bold>\ a]" by (smt (verit, del_insts) neg_char compl_def impl_char join_def meet_def subset_def) +lemma "[\\<^sup>Bb, \<^bold>\a \<^bold>\ b \ \<^bold>\b \<^bold>\ a]" nitpick oops \\ countermodel \ +lemma cons_lcop2_B: "CNTR \ \ [\\<^sup>Bb, \<^bold>\a \<^bold>\ b \ \<^bold>\b \<^bold>\ a]" by (metis cons_lcop2_A pconAB) + +text\The following axioms are commonly employed in the literature on LFIs to obtain stronger logics. +We explore under which conditions they can be assumed while keeping the logic boldly paraconsistent.\ +abbreviation cf where "cf \ \P. [\<^bold>\\<^bold>\P \ P]" +abbreviation ce where "ce \ \P. [P \ \<^bold>\\<^bold>\P]" +abbreviation ciw_a where "ciw_a \ \P. [\ \\<^sup>AP \<^bold>\ \\<^sup>AP]" +abbreviation ciw_b where "ciw_b \ \P. [\ \\<^sup>BP \<^bold>\ \\<^sup>BP]" +abbreviation ci_a where "ci_a \ \P. [\<^bold>\(\\<^sup>AP) \ \\<^sup>AP]" +abbreviation ci_b where "ci_b \ \P. [\<^bold>\(\\<^sup>BP) \ \\<^sup>BP]" +abbreviation cl_a where "cl_a \ \P. [\<^bold>\(\\<^sup>AP) \ \\<^sup>AP]" +abbreviation cl_b where "cl_b \ \P. [\<^bold>\(\\<^sup>BP) \ \\<^sup>BP]" +abbreviation ca_conj_a where "ca_conj_a \ \P Q. [\\<^sup>AP,\\<^sup>AQ \ \\<^sup>A(P \<^bold>\ Q)]" +abbreviation ca_conj_b where "ca_conj_b \ \P Q. [\\<^sup>BP,\\<^sup>BQ \ \\<^sup>B(P \<^bold>\ Q)]" +abbreviation ca_disj_a where "ca_disj_a \ \P Q. [\\<^sup>AP,\\<^sup>AQ \ \\<^sup>A(P \<^bold>\ Q)]" +abbreviation ca_disj_b where "ca_disj_b \ \P Q. [\\<^sup>BP,\\<^sup>BQ \ \\<^sup>B(P \<^bold>\ Q)]" +abbreviation ca_impl_a where "ca_impl_a \ \P Q. [\\<^sup>AP,\\<^sup>AQ \ \\<^sup>A(P \<^bold>\ Q)]" +abbreviation ca_impl_b where "ca_impl_b \ \P Q. [\\<^sup>BP,\\<^sup>BQ \ \\<^sup>B(P \<^bold>\ Q)]" +abbreviation ca_a where "ca_a \ ca_conj_a \ ca_disj_a \ ca_impl_a" +abbreviation ca_b where "ca_b \ ca_conj_b \ ca_disj_b \ ca_impl_b" + +text\cf\ +lemma "BORDER \ \ cf" nitpick oops \\ countermodel \ + +text\ce\ +lemma "BORDER \ \ ce" nitpick oops \\ countermodel \ + +text\ciw\ +lemma prop_ciw_a: "ciw_a" by (simp add: conn) +lemma prop_ciw_b: "ciw_b" by (simp add: conn svfun_compl_def) + +text\ci\ +lemma "BORDER \ \ ci_a" nitpick oops \\ countermodel \ +lemma "BORDER \ \ ci_b" nitpick oops \\ countermodel \ + +text\cl\ +lemma "BORDER \ \ cl_a" nitpick oops \\ countermodel \ +lemma "BORDER \ \ cl_b" nitpick oops \\ countermodel \ + +text\ca_conj\ +lemma prop_ca_conj_b: "nMULT\<^sup>b \ = ca_conj_b" by (metis MULT_b_def nMULTb_compl sfun_compl_invol) +lemma prop_ca_conj_a: "nMULTr\<^sup>b \ = ca_conj_a" unfolding cond op_fixpoint_def by (smt (z3) compl_def dimpl_def join_def meet_def op_fixpoint_def subset_def subset_in_def) + +text\ca_disj\ +lemma prop_ca_disj_b: "ADDI\<^sup>a \ = ca_disj_b" by (simp add: nADDI_a_def nADDIa_compl) +lemma prop_ca_disj_a: "nMULTr\<^sup>a \ = ca_disj_a" oops (*TODO*) + +text\ca_impl\ +lemma "BORDER \ \ ca_impl_a" nitpick oops \\ countermodel \ +lemma "BORDER \ \ ca_impl_b" nitpick oops \\ countermodel \ + +end diff --git a/thys/Topological_Semantics/logics_LFU.thy b/thys/Topological_Semantics/logics_LFU.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/logics_LFU.thy @@ -0,0 +1,81 @@ +theory logics_LFU + imports logics_consequence conditions_relativized_infinitary +begin + +subsection \Logics of Formal Undeterminedness (LFUs)\ + +text\The LFUs are a family of paracomplete logics featuring a 'determinedness' operator \ +that can be used to recover some classical properties of negation (in particular TND). +LFUs behave in a sense dually to LFIs. Both can be semantically embedded as extensions of Boolean algebras. +We show a shallow semantical embedding of a family of self-extensional LFUs using the closure operator +as primitive.\ + +(*Let us assume a concrete type w (for 'worlds' or 'points').*) +typedecl w +(*Let us assume the following primitive unary operation \ (intended as a closure operator).*) +consts \::"w \ \ w \" + +(*From the topological cube of opposition:*) +abbreviation "\ \ \\<^sup>d" +abbreviation "\ \ (\\<^sup>f\<^sup>p)\<^sup>d" + +(*let us recall that: *) +lemma "EXPN \ = CNTR \" using EXPN_CNTR_dual1 EXPN_fp by blast +lemma "EXPN \ = CNTR \" by (simp add: EXPN_CNTR_dual1) + +text\For LFUs we use the negation previously defined as @{text "\\<^sup>d\<^sup>- = \\<^sup>-"}.\ +abbreviation neg ("\<^bold>\_"[70]71) where "neg \ \\<^sup>-" + +text\In terms of the border operator the negation looks as follows:\ +lemma neg_char: "EXPN \ \ \<^bold>\A = (\<^bold>\A \<^bold>\ \\<^sup>d A)" unfolding conn by (metis EXPN_def compl_def dimpl_def dual_invol op_fixpoint_def subset_def svfun_compl_def) + +abbreviation "CLOSURE \ \ ADDI \ \ EXPN \ \ NORM \ \ IDEM \" + +text\This negation is of course paracomplete.\ +lemma "CLOSURE \ \ [\ a \<^bold>\ \<^bold>\a]" nitpick oops \\ countermodel \ + +text\We define two pairs of un/determinedness operators and show how they relate to each other. +This logic corresponds to the paracomplete dual of the LFI 'RmbC-ciw'.\ +abbreviation op_det_a::"w \ \ w \" ("\\<^sup>A_" [57]58) + where "\\<^sup>AA \ A \<^bold>\ \<^bold>\A" +abbreviation op_und_a::"w \ \ w \" ("\\<^sup>A_" [57]58) (* \ as truth-gap *) + where "\\<^sup>AA \ \<^bold>\\\<^sup>AA" +abbreviation op_det_b::"w \ \ w \" ("\\<^sup>B_" [57]58) + where "\\<^sup>BA \ \\<^sup>d A" +abbreviation op_und_b::"w \ \ w \" ("\\<^sup>B_" [57]58) (* \ as border of the complement *) + where "\\<^sup>BA \ \\<^sup>d\<^sup>- A" + + +text\Observe that assumming EXPN \ we are allowed to exchange A and B variants.\ +lemma pundAB: "EXPN \ \ \\<^sup>AA = \\<^sup>BA" using neg_char by (metis BA_deMorgan1 BA_dn L4 L9 dimpl_char impl_char ofp_comm_dc2 op_fixpoint_def sdfun_dcompl_def setequ_ext svfun_compl_def) +lemma pdetAB: "EXPN \ \ \\<^sup>AA = \\<^sup>BA" by (metis dual_compl_char1 pundAB sfun_compl_invol svfun_compl_def) + +text\Variants A and B give us slightly different properties (there are countermodels for those not shown).\ +lemma Prop1: "\\<^sup>BA = \\<^sup>f\<^sup>p A" by (simp add: dual_invol setequ_ext) +lemma Prop2: "\\<^sup>AA = (\ A \<^bold>\ A)" unfolding conn by (metis compl_def svfun_compl_def) +lemma Prop3: "fp \ A \ [\ \\<^sup>B\<^bold>\A]" by (simp add: dual_invol fp_d_rel gtrue_def) +lemma Prop4a: "fp \ A \ [\ \\<^sup>BA]" by (simp add: dual_invol fp_rel gtrue_def) +lemma Prop4b: "fp \ A \ [\ \\<^sup>AA]" by (simp add: compl_def fixpoints_def join_def setequ_ext svfun_compl_def) + +text\Recovering TND works for both variants.\ +lemma "[\\<^sup>Aa \ a, \<^bold>\a]" by (simp add: subset_def) +lemma "[\ \\<^sup>Aa \<^bold>\ a \<^bold>\ \<^bold>\a]" by (metis compl_def join_def) +lemma "[\\<^sup>Ba \ a, \<^bold>\a]" by (simp add: compl_def dimpl_def dual_invol join_def op_fixpoint_def subset_def svfun_compl_def) +lemma "[\ \\<^sup>Ba \<^bold>\ a \<^bold>\ \<^bold>\a]" by (metis dimpl_def dual_compl_char1 dual_invol join_def ofp_comm_compl op_fixpoint_def) + +text\We show how (local) contraposition variants (among others) can be recovered using the + determinedness operators.\ +lemma "[\\<^sup>Aa, a \<^bold>\ b \ \<^bold>\b \<^bold>\ \<^bold>\a]" nitpick oops +lemma det_lcop0_A: "EXPN \ \ [\\<^sup>Aa, a \<^bold>\ b \ \<^bold>\b \<^bold>\ \<^bold>\a]" using neg_char impl_char unfolding conn order by fastforce +lemma "[\\<^sup>Ba, a \<^bold>\ b \ \<^bold>\b \<^bold>\ \<^bold>\a]" nitpick oops +lemma det_lcop0_B: "EXPN \ \ [\\<^sup>Ba, a \<^bold>\ b \ \<^bold>\b \<^bold>\ \<^bold>\a]" by (metis det_lcop0_A pdetAB) +lemma "[\\<^sup>Aa, a \<^bold>\ \<^bold>\b \ b \<^bold>\ \<^bold>\a]" nitpick oops +lemma det_lcop1_A: "EXPN \ \ [\\<^sup>Aa, a \<^bold>\ \<^bold>\b \ b \<^bold>\ \<^bold>\a]" by (smt (verit, ccfv_SIG) impl_char impl_def join_def meet_def neg_char subset_def) +lemma "[\\<^sup>Ba, a \<^bold>\ \<^bold>\b \ b \<^bold>\ \<^bold>\a]" nitpick oops +lemma det_lcop1_B: "EXPN \ \ [\\<^sup>Ba, a \<^bold>\ \<^bold>\b \ b \<^bold>\ \<^bold>\a]" by (metis det_lcop1_A pdetAB) +lemma "[\\<^sup>Aa, \<^bold>\a \<^bold>\ b \ \<^bold>\b \<^bold>\ a]" nitpick oops +lemma det_lcop2_A: "EXPN \ \ [\\<^sup>Aa, \<^bold>\a \<^bold>\ b \ \<^bold>\b \<^bold>\ a]" by (smt (verit, del_insts) neg_char compl_def impl_char join_def meet_def subset_def) +lemma "[\\<^sup>Ba, \<^bold>\a \<^bold>\ b \ \<^bold>\b \<^bold>\ a]" nitpick oops +lemma det_lcop2_B: "EXPN \ \ [\\<^sup>Ba, \<^bold>\a \<^bold>\ b \ \<^bold>\b \<^bold>\ a]" by (metis det_lcop2_A pdetAB) + +end diff --git a/thys/Topological_Semantics/logics_consequence.thy b/thys/Topological_Semantics/logics_consequence.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/logics_consequence.thy @@ -0,0 +1,33 @@ +theory logics_consequence + imports boolean_algebra +begin + +section \Logics based on Topological Boolean Algebras\ + +subsection \Logical Consequence and Validity\ + +text\Logical validity can be defined as truth in all points (i.e. as denoting the top element).\ +abbreviation (input) gtrue::"'w \ \ bool" ("[\ _]") + where "[\ A] \ \w. A w" +lemma gtrue_def: "[\ A] \ A \<^bold>= \<^bold>\" by (simp add: setequ_def top_def) + +text\When defining a logic over an existing algebra we have two choices: a global (truth preserving) +and a local (degree preserving) notion of logical consequence. For LFIs/LFUs we prefer the latter.\ +abbreviation (input) conseq_global1::"'w \ \ 'w \\bool" ("[_ \\<^sub>g _]") + where "[A \\<^sub>g B] \ [\ A] \ [\ B]" +abbreviation (input) conseq_global21::"'w \ \ 'w \ \ 'w \ \ bool" ("[_,_ \\<^sub>g _]") + where "[A\<^sub>1, A\<^sub>2 \\<^sub>g B] \ [\ A\<^sub>1] \ [\ A\<^sub>2] \ [\ B]" +abbreviation (input) conseq_global31::"'w \ \ 'w \ \ 'w \ \ 'w \ \ bool" ("[_,_,_ \\<^sub>g _]") + where "[A\<^sub>1, A\<^sub>2, A\<^sub>3 \\<^sub>g B] \ [\ A\<^sub>1] \ [\ A\<^sub>2] \ [\ A\<^sub>3] \ [\ B]" + +abbreviation (input) conseq_local1::"'w \ \ 'w \ \ bool" ("[_ \ _]") + where "[A \ B] \ A \<^bold>\ B" +abbreviation (input) conseq_local21::"'w \ \ 'w \ \ 'w \ \ bool" ("[_,_ \ _]") + where "[A\<^sub>1, A\<^sub>2 \ B] \ A\<^sub>1 \<^bold>\ A\<^sub>2 \<^bold>\ B" +abbreviation (input) conseq_local12::"'w \ \ 'w \ \ 'w \ \ bool" ("[_ \ _,_]") + where "[A \ B\<^sub>1, B\<^sub>2] \ A \<^bold>\ B\<^sub>1 \<^bold>\ B\<^sub>2" +abbreviation (input) conseq_local31::"'w \ \ 'w \ \ 'w \ \ 'w \ \ bool" ("[_,_,_ \ _]") + where "[A\<^sub>1, A\<^sub>2, A\<^sub>3 \ B] \ A\<^sub>1 \<^bold>\ A\<^sub>2 \<^bold>\ A\<^sub>3 \<^bold>\ B" +(*add more as the need arises...*) + +end diff --git a/thys/Topological_Semantics/logics_negation.thy b/thys/Topological_Semantics/logics_negation.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/logics_negation.thy @@ -0,0 +1,271 @@ +theory logics_negation + imports logics_consequence conditions_relativized +begin + +subsection \Properties of negation(-like) operators\ + +text\To avoid visual clutter we introduce convenient notation for type for properties of operators.\ +type_synonym 'w \ = "('w \ \ 'w \) \ bool" + +named_theorems neg (*to group together definitions for properties of negations*) + + +subsubsection \Principles of excluded middle, contradiction and explosion\ + +text\TND: tertium non datur, aka. law of excluded middle (resp. strong, weak, minimal).\ +abbreviation pTND ("TND\<^sup>_ _") where "TND\<^sup>a \ \ [\ a \<^bold>\ \ a]" +abbreviation pTNDw ("TNDw\<^sup>_ _") where "TNDw\<^sup>a \ \ \b. [\ b \ a, \ a]" +abbreviation pTNDm ("TNDm\<^sup>_ _") where "TNDm\<^sup>a \ \ [\ \<^bold>\ \ a, \ a]" +definition TND ::"'w \" where "TND \ \ \\. TND\<^sup>\ \" +definition TNDw::"'w \" where "TNDw \ \ \\. TNDw\<^sup>\ \" +definition TNDm::"'w \" where "TNDm \ \ \\. TNDm\<^sup>\ \" +declare TND_def[neg] TNDw_def[neg] TNDm_def[neg] + +text\Explore some (non)entailment relations.\ +lemma "TND \ \ TNDw \" unfolding neg conn order by simp +lemma "TNDw \ \ TND \" nitpick oops \\ counterexample \ +lemma "TNDw \ \ TNDm \" unfolding neg by simp +lemma "TNDm \ \ TNDw \" nitpick oops \\ counterexample \ + +text\ECQ: ex contradictione (sequitur) quodlibet (variants: strong, weak, minimal).\ +abbreviation pECQ ("ECQ\<^sup>_ _") where "ECQ\<^sup>a \ \ [a, \ a \ \<^bold>\]" +abbreviation pECQw ("ECQw\<^sup>_ _") where "ECQw\<^sup>a \ \ \b. [a, \ a \ \ b]" +abbreviation pECQm ("ECQm\<^sup>_ _") where "ECQm\<^sup>a \ \ [a, \ a \ \ \<^bold>\]" +definition ECQ ::"'w \" where "ECQ \ \ \a. ECQ\<^sup>a \" +definition ECQw::"'w \" where "ECQw \ \ \a. ECQw\<^sup>a \" +definition ECQm::"'w \" where "ECQm \ \ \a. ECQm\<^sup>a \" +declare ECQ_def[neg] ECQw_def[neg] ECQm_def[neg] + +text\Explore some (non)entailment relations.\ +lemma "ECQ \ \ ECQw \" unfolding neg conn order by blast +lemma "ECQw \ \ ECQ \" nitpick oops \\ counterexample \ +lemma "ECQw \ \ ECQm \" unfolding neg by simp +lemma "ECQm \ \ ECQw \" nitpick oops \\ counterexample \ + +text\LNC: law of non-contradiction.\ +abbreviation pLNC ("LNC\<^sup>_ _") where "LNC\<^sup>a \ \ [\ \(a \<^bold>\ \ a)]" +definition LNC::"'w \" where "LNC \ \ \a. LNC\<^sup>a \" +declare LNC_def[neg] + +text\ECQ and LNC are in general independent.\ +lemma "ECQ \ \ LNC \" nitpick oops \\ counterexample \ +lemma "LNC \ \ ECQm \" nitpick oops \\ counterexample \ + + +subsubsection \Contraposition rules\ + +text\CoP: contraposition (weak 'rule-like' variants). +Variant 0 is antitonicity (ANTI). Variants 1-3 are stronger.\ +abbreviation pCoP1 ("CoP1\<^sup>_\<^sup>_ _") where "CoP1\<^sup>a\<^sup>b \ \ [a \ \ b] \ [b \ \ a]" +abbreviation pCoP2 ("CoP2\<^sup>_\<^sup>_ _") where "CoP2\<^sup>a\<^sup>b \ \ [\ a \ b] \ [\ b \ a]" +abbreviation pCoP3 ("CoP3\<^sup>_\<^sup>_ _") where "CoP3\<^sup>a\<^sup>b \ \ [\ a \ \ b] \ [b \ a]" + +abbreviation CoP0 ::"'w \" where "CoP0 \ \ ANTI \" +definition CoP1 ::"'w \" where "CoP1 \ \ \a b. CoP1\<^sup>a\<^sup>b \" +definition CoP2 ::"'w \" where "CoP2 \ \ \a b. CoP2\<^sup>a\<^sup>b \" +definition CoP3 ::"'w \" where "CoP3 \ \ \a b. CoP3\<^sup>a\<^sup>b \" + +declare CoP1_def[neg] CoP2_def[neg] CoP3_def[neg] + +text\Explore some (non)entailment relations.\ +lemma "CoP1 \ \ CoP0 \" unfolding ANTI_def CoP1_def using subset_char1 by blast +lemma "CoP0 \ \ CoP1 \" nitpick oops \\ counterexample \ +lemma "CoP2 \ \ CoP0 \" unfolding ANTI_def CoP2_def using subset_char1 by blast +lemma "CoP0 \ \ CoP2 \" nitpick oops \\ counterexample \ +lemma "CoP3 \ \ CoP0 \" oops (*TODO*) +lemma "CoP0 \ \ CoP3 \" nitpick oops \\ counterexample \ + +text\All three strong variants are pairwise independent. However, CoP3 follows from CoP1 plus CoP2.\ +lemma CoP123: "CoP1 \ \ CoP2 \ \ CoP3 \" unfolding neg order by smt +text\Taking all CoP together still leaves room for a boldly paraconsistent resp. paracomplete logic.\ +lemma "CoP1 \ \ CoP2 \ \ ECQm \" nitpick oops \\ counterexample \ +lemma "CoP1 \ \ CoP2 \ \ TNDm \" nitpick oops \\ counterexample \ + + +subsubsection \Modus tollens rules\ + +text\MT: modus (tollendo) tollens (weak 'rule-like' variants).\ +abbreviation pMT0 ("MT0\<^sup>_\<^sup>_ _") where "MT0\<^sup>a\<^sup>b \ \ [a \ b] \ [\ \ b] \ [\ \ a]" +abbreviation pMT1 ("MT1\<^sup>_\<^sup>_ _") where "MT1\<^sup>a\<^sup>b \ \ [a \ \ b] \ [\ b] \ [\ \ a]" +abbreviation pMT2 ("MT2\<^sup>_\<^sup>_ _") where "MT2\<^sup>a\<^sup>b \ \ [\ a \ b] \ [\ \ b] \ [\ a]" +abbreviation pMT3 ("MT3\<^sup>_\<^sup>_ _") where "MT3\<^sup>a\<^sup>b \ \ [\ a \ \ b] \ [\ b] \ [\ a]" +definition MT0::"'w \" where "MT0 \ \ \a b. MT0\<^sup>a\<^sup>b \" +definition MT1::"'w \" where "MT1 \ \ \a b. MT1\<^sup>a\<^sup>b \" +definition MT2::"'w \" where "MT2 \ \ \a b. MT2\<^sup>a\<^sup>b \" +definition MT3::"'w \" where "MT3 \ \ \a b. MT3\<^sup>a\<^sup>b \" + +declare MT0_def[neg] MT1_def[neg] MT2_def[neg] MT3_def[neg] + +text\Again, all MT variants are pairwise independent. We explore some (non)entailment relations.\ +lemma "CoP0 \ \ MT0 \" unfolding neg order cond conn by blast +lemma "CoP1 \ \ MT1 \" unfolding neg order conn by blast +lemma "CoP2 \ \ MT2 \" unfolding neg order conn by blast +lemma "CoP3 \ \ MT3 \" unfolding neg order conn by blast +lemma "MT0 \ \ MT1 \ \ MT2 \ \ MT3 \ \ CoP0 \" nitpick oops \\ counterexample \ +lemma "MT0 \ \ MT1 \ \ MT2 \ \ MT3 \ \ ECQm \" nitpick oops \\ counterexample \ +lemma "MT0 \ \ MT1 \ \ MT2 \ \ MT3 \ \ TNDm \" nitpick oops \\ counterexample \ +lemma MT123: "MT1 \ \ MT2 \ \ MT3 \" unfolding neg order conn by metis + + +subsubsection \Double negation introduction and elimination\ + +text\DNI/DNE: double negation introduction/elimination (strong 'axiom-like' variants).\ +abbreviation pDNI ("DNI\<^sup>_ _") where "DNI\<^sup>a \ \ [a \ \(\ a)]" +abbreviation pDNE ("DNE\<^sup>_ _") where "DNE\<^sup>a \ \ [\(\ a) \ a]" +definition DNI::"'w \" where "DNI \ \ \a. DNI\<^sup>a \" +definition DNE::"'w \" where "DNE \ \ \a. DNE\<^sup>a \" +declare DNI_def[neg] DNE_def[neg] + +text\CoP1 (resp. CoP2) can alternatively be defined as CoPw plus DNI (resp. DNE).\ +lemma "DNI \ \ CoP1 \" nitpick oops \\ counterexample \ +lemma CoP1_def2: "CoP1 \ = (CoP0 \ \ DNI \)" unfolding neg cond using subset_char2 by blast +lemma "DNE \ \ CoP2 \" nitpick oops \\ counterexample \ +lemma CoP2_def2: "CoP2 \ = (CoP0 \ \ DNE \)" unfolding neg cond using subset_char1 by blast + +text\Explore some non-entailment relations:\ +lemma "DNI \ \ DNE \ \ CoP0 \" nitpick oops \\ counterexample \ +lemma "DNI \ \ DNE \ \ TNDm \" nitpick oops \\ counterexample \ +lemma "DNI \ \ DNE \ \ ECQm \" nitpick oops \\ counterexample \ +lemma "DNI \ \ DNE \ \ MT0 \" nitpick oops \\ counterexample \ +lemma "DNI \ \ DNE \ \ MT1 \" nitpick oops \\ counterexample \ +lemma "DNI \ \ DNE \ \ MT2 \" nitpick oops \\ counterexample \ +lemma "DNI \ \ DNE \ \ MT3 \" nitpick oops \\ counterexample \ + +text\DNI/DNE: double negation introduction/elimination (weak 'rule-like' variants).\ +abbreviation prDNI ("rDNI\<^sup>_ _") where "rDNI\<^sup>a \ \ [\ a] \ [\ \(\ a)]" +abbreviation prDNE ("rDNE\<^sup>_ _") where "rDNE\<^sup>a \ \ [\ \(\ a)] \ [\ a]" +definition rDNI::"'w \" where "rDNI \ \ \a. rDNI\<^sup>a \" +definition rDNE::"'w \" where "rDNE \ \ \a. rDNE\<^sup>a \" +declare rDNI_def[neg] rDNE_def[neg] + +text\The 'rule-like' variants for DNI/DNE are strictly weaker than the 'axiom-like' ones.\ +lemma "DNI \ \ rDNI \" unfolding neg order conn by simp +lemma "rDNI \ \ DNI \" nitpick oops \\ counterexample \ +lemma "DNE \ \ rDNE \" unfolding neg order conn by blast +lemma "rDNE \ \ DNE \" nitpick oops \\ counterexample \ +text\The 'rule-like' variants for DNI/DNE follow already from modus tollens.\ +lemma MT1_rDNI: "MT1 \ \ rDNI \" unfolding neg order by blast +lemma MT2_rDNE: "MT2 \ \ rDNE \" unfolding neg order by blast + + +subsubsection \(Anti)Normality and its dual\ + +text\nNORM (resp. nDNRM) is entailed by CoP1 (resp. CoP2). \ +lemma CoP1_NORM: "CoP1 \ \ nNORM \" unfolding neg cond conn order by simp +lemma CoP2_DNRM: "CoP2 \ \ nDNRM \" unfolding neg cond conn by (smt (verit) setequ_char subset_def) +lemma "DNI \ \ nNORM \" nitpick oops \\ counterexample \ +lemma "DNE \ \ nDNRM \" nitpick oops \\ counterexample \ +text\nNORM and nDNRM together entail the rule variant of DNI (rDNI).\ +lemma nDNRM_rDNI: "nNORM \ \ nDNRM \ \ rDNI \" unfolding neg cond by (simp add: gtrue_def setequ_ext) +lemma "nNORM \ \ nDNRM \ \ rDNE \" nitpick oops \\ counterexample \ + + +subsubsection \De Morgan laws\ + +text\De Morgan laws correspond to anti-additivity and anti-multiplicativity).\ + +text\DM3 (resp. DM4) are entailed by CoP0/ANTI together with DNE (resp. DNI).\ +lemma CoP0_DNE_nMULTb: "CoP0 \ \ DNE \ \ nMULT\<^sup>b \" unfolding neg cond by (metis ANTI_def ANTI_nADDIb L12 nADDI_b_def subset_char1) +lemma CoP0_DNI_nADDIa: "CoP0 \ \ DNI \ \ nADDI\<^sup>a \" unfolding neg cond by (metis ANTI_def ANTI_nMULTa L11 nMULT_a_def subset_char2) + +text\From this follows that DM3 (resp. DM4) is entailed by CoP2 (resp. CoP1).\ +lemma CoP2_nMULTb: "CoP2 \ \ nMULT\<^sup>b \" by (simp add: CoP0_DNE_nMULTb CoP2_def2) +lemma CoP1_nADDIa: "CoP1 \ \ nADDI\<^sup>a \" by (simp add: CoP0_DNI_nADDIa CoP1_def2) + +text\Explore some non-entailment relations:\ +lemma "CoP0 \ \ nADDI\<^sup>a \ \ nMULT\<^sup>b \ \ nNORM \ \ nDNRM \ \ DNI \" nitpick oops \\ counterexample \ +lemma "CoP0 \ \ nADDI\<^sup>a \ \ nMULT\<^sup>b \ \ nNORM \ \ nDNRM \ \ DNE \" nitpick oops \\ counterexample \ +lemma "CoP0 \ \ nADDI\<^sup>a \ \ nMULT\<^sup>b \ \ DNI \ \ DNE \ \ ECQm \" nitpick oops \\ counterexample \ +lemma "CoP0 \ \ nADDI\<^sup>a \ \ nMULT\<^sup>b \ \ DNI \ \ DNE \ \ TNDm \" nitpick oops \\ counterexample \ + +subsubsection \Strong contraposition (axiom-like)\ +text\Observe that the definitions below take implication as an additional parameter: \.\ + +text\lCoP: (local) contraposition (strong 'axiom-like' variants, using local consequence).\ +abbreviation plCoP0 ("lCoP0\<^sup>_\<^sup>_ _ _") where "lCoP0\<^sup>a\<^sup>b \ \ \ [\ a b \ \ (\ b) (\ a)]" +abbreviation plCoP1 ("lCoP1\<^sup>_\<^sup>_ _ _") where "lCoP1\<^sup>a\<^sup>b \ \ \ [\ a (\ b) \ \ b (\ a)]" +abbreviation plCoP2 ("lCoP2\<^sup>_\<^sup>_ _ _") where "lCoP2\<^sup>a\<^sup>b \ \ \ [\ (\ a) b \ \ (\ b) a]" +abbreviation plCoP3 ("lCoP3\<^sup>_\<^sup>_ _ _") where "lCoP3\<^sup>a\<^sup>b \ \ \ [\ (\ a) (\ b) \ \ b a]" +definition lCoP0::"('w \\'w \\'w \) \ 'w \" where "lCoP0 \ \ \ \a b. lCoP0\<^sup>a\<^sup>b \ \" +definition lCoP1::"('w \\'w \\'w \) \ 'w \" where "lCoP1 \ \ \ \a b. lCoP1\<^sup>a\<^sup>b \ \" +definition lCoP2::"('w \\'w \\'w \) \ 'w \" where "lCoP2 \ \ \ \a b. lCoP2\<^sup>a\<^sup>b \ \" +definition lCoP3::"('w \\'w \\'w \) \ 'w \" where "lCoP3 \ \ \ \a b. lCoP3\<^sup>a\<^sup>b \ \" + +declare lCoP0_def[neg] lCoP1_def[neg] lCoP2_def[neg] lCoP3_def[neg] + +text\All these contraposition variants are in general independent from each other. +However if we employ classical implication we can verify some relationships.\ + +lemma lCoP1_def2: "lCoP1(\<^bold>\) \ = (lCoP0(\<^bold>\) \ \ DNI \)" unfolding neg conn order by metis +lemma lCoP2_def2: "lCoP2(\<^bold>\) \ = (lCoP0(\<^bold>\) \ \ DNE \)" unfolding neg conn order by blast +lemma "lCoP1(\<^bold>\) \ \ lCoP0(\<^bold>\) \" unfolding neg conn order by blast +lemma "lCoP0(\<^bold>\) \ \ lCoP1(\<^bold>\) \" nitpick oops \\ counterexample \ +lemma "lCoP2(\<^bold>\) \ \ lCoP0(\<^bold>\) \" unfolding neg conn order by blast +lemma "lCoP0(\<^bold>\) \ \ lCoP2(\<^bold>\) \" nitpick oops \\ counterexample \ +lemma "lCoP3(\<^bold>\) \ \ lCoP0(\<^bold>\) \" unfolding neg conn order by blast +lemma "lCoP0(\<^bold>\) \ \ lCoP3(\<^bold>\) \" nitpick oops \\ counterexample \ +lemma lCoP123: "lCoP1(\<^bold>\) \ \ lCoP2(\<^bold>\) \ \ lCoP3(\<^bold>\) \" unfolding neg conn order by metis + +text\Strong/axiom-like variants imply weak/rule-like ones as expected.\ +lemma "lCoP0(\<^bold>\) \ \ CoP0 \" unfolding neg cond conn order by blast +lemma "lCoP1(\<^bold>\) \ \ CoP1 \" unfolding neg conn order by blast +lemma "lCoP2(\<^bold>\) \ \ CoP2 \" unfolding neg conn order by blast +lemma "lCoP3(\<^bold>\) \ \ CoP3 \" unfolding neg conn order by blast + +text\Explore some (non)entailment relations.\ +lemma lCoP1_TND: "lCoP1(\<^bold>\) \ \ TND \" unfolding neg conn by (smt (verit, best) setequ_char subset_def) +lemma "TND \ \ lCoP1(\<^bold>\) \" nitpick oops \\ counterexample \ +lemma lCoP2_ECQ: "lCoP2(\<^bold>\) \ \ ECQ \" unfolding neg conn by (smt (verit) setequ_def subset_def) +lemma "ECQ \ \ lCoP2(\<^bold>\) \" nitpick oops \\ counterexample \ + + +subsubsection \Local modus tollens axioms\ + +text\lMT: (local) Modus tollens (strong, 'axiom-like' variants, using local consequence).\ +abbreviation plMT0 ("lMT0\<^sup>_\<^sup>_ _ _") where "lMT0\<^sup>a\<^sup>b \ \ \ [\ a b, \ b \ \ a]" +abbreviation plMT1 ("lMT1\<^sup>_\<^sup>_ _ _") where "lMT1\<^sup>a\<^sup>b \ \ \ [\ a (\ b), b \ \ a]" +abbreviation plMT2 ("lMT2\<^sup>_\<^sup>_ _ _") where "lMT2\<^sup>a\<^sup>b \ \ \ [\ (\ a) b, \ b \ a]" +abbreviation plMT3 ("lMT3\<^sup>_\<^sup>_ _ _") where "lMT3\<^sup>a\<^sup>b \ \ \ [\ (\ a) (\ b), b \ a]" +definition lMT0::"('w \\'w \\'w \) \ 'w \" where "lMT0 \ \ \ \a b. lMT0\<^sup>a\<^sup>b \ \" +definition lMT1::"('w \\'w \\'w \) \ 'w \" where "lMT1 \ \ \ \a b. lMT1\<^sup>a\<^sup>b \ \" +definition lMT2::"('w \\'w \\'w \) \ 'w \" where "lMT2 \ \ \ \a b. lMT2\<^sup>a\<^sup>b \ \" +definition lMT3::"('w \\'w \\'w \) \ 'w \" where "lMT3 \ \ \ \a b. lMT3\<^sup>a\<^sup>b \ \" + +declare lMT0_def[neg] lMT1_def[neg] lMT2_def[neg] lMT3_def[neg] + +text\All these MT variants are in general independent from each other and also from (strong) CoP instances. +However if we take classical implication we can verify that local MT and CoP are indeed equivalent.\ +lemma "lMT0(\<^bold>\) \ = lCoP0(\<^bold>\) \" unfolding neg conn order by blast +lemma "lMT1(\<^bold>\) \ = lCoP1(\<^bold>\) \" unfolding neg conn order by blast +lemma "lMT2(\<^bold>\) \ = lCoP2(\<^bold>\) \" unfolding neg conn order by blast +lemma "lMT3(\<^bold>\) \ = lCoP3(\<^bold>\) \" unfolding neg conn order by blast + + +subsubsection \Disjunctive syllogism\ + +text\DS: disjunctive syllogism.\ +abbreviation pDS1 ("DS1\<^sup>_\<^sup>_ _ _") where "DS1\<^sup>a\<^sup>b \ \ \ [a \<^bold>\ b \ \ (\ a) b]" +abbreviation pDS2 ("DS2\<^sup>_\<^sup>_ _ _") where "DS2\<^sup>a\<^sup>b \ \ \ [\ (\ a) b \ a \<^bold>\ b]" +abbreviation pDS3 ("DS3\<^sup>_\<^sup>_ _ _") where "DS3\<^sup>a\<^sup>b \ \ \ [\ a \<^bold>\ b \ \ a b]" +abbreviation pDS4 ("DS4\<^sup>_\<^sup>_ _ _") where "DS4\<^sup>a\<^sup>b \ \ \ [\ a b \ \ a \<^bold>\ b]" +definition DS1::"('w \\'w \\'w \) \ 'w \" where "DS1 \ \ \ \a b. DS1\<^sup>a\<^sup>b \ \" +definition DS2::"('w \\'w \\'w \) \ 'w \" where "DS2 \ \ \ \a b. DS2\<^sup>a\<^sup>b \ \" +definition DS3::"('w \\'w \\'w \) \ 'w \" where "DS3 \ \ \ \a b. DS3\<^sup>a\<^sup>b \ \" +definition DS4::"('w \\'w \\'w \) \ 'w \" where "DS4 \ \ \ \a b. DS4\<^sup>a\<^sup>b \ \" + +declare DS1_def[neg] DS2_def[neg] DS3_def[neg] DS4_def[neg] + +text\All DS variants are in general independent from each other. However if we take classical implication +we can verify that the pairs DS1-DS3 and DS2-DS4 are indeed equivalent. \ +lemma "DS1(\<^bold>\) \ = DS3(\<^bold>\) \" unfolding neg conn order by blast +lemma "DS2(\<^bold>\) \ = DS4(\<^bold>\) \" unfolding neg conn order by blast + +text\Explore some (non)entailment relations.\ +lemma DS1_nDNor: "DS1(\<^bold>\) \ \ nDNRM \" unfolding neg cond conn order by metis +lemma DS2_nNor: "DS2(\<^bold>\) \ \ nNORM \" unfolding neg cond conn order by metis +lemma lCoP2_DS1: "lCoP2(\<^bold>\) \ \ DS1(\<^bold>\) \" unfolding neg conn order by blast +lemma lCoP1_DS2: "lCoP1(\<^bold>\) \ \ DS2(\<^bold>\) \" unfolding neg conn order by blast +lemma "CoP2 \ \ DS1(\<^bold>\) \" nitpick oops \\ counterexample \ +lemma "CoP1 \ \ DS2(\<^bold>\) \" nitpick oops \\ counterexample \ + +end diff --git a/thys/Topological_Semantics/logics_operators.thy b/thys/Topological_Semantics/logics_operators.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/logics_operators.thy @@ -0,0 +1,77 @@ +theory logics_operators + imports conditions_positive +begin + +subsection \Converting between topological operators\ + +text\We verify minimal conditions under which operators resulting from conversion functions coincide.\ + +text\Conversions between interior, closure and exterior are straightforward and hold without restrictions: + Interior and closure are each other duals. Exterior is the complement of closure. + We focus here on conversions involving the border and frontier operators.\ + +text\Interior operator as derived from border.\ +definition Int_br::"('w \\'w \)\('w \\'w \)" ("\\<^sub>B") + where "\\<^sub>B \ \ \A. A \<^bold>\ (\ A)" +text\Interior operator as derived from frontier.\ +definition Int_fr::"('w \\'w \)\('w \\'w \)" ("\\<^sub>F") + where "\\<^sub>F \ \ \A. A \<^bold>\ (\ A)" +text\Closure operator as derived from border.\ +definition Cl_br::"('w \\'w \)\('w \\'w \)" ("\\<^sub>B") + where "\\<^sub>B \ \ \A. A \<^bold>\ \(\<^bold>\A)" +text\Closure operator as derived from frontier.\ +definition Cl_fr::"('w \\'w \)\('w \\'w \)" ("\\<^sub>F") + where "\\<^sub>F \ \ \A. A \<^bold>\ (\ A)" +text\Frontier operator as derived from interior.\ +definition Fr_int::"('w \\'w \)\('w \\'w \)" ("\\<^sub>I") + where "\\<^sub>I \ \ \A. \<^bold>\(\ A \<^bold>\ \(\<^bold>\A))" +text\Frontier operator as derived from closure.\ +definition Fr_cl::"('w \\'w \)\('w \\'w \)" ("\\<^sub>C") + where "\\<^sub>C \ \ \A. (\ A) \<^bold>\ \(\<^bold>\A)" +text\Frontier operator as derived from border.\ +definition Fr_br::"('w \\'w \)\('w \\'w \)" ("\\<^sub>B") + where "\\<^sub>B \ \ \A. \ A \<^bold>\ \(\<^bold>\A)" +text\Border operator as derived from interior.\ +definition Br_int::"('w \\'w \)\('w \\'w \)" ("\\<^sub>I") + where "\\<^sub>I \ \ \A. A \<^bold>\ (\ A)" +text\Border operator as derived from closure.\ +definition Br_cl::"('w \\'w \)\('w \\'w \)" ("\\<^sub>C") + where "\\<^sub>C \ \ \A. A \<^bold>\ \(\<^bold>\A)" +text\Border operator as derived from frontier.\ +definition Br_fr::"('w \\'w \)\('w \\'w \)" ("\\<^sub>F") + where "\\<^sub>F \ \ \A. A \<^bold>\ (\ A)" + +text\Inter-definitions involving border or frontier do not hold without restrictions.\ +lemma "\ = \\<^sub>C (\\<^sub>B \)" nitpick oops \\ countermodel \ +lemma "\ = \\<^sub>I (\\<^sub>B \)" nitpick oops \\ countermodel \ +lemma "\ = \\<^sub>F (\\<^sub>B \)" nitpick oops \\ countermodel \ +lemma "\ = \\<^sub>C (\\<^sub>F \)" nitpick oops \\ countermodel \ +lemma "\ = \\<^sub>I (\\<^sub>F \)" nitpick oops \\ countermodel \ +lemma "\ = \\<^sub>B (\\<^sub>F \)" nitpick oops \\ countermodel \ + +lemma "\ = \\<^sub>B (\\<^sub>C \)" nitpick oops \\ countermodel \ +lemma "\ = \\<^sub>F (\\<^sub>C \)" nitpick oops \\ countermodel \ +lemma "\ = \\<^sub>B (\\<^sub>C \)" nitpick oops \\ countermodel \ +lemma "\ = \\<^sub>F (\\<^sub>C \)" nitpick oops \\ countermodel \ + + +text\Inter-definitions involving border or frontier always assume the second Kuratowski condition + (or its respective counterpart: C2, I2, B2 or F2).\ +abbreviation "C2 \ \ EXPN \" +abbreviation "I2 \ \ CNTR \" +abbreviation "B2 \ \ CNTR \" +abbreviation "F2 \ \ \A. \(\<^bold>\A) \<^bold>= \ A" + +lemma "B2 \ \ \ = \\<^sub>C (\\<^sub>B \)" unfolding CNTR_def Br_cl_def Cl_br_def conn order by metis +lemma "B2 \ \ \ = \\<^sub>I (\\<^sub>B \)" unfolding CNTR_def Br_int_def Int_br_def conn order by metis +lemma "B2 \ \ \ = \\<^sub>F (\\<^sub>B \)" unfolding CNTR_def Br_fr_def Fr_br_def conn order by metis +lemma "F2 \ \ \ = \\<^sub>C (\\<^sub>F \)" unfolding Cl_fr_def Fr_cl_def conn order by metis +lemma "F2 \ \ \ = \\<^sub>I (\\<^sub>F \)" unfolding Int_fr_def Fr_int_def conn order by metis +lemma "F2 \ \ \ = \\<^sub>B (\\<^sub>F \)" unfolding Br_fr_def Fr_br_def conn order by metis + +lemma "C2 \ \ \ = \\<^sub>B (\\<^sub>C \)" unfolding EXPN_def Br_cl_def Cl_br_def conn order by metis +lemma "C2 \ \ \ = \\<^sub>F (\\<^sub>C \)" unfolding EXPN_def Fr_cl_def Cl_fr_def conn order by metis +lemma "I2 \ \ \ = \\<^sub>B (\\<^sub>I \)" unfolding CNTR_def Int_br_def Br_int_def conn order by metis +lemma "I2 \ \ \ = \\<^sub>F (\\<^sub>I \)" unfolding CNTR_def Int_fr_def Fr_int_def conn order by metis + +end diff --git a/thys/Topological_Semantics/logics_quantifiers.thy b/thys/Topological_Semantics/logics_quantifiers.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/logics_quantifiers.thy @@ -0,0 +1,99 @@ +theory logics_quantifiers + imports boolean_algebra_infinitary +begin + +subsection \Quantifiers (restricted and unrestricted)\ + +text\Introduce pedagogically convenient notation.\ +notation HOL.All ("\") notation HOL.Ex ("\") + +text\Let us recall that in HOL we have: \ +lemma "(\x. P) = \(\x. P)" by simp +lemma "(\x. P) = \(\x. P)" by simp +lemma "\ = (\P. \\(\x. \P x))" by simp + +text\We can introduce their respective 'w-type-lifted variants as follows: \ +definition mforall::"('i\'w \)\'w \" ("\<^bold>\_") + where "\<^bold>\\ \ \w. \X. \ X w" +definition mexists::"('i\'w \)\'w \" ("\<^bold>\_") + where "\<^bold>\\ \ \w. \X. \ X w" + +text\To improve readability, we introduce for them standard binder notation.\ +notation mforall (binder "\<^bold>\" [48]49) notation mexists (binder "\<^bold>\" [48]49) + +text\And thus we obtain the 'w-type-lifted variant of the standard (variable-binding) quantifiers.\ +lemma "(\<^bold>\X. \) = \<^bold>\(\X. \)" by (simp add: mforall_def) +lemma "(\<^bold>\X. \) = \<^bold>\(\X. \)" by (simp add: mexists_def) + +text\Quantifiers are dual to each other in the expected way.\ +lemma "\<^bold>\\ = \<^bold>\(\<^bold>\\\<^sup>-)" by (simp add: compl_def mexists_def mforall_def svfun_compl_def) +lemma "(\<^bold>\X. \ X) = \<^bold>\(\<^bold>\X. \<^bold>\(\ X))" by (simp add: compl_def mexists_def mforall_def) + +text\Relationship between quantifiers and the infinitary supremum and infimum operations.\ +lemma mforall_char: "\<^bold>\\ = \<^bold>\\\ _\" unfolding infimum_def mforall_def range_def by metis +lemma mexists_char: "\<^bold>\\ = \<^bold>\\\ _\" unfolding supremum_def mexists_def range_def by metis +(*Using binder notation:*) +lemma mforallb_char: "(\<^bold>\X. \) = \<^bold>\\(\X. \) _\" unfolding infimum_def mforall_def range_def by simp +lemma mexistsb_char: "(\<^bold>\X. \) = \<^bold>\\(\X. \) _\" unfolding supremum_def mexists_def range_def by simp + + +text\We now consider quantification restricted over constant and varying domains.\ + +text\Constant domains: first generalization of quantifiers above (e.g. free logic).\ +definition mforall_const::"'i \ \ ('i \ 'w \) \ 'w \" ("\<^bold>\[_]_") + where "\<^bold>\[D]\ \ \w. \X. (D X) \ (\ X) w" +definition mexists_const::"'i \ \ ('i \ 'w \) \ 'w \" ("\<^bold>\[_]_") + where "\<^bold>\[D]\ \ \w. \X. (D X) \ (\ X) w" + +(*Alas! the convenient binder notation cannot be easily introduced for restricted quantifiers.*) + +text\Constant-domain quantification generalises its unrestricted counterpart.\ +lemma "\<^bold>\\ = \<^bold>\[\<^bold>\]\" by (simp add: mforall_const_def mforall_def top_def) +lemma "\<^bold>\\ = \<^bold>\[\<^bold>\]\" by (simp add: mexists_const_def mexists_def top_def) + +text\Constant-domain quantification can also be characterised using infimum and supremum.\ +lemma mforall_const_char: "\<^bold>\[D]\ = \<^bold>\\\ D\" unfolding image_def infimum_def mforall_const_def by metis +lemma mexists_const_char: "\<^bold>\[D]\ = \<^bold>\\\ D\" unfolding image_def supremum_def mexists_const_def by metis + +text\Constant-domain quantifiers also allow us to nicely characterize the interaction between + function composition and (restricted) quantification:\ +lemma mforall_comp: "\<^bold>\(\\\) = \<^bold>\[\\ _\] \" unfolding fun_comp_def mforall_const_def mforall_def range_def by metis +lemma mexists_comp: "\<^bold>\(\\\) = \<^bold>\[\\ _\] \" unfolding fun_comp_def mexists_const_def mexists_def range_def by metis + + +text\Varying domains: we can also restrict quantifiers by taking a 'functional domain' as additional parameter. +The latter is a set-valued mapping each element 'i to a set of points (e.g. where it 'exists').\ +definition mforall_var::"('i \ 'w \) \ ('i \ 'w \) \ 'w \" ("\<^bold>\{_}_") + where "\<^bold>\{\}\ \ \w. \X. (\ X) w \ (\ X) w" +definition mexists_var::"('i \ 'w \) \ ('i \ 'w \) \ 'w \" ("\<^bold>\{_}_") + where "\<^bold>\{\}\ \ \w. \X. (\ X) w \ (\ X) w" + +text\Varying-domain quantification generalizes its constant-domain counterpart.\ +lemma "\<^bold>\[D]\ = \<^bold>\{D\}\" by (simp add: mforall_const_def mforall_var_def) +lemma "\<^bold>\[D]\ = \<^bold>\{D\}\" by (simp add: mexists_const_def mexists_var_def) + +text\Restricted quantifiers are dual to each other in the expected way.\ +lemma "\<^bold>\[D]\ = \<^bold>\(\<^bold>\[D]\\<^sup>-)" by (metis iDM_b im_prop2 mexists_const_char mforall_const_char setequ_ext) +lemma "\<^bold>\{\}\ = \<^bold>\(\<^bold>\{\}\\<^sup>-)" by (simp add: compl_def mexists_var_def mforall_var_def svfun_compl_def) + +text\We can use 2nd-order connectives on set-valued functions to encode restricted quantifiers as unrestricted.\ +lemma "\<^bold>\{\}\ = \<^bold>\(\ \<^bold>\\<^sup>: \)" by (simp add: impl_def mforall_def mforall_var_def svfun_impl_def) +lemma "\<^bold>\{\}\ = \<^bold>\(\ \<^bold>\\<^sup>: \)" by (simp add: meet_def mexists_def mexists_var_def svfun_meet_def) + +text\Observe that using these operators has the advantage of allowing for binder notation.\ +lemma "\<^bold>\{\}\ = (\<^bold>\X. (\ \<^bold>\\<^sup>: \) X)" by (simp add: impl_def mforall_def mforall_var_def svfun_impl_def) +lemma "\<^bold>\{\}\ = (\<^bold>\X. (\ \<^bold>\\<^sup>: \) X)" by (simp add: meet_def mexists_def mexists_var_def svfun_meet_def) + +text\To sumarize: different sorts of restricted quantification can be emulated + by employing 2nd-order operations to adequately relativize predicates.\ +lemma "\<^bold>\[D]\ = (\<^bold>\X. (D\ \<^bold>\\<^sup>: \) X)" by (simp add: impl_def mforall_const_def mforall_def svfun_impl_def) +lemma "\<^bold>\{\<^bold>\\<^sup>:}\ = (\<^bold>\X. (\<^bold>\\<^sup>: \<^bold>\\<^sup>: \) X)" by (simp add: impl_def mforall_def mforall_var_def svfun_impl_def) +lemma "\<^bold>\\ = \<^bold>\{\<^bold>\\<^sup>:}\" by (simp add: mforall_def mforall_var_def svfun_top_def top_def) +lemma "(\<^bold>\X. \ X) = \<^bold>\{\<^bold>\\<^sup>:}\" by (simp add: mforall_def mforall_var_def svfun_top_def top_def) + +named_theorems quant (*to group together definitions related to quantification*) +declare mforall_def[quant] mexists_def[quant] + mforall_const_def[quant] mexists_const_def[quant] + mforall_var_def[quant] mexists_var_def[quant] + +end diff --git a/thys/Topological_Semantics/logics_quantifiers_example.thy b/thys/Topological_Semantics/logics_quantifiers_example.thy new file mode 100644 --- /dev/null +++ b/thys/Topological_Semantics/logics_quantifiers_example.thy @@ -0,0 +1,64 @@ +theory logics_quantifiers_example + imports logics_quantifiers conditions_positive_infinitary +begin + +subsection \Examples on Quantifiers\ + +text\First-order quantification example.\ +lemma "(\x. A x \ (\y. B x y)) \ (\x. \y. A x \ B x y)" by simp +lemma "(\<^bold>\x. A x \<^bold>\ (\<^bold>\y. B x y)) \<^bold>= (\<^bold>\x. \<^bold>\y. A x \<^bold>\ B x y)" by (simp add: impl_def mexists_def setequ_def) + +text\Propositional quantification example.\ +lemma "\A. (\B. (A \ \B))" by blast +lemma "(\<^bold>\A. (\<^bold>\B. A \<^bold>\ \<^bold>\B)) \<^bold>= \<^bold>\" unfolding mforall_def mexists_def by (smt (verit) compl_def dimpl_def setequ_def top_def) + +text\Drinker's principle.\ +lemma "\<^bold>\x. Drunk x \<^bold>\ (\<^bold>\y. Drunk y) \<^bold>= \<^bold>\" + by (simp add: impl_def mexists_def mforall_def setequ_def top_def) + +text\Example in non-classical logics.\ +typedecl w +type_synonym \ = "(w \)" + +consts \::"\ \ \" +abbreviation "\ \ \\<^sup>d" +abbreviation "CLOSURE \ \ ADDI \ \ EXPN \ \ NORM \ \ IDEM \" +abbreviation "INTERIOR \ \ MULT \ \ CNTR \ \ DNRM \ \ IDEM \" + +definition mforallInt::"(\ \ \) \ \" ("\<^bold>\\<^sup>I_") + where "\<^bold>\\<^sup>I\ \ \<^bold>\[fp \]\" +definition mexistsInt::"(\ \ \) \ \" ("\<^bold>\\<^sup>I_") + where "\<^bold>\\<^sup>I\ \ \<^bold>\[fp \]\" + +(*To improve readability, we introduce for them standard binder notation.*) +notation mforallInt (binder "\<^bold>\\<^sup>I" [48]49) +notation mexistsInt (binder "\<^bold>\\<^sup>I" [48]49) + +abbreviation intneg ("\<^bold>\\<^sup>I_") where "\<^bold>\\<^sup>IA \ \\<^sup>d\<^sup>- A" +abbreviation parneg ("\<^bold>\\<^sup>C_") where "\<^bold>\\<^sup>CA \ \\<^sup>d\<^sup>- A" + +lemma "(\<^bold>\X. (\<^bold>\B. (X \<^bold>\ \<^bold>\B))) \<^bold>= \<^bold>\" by (smt (verit, del_insts) compl_def dimpl_def mexists_def mforall_def setequ_def top_def) +lemma "(\<^bold>\\<^sup>IX. (\<^bold>\\<^sup>IB. (X \<^bold>\ \<^bold>\\<^sup>IB))) \<^bold>= \<^bold>\" nitpick oops \\ counterexample \ + + +subsection \Barcan formula and its converse\ + +text\The converse Barcan formula follows readily from monotonicity.\ +lemma CBarcan1: "MONO \ \ \\. \(\<^bold>\x. \ x) \<^bold>\ (\<^bold>\x. \(\ x))" by (smt (verit, ccfv_SIG) MONO_def mforall_def subset_def) +lemma CBarcan2: "MONO \ \ \\. (\<^bold>\x. \(\ x)) \<^bold>\ \(\<^bold>\x. \ x)" by (smt (verit) MONO_def mexists_def subset_def) + +text\However, the Barcan formula requires a stronger assumption (of an infinitary character).\ +lemma Barcan1: "iMULT\<^sup>b \ \ \\. (\<^bold>\x. \(\ x)) \<^bold>\ \(\<^bold>\x. \ x)" unfolding iMULT_b_def by (smt (verit) infimum_def mforall_char image_def range_char1 subset_def) +lemma Barcan2: "iADDI\<^sup>a \ \ \\. \(\<^bold>\x. \ x) \<^bold>\ (\<^bold>\x. \(\ x))" unfolding iADDI_a_def by (smt (verit, ccfv_threshold) mexists_char image_def range_char1 subset_def supremum_def) + +text\Converse Barcan Formula and composition.\ +lemma "MONO \ \ \\. \(\<^bold>\ \) \<^bold>\ \<^bold>\(\ \ \)" by (metis MONO_iMULTa iMULT_a_def mforall_char mforall_comp mforall_const_char) +lemma "MONO \ \ \\. \(\<^bold>\[D] \) \<^bold>\ \<^bold>\[D](\ \ \)" by (smt (verit) MONO_iMULTa fun_comp_def iMULT_a_def mforall_const_char mforall_const_def image_def subset_def) +lemma "CNTR \ \ iMULT \ \ IDEM \ \ \\. \(\<^bold>\{\} \) \<^bold>\ \<^bold>\{\}(\ \ \)" nitpick oops \\ counterexample \ + +text\Barcan Formula and composition.\ +lemma "iMULT\<^sup>b \ \ \\. \<^bold>\(\ \ \) \<^bold>\ \(\<^bold>\ \)" by (metis iMULT_b_def mforall_char mforall_comp mforall_const_char) +lemma "iMULT\<^sup>b \ \ \\. \<^bold>\[D](\ \ \) \<^bold>\ \(\<^bold>\[D] \)" by (smt (verit) fun_comp_def iMULT_b_def infimum_def mforall_const_char image_def subset_def) +lemma "iADDI \ \ iMULT \ \ \\. \<^bold>\{\}(\ \ \) \<^bold>\ \(\<^bold>\{\} \)" nitpick oops \\ counterexample \ + +end