theory sse_boolean_algebra imports Main begin declare[[syntax_ambiguity_warning=false]] nitpick_params[assms=true, user_axioms=true, show_all, expect=genuine, format=3] (*default Nitpick settings*) section ‹Shallow embedding of a Boolean algebra of propositions› text‹\noindent{In this section we present a shallow semantical embedding (SSE, cf. @{cite J41} and @{cite J23}) for a family of logics whose semantics is based upon extensions of (complete and atomic) Boolean algebras. The range of such logics is indeed very wide, including, as we will see, quantified paraconsistent and paracomplete (e.g. intuitionistic) logics. Aside from illustrating how the SSE approach works in practice we show how it allows us to effectively harness theorem provers, model finders and `hammers' for reasoning with quantified non-classical logics. Proof reconstructions have deliberately been avoided. Most of the proofs (in fact, all one-liners) have been found using Sledgehammer.}› text‹\noindent{Two notions play a fundamental role in this work: propositions and propositional functions. Propositions, qua sentence denotations, are modeled as objects of type @{text "w⇒bool"} (shortened as @{text "σ"}). Propositional functions, as the name indicates, are basically anything with a (parametric) type @{text "'t⇒σ"}.}› text‹\noindent{We introduce a type @{text "w"} for the domain of points (aka. 'worlds', 'states', etc.). @{text "σ"} is a type alias for sets of points (i.e. propositions) encoded as characteristic functions.}› typedecl w type_synonym σ = "w⇒bool" text‹\noindent{In the sequel, we introduce the following naming convention for variables: (i) Latin letters (A, b, M, P, q, X, y, etc.) denote in general propositions (type @{text "σ"}); however, we reserve letters D and S to denote sets of propositions (aka. domains/spaces) and the letters u, v and w to denote worlds/points. (ii) Greek letters (in particular @{text "π"}) denote propositional functions (type @{text "'t⇒σ"}); among the latter we may employ the letters @{text "φ"}, @{text "ψ"} and @{text "η"} to explicitly name those corresponding to unary connectives/operations (type @{text "σ⇒σ"}).}› subsection ‹Encoding Boolean operations› text‹\noindent{We start with an ordered algebra,}› abbreviation sequ::"σ⇒σ⇒bool" (infixr "❙≈" 45) where "A ❙≈B ≡ ∀w. (A w) ⟷ (B w)" abbreviation subs::"σ⇒σ⇒bool" (infixr "❙≼" 45) where "A ❙≼B ≡ ∀w. (A w) ⟶ (B w)" abbreviation sups::"σ⇒σ⇒bool" (infixr "❙≽" 45) where "B ❙≽A ≡ A ❙≼B" text‹\noindent{define meet and join by reusing HOL metalogical conjunction and disjunction,}› definition meet::"σ⇒σ⇒σ" (infixr "❙∧" 54) where "A ❙∧B ≡ λw. (A w) ∧ (B w)" definition join::"σ⇒σ⇒σ" (infixr "❙∨" 53) where "A ❙∨B ≡ λw. (A w) ∨ (B w)" text‹\noindent{and introduce further operations to obtain a Boolean 'algebra of propositions'.}› definition top::"σ" ("❙⊤") where "❙⊤≡ λw. True" definition bottom::"σ" ("❙⊥") where "❙⊥≡ λw. False" definition impl::"σ⇒σ⇒σ" (infixr "❙→" 51) where "A ❙→B ≡ λw. (A w)⟶(B w)" definition dimp::"σ⇒σ⇒σ" (infixr "❙↔" 51) where "A ❙↔B ≡ λw. (A w)⟷(B w)" definition diff::"σ⇒σ⇒σ" (infixr "❙↼" 51) where "A ❙↼B ≡ λw. (A w) ∧ ¬(B w)" definition compl::"σ⇒σ" ("❙─_" [57]58) where "❙─A ≡ λw. ¬(A w)" named_theorems conn (*algebraic connectives*) declare meet_def[conn] join_def[conn] top_def[conn] bottom_def[conn] impl_def[conn] dimp_def[conn] diff_def[conn] compl_def[conn] text‹\noindent{Quite trivially, we can verify that the algebra satisfies some essential lattice properties.}› lemma "a ❙∨a ❙≈a" unfolding conn by simp lemma "a ❙∧a ❙≈a" unfolding conn by simp lemma "a ❙≼a ❙∨b" unfolding conn by simp lemma "a ❙∧b ❙≼a" unfolding conn by simp lemma "(a ❙∧b) ❙∨b ❙≈b" unfolding conn by auto (*absorption 1*) lemma "a ❙∧(a ❙∨b) ❙≈a" unfolding conn by auto (*absorption 2*) lemma "a ❙≼c ⟹ b ❙≼c ⟹ a ❙∨b ❙≼c" unfolding conn by simp lemma "c ❙≼a ⟹ c ❙≼b ⟹ c ❙≼a ❙∧b" unfolding conn by simp lemma "a ❙≼b ≡ (a ❙∨b) ❙≈b" unfolding conn by smt lemma "b ❙≼a ≡ (a ❙∧b) ❙≈b" unfolding conn by smt lemma "a ❙≼c ⟹ b ❙≼d ⟹ (a ❙∨b) ❙≼(c ❙∨d)" unfolding conn by simp lemma "a ❙≼c ⟹ b ❙≼d ⟹ (a ❙∧b) ❙≼(c ❙∧d)" unfolding conn by simp subsection ‹Second-order operations and fixed-points› text‹\noindent{We define equality for propositional functions as follows.}› definition equal_op::"('t⇒σ)⇒('t⇒σ)⇒bool" (infix "❙≡" 60) where "φ ❙≡ψ ≡ ∀X. φ X ❙≈ψ X" text‹\noindent{Moreover, we define some useful Boolean (2nd-order) operations on propositional functions,}› abbreviation unionOp::"('t⇒σ)⇒('t⇒σ)⇒('t⇒σ)" (infixr "❙⊔" 61) where "φ ❙⊔ψ ≡ λX. φ X ❙∨ψ X" abbreviation interOp::"('t⇒σ)⇒('t⇒σ)⇒('t⇒σ)" (infixr "❙⊓" 62) where "φ ❙⊓ψ ≡ λX. φ X ❙∧ψ X" abbreviation compOp::"('t⇒σ)⇒('t⇒σ)" ("(_⇧^{c})") where "φ⇧^{c}≡ λX. ❙─φ X" text‹\noindent{some of them explicitly targeting operations,}› definition dual::"(σ⇒σ)⇒(σ⇒σ)" ("(_⇧^{d})") where "φ⇧^{d}≡ λX. ❙─(φ(❙─X))" text‹\noindent{and also define an useful operation (for technical purposes).}› definition id::"σ⇒σ" ("id") where "id A ≡ A" text‹\noindent{We now prove some useful lemmas (some of them may help the provers in their hard work).}› lemma comp_symm: "φ⇧^{c}= ψ ⟹ φ = ψ⇧^{c}" unfolding conn by blast lemma comp_invol: "φ⇧^{c}⇧^{c}= φ" unfolding conn by blast lemma dual_symm: "(φ ≡ ψ⇧^{d}) ⟹ (ψ ≡ φ⇧^{d})" unfolding dual_def conn by simp lemma dual_comp: "φ⇧^{d}⇧^{c}= φ⇧^{c}⇧^{d}" unfolding dual_def by simp lemma "id⇧^{d}❙≡id" by (simp add: id_def dual_def equal_op_def conn) lemma "id⇧^{c}❙≡compl" by (simp add: id_def dual_def equal_op_def conn) lemma "(A ❙⊔B)⇧^{d}❙≡(A⇧^{d}) ❙⊓(B⇧^{d})" by (simp add: dual_def equal_op_def conn) lemma "(A ❙⊔B)⇧^{c}❙≡(A⇧^{c}) ❙⊓(B⇧^{c})" by (simp add: equal_op_def conn) lemma "(A ❙⊓B)⇧^{d}❙≡(A⇧^{d}) ❙⊔(B⇧^{d})" by (simp add: dual_def equal_op_def conn) lemma "(A ❙⊓B)⇧^{c}❙≡(A⇧^{c}) ❙⊔(B⇧^{c})" by (simp add: equal_op_def conn) text‹\noindent{The notion of a fixed point is a fundamental one. We speak of propositions being fixed points of operations. For a given operation we define in the usual way a fixed-point predicate for propositions.}› abbreviation fixedpoint::"(σ⇒σ)⇒(σ⇒bool)" ("fp") where "fp φ ≡ λX. φ X ❙≈X" lemma fp_d: "(fp φ⇧^{d}) X = (fp φ)(❙─X)" unfolding dual_def conn by auto lemma fp_c: "(fp φ⇧^{c}) X = (X ❙≈❙─(φ X))" unfolding conn by auto lemma fp_dc:"(fp φ⇧^{d}⇧^{c}) X = (X ❙≈φ(❙─X))" unfolding dual_def conn by auto text‹\noindent{Indeed, we can 'operationalize' this predicate by defining a fixed-point operator as follows:}› abbreviation fixedpoint_op::"(σ⇒σ)⇒(σ⇒σ)" ("(_⇧^{f}⇧^{p})") where "φ⇧^{f}⇧^{p}≡ λX. (φ X) ❙↔X" lemma ofp_c: "(φ⇧^{c})⇧^{f}⇧^{p}❙≡(φ⇧^{f}⇧^{p})⇧^{c}" unfolding conn equal_op_def by auto lemma ofp_d: "(φ⇧^{d})⇧^{f}⇧^{p}❙≡(φ⇧^{f}⇧^{p})⇧^{d}⇧^{c}" unfolding dual_def equal_op_def conn by auto lemma ofp_dc:"(φ⇧^{d}⇧^{c})⇧^{f}⇧^{p}❙≡(φ⇧^{f}⇧^{p})⇧^{d}" unfolding dual_def equal_op_def conn by auto lemma ofp_decomp: "φ⇧^{f}⇧^{p}❙≡(id ❙⊓φ) ❙⊔((id ❙⊔φ)⇧^{c})" unfolding equal_op_def id_def conn by auto lemma ofp_invol: "(φ⇧^{f}⇧^{p})⇧^{f}⇧^{p}❙≡φ" unfolding conn equal_op_def by auto text‹\noindent{Fixed-point predicate and fixed-point operator are closely related.}› lemma fp_rel: "((fp φ) X) = (φ⇧^{f}⇧^{p}X ❙≈❙⊤)" unfolding conn by auto lemma fp_d_rel: "((fp φ⇧^{d}) X) = (φ⇧^{f}⇧^{p}(❙─X) ❙≈❙⊤)" unfolding dual_def conn by auto lemma fp_c_rel: "((fp φ⇧^{c}) X) = (φ⇧^{f}⇧^{p}X ❙≈❙⊥)" unfolding conn by auto lemma fp_dc_rel: "((fp φ⇧^{d}⇧^{c}) X) = (φ⇧^{f}⇧^{p}(❙─X) ❙≈❙⊥)" unfolding dual_def conn by auto subsection ‹Equality and atomicity› text‹\noindent{We prove some facts about equality (which may help improve prover's performance).}› lemma eq_ext: "a ❙≈b ⟹ a = b" using ext by blast lemma eq_ext': "a ❙≡b ⟹ a = b" using ext unfolding equal_op_def by blast lemma meet_char: "a ❙≼b ⟷ a ❙∧b ❙≈a" unfolding conn by blast lemma join_char: "a ❙≼b ⟷ a ❙∨b ❙≈b" unfolding conn by blast text‹\noindent{We can verify indeed that the algebra is atomic (in three different ways) by relying on the presence of primitive equality in HOL. A more general class of Boolean algebras could in principle be obtained in systems without primitive equality or by suitably restricting quantification over propositions (e.g. defining a topology and restricting quantifiers to open/closed sets).}› definition "atom a ≡ ¬(a ❙≈❙⊥) ∧ (∀p. a ❙≼p ∨ a ❙≼❙─p)" lemma atomic1: "∀w. ∃q. q w ∧ (∀p. p w ⟶ q ❙≼p)" using the_sym_eq_trivial by (metis (full_types)) lemma atomic2: "∀w. ∃q. q w ∧ atom(q)" using the_sym_eq_trivial by (metis (full_types) atom_def compl_def bottom_def) lemma atomic3: "∀p. ¬(p ❙≈❙⊥) ⟶ (∃q. atom(q) ∧ q ❙≼p)" proof - (*using atom_def unfolding conn by fastforce*) { fix p { assume "¬(p ❙≈❙⊥)" hence "∃v. p v" unfolding conn 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 by simp have "∀v. ?q v ⟶ p v" using 1 by simp hence 3: "?q ❙≼p" by simp from 2 3 have "∃q. atom(q) ∧ q ❙≼p" by blast } hence "¬(p ❙≈❙⊥) ⟶ (∃q. atom(q) ∧ q ❙≼p)" by (rule impI) } thus ?thesis by (rule allI) qed end