Theory sse_boolean_algebra

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›

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
`