module Examples where
import FOL
import Text.Html
infixr -->
(-->) :: Formula -> Formula -> Formula
(-->) = Implies
examples :: [(String, Formula)]
examples = [ ("Law of excluded middle",
(p `Or` Not p)
)
, ("Contraposition",
((p-->q)-->(Not q --> Not p)))
, ("Contradiction",
p--> (Not p --> q)
)
, ("Pierce's law",
((p-->q) -->p)-->p
)
, ("Distributivity of ∧ over ∨",
(p`Or`(q`And`r)) --> ((p`Or`q)`And`(p`Or`r)))
-- , ("Distributivity of ∨ over ∧",
-- (p`And`(q`Or`r)) --> ((p`And`q)`Or`(p`And`q)))
, ("Distributivity of ∀ over ⇒",
Forall "X" (pp "X" --> qq "X") -->
(Forall "X" (pp "X") --> Forall "X" (qq "X"))
)
-- , ("Distributivity of ∀ over ∧",
-- (Forall "X" ((pp "X")`And`(qq "X"))) -->
-- (Forall "X" (pp "X") `And`
-- Forall "X" (qq "X"))
-- )
, ("Moving ∃ across ∀",
Exist "X" (Forall "Y" (Rel "p" [Var "X", Var "Y"])) -->
Forall "Y" (Exist "X" (Rel "p" [Var "X", Var "Y"]))
)
, ("An example of Skolemization",
(Forall "X" (Exist "Y" (Rel "p" [Var "X", Var "Y"])))
--> Exist "Y" (Rel "p" [Fun "a" [], Var "Y"])
)
]
where p = Rel "p" []
q = Rel "q" []
r = Rel "r" []
pp x = Rel "p" [Var x]
qq x = Rel "q" [Var x]