Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Partially implements a natural deduction system in Haskell
{-# LANGUAGE TypeOperators #-}
module NaturalDeduction where
data () -- no inhabitants
type (¬)p = p -> ()
type () = (,)
type () = Either
type () = (->)
modusTollens :: (p q) (¬)q (¬)p
modusTollens (φ, ψ) = ψ . φ
true :: truth
true = true
exclMid :: p (¬)p
exclMid = true
type p q = (p q) (q p)
dblNeg :: p (¬)((¬) p)
dblNeg = (flip ($), true)
transposition :: (p q) ((¬)q (¬)p)
transposition =
(curry modusTollens, \c p -> -- c = contrapositive
undoDblNegate $ curry modusTollens c $ dblNegate p)
where (dblNegate, undoDblNegate) = dblNeg
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment