Add axioms of intuitionistic logic to Heyting algebras

src/SubHask/Algebra.hs

@@ -54,6 +54,15 @@ module SubHask.Algebra
     , law_Heyting_infleft
     , law_Heyting_infright
     , law_Heyting_distributive
+    , theorem_Heyting_then1
+    , theorem_Heyting_then2
+    , theorem_Heyting_and1
+    , theorem_Heyting_and2
+    , theorem_Heyting_and3
+    , theorem_Heyting_or1
+    , theorem_Heyting_or2
+    , theorem_Heyting_or3
+    , theorem_Heyting_false
     , Boolean
     , law_Boolean_infcomplement
     , law_Boolean_supcomplement
@@ -960,8 +969,48 @@ law_Heyting_infright b1 b2 = (b2 && (b1 ==> b2)) == b2
 law_Heyting_distributive :: (Eq b, Heyting b) => b -> b -> b -> Bool
 law_Heyting_distributive b1 b2 b3 = (b1 ==> (b2 && b3)) == ((b1 ==> b2) && (b1 ==> b3))
 
--- | FIXME: add the axioms for intuitionist logic, which are theorems based on these laws
+-- | Axioms for intuitionist logic
 --
+-- See <https://en.wikipedia.org/wiki/Intuitionistic_logic#Hilbert-style_calculus> for the axioms of intuitionist logic
+-- and <https://en.wikipedia.org/wiki/Heyting_algebra#Characterization_using_the_axioms_of_intuitionistic_logic> for a 
+-- characterization of Heyting algebras via the axioms. (Conditions 3-11 are the axioms.)
+
+-- a ==> (b ==> a)
+theorem_Heyting_then1 :: (Eq b, Heyting b) => b -> b -> Bool
+theorem_Heyting_then1 b1 b2 = (b1 ==> (b2 ==> b1)) == maxBound
+
+-- (a ==> ( b ==> c)) ==> ((a ==> b ) ==> (a ==> c))
+theorem_Heyting_then2 :: (Eq b, Heyting b) => b -> b -> b -> Bool
+theorem_Heyting_then2 b1 b2 b3 = ((b1 ==> (b2 ==> b3)) ==> ((b1 ==> b2) ==> (b1 ==> b3))) == maxBound
+
+-- (a && b) ==> a
+theorem_Heyting_and1 :: (Eq b, Heyting b) => b -> b -> Bool
+theorem_Heyting_and1 b1 b2 = ((b1 && b2) ==> b1) == maxBound
+
+-- (a && b) ==> b
+theorem_Heyting_and2 :: (Eq b, Heyting b) => b -> b -> Bool
+theorem_Heyting_and2 b1 b2 = ((b1 && b2) ==> b2) == maxBound
+
+-- a ==> (b ==> (a && b))
+theorem_Heyting_and3 :: (Eq b, Heyting b) => b -> b -> Bool
+theorem_Heyting_and3 b1 b2 = (b1 ==> (b2 ==> (b1 && b2))) == maxBound
+
+-- a ==> (a || b)
+theorem_Heyting_or1 :: (Eq b, Heyting b) => b -> b -> Bool
+theorem_Heyting_or1 b1 b2 = (b1 ==> (b1 || b2)) == maxBound
+
+-- b ==> (a || b)
+theorem_Heyting_or2 :: (Eq b, Heyting b) => b -> b-> Bool
+theorem_Heyting_or2 b1 b2 = (b2 ==> (b1 || b2)) == maxBound
+
+-- (a ==> c) ==> ((b ==> c) ==> (a || b ==> c))
+theorem_Heyting_or3 :: (Eq b, Heyting b) => b -> b -> b -> Bool
+theorem_Heyting_or3 b1 b2 b3 = ((b1 ==> b3) ==> ((b2 ==> b3) ==> (b1 || b2 ==> b3))) == maxBound
+
+-- bottomElement ==> a
+theorem_Heyting_false :: (Eq b, Heyting b) => b -> Bool
+theorem_Heyting_false b1 = (minBound ==> b1) == maxBound
+
 
 -- | Modus ponens gives us a default definition for "==>" in a "Boolean" algebra.
 -- This formula is guaranteed to not work in a "Heyting" algebra that is not "Boolean".

src/SubHask/TemplateHaskell/Test.hs

@@ -65,6 +65,15 @@ testMap = Map.fromList
         , "law_Heyting_infleft"
         , "law_Heyting_infright"
         , "law_Heyting_distributive"
+        , "theorem_Heyting_then1"
+        , "theorem_Heyting_then2"
+        , "theorem_Heyting_and1"
+        , "theorem_Heyting_and2"
+        , "theorem_Heyting_and3"
+        , "theorem_Heyting_or1"
+        , "theorem_Heyting_or2"
+        , "theorem_Heyting_or3"
+        , "theorem_Heyting_false"
         ] )
     , ("Boolean",
         [ "law_Boolean_infcomplement"