Copyright	(c) Isaac van Bakel 2020
License	BSD-3
Maintainer	ivb@vanbakel.io
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

Hout.Logic.Intuitionistic

Description

This module contains type aliases for intuitionistic logic constructions which are expressed as Haskell types.

It also gives the natural deduction rules for those aliases, except when they are aliases of arrow types. For example, implies-introduction and elimination are both Haskell arrow constructions (function abstraction and application, respectively) so no rule is given.

Synopsis

type True = ()
type False = Void
type (/\) a b = (a, b)
type (\/) a b = Either a b
type Not a = a -> False
type (<->) a b = (a -> b) /\ (b -> a)
andIntro :: a -> b -> a /\ b
andElimLeft :: (a /\ b) -> a
andElimRight :: (a /\ b) -> b
orIntroLeft :: a -> a \/ b
orIntroRight :: b -> a \/ b
orElim :: (a -> c) -> (b -> c) -> (a \/ b) -> c
trueIntro :: True
exFalso :: False -> a
iffIntro :: (a -> b) -> (b -> a) -> a <-> b
iffElimLeft :: (a <-> b) -> a -> b
iffElimRight :: (a <-> b) -> b -> a

Documentation

type True = () Source #

The trivially-inhabited type. True is defined as '()' to give it a canonical construction, so that all proofs of True are identical.

type False = Void Source #

The uninhabited type.

type (/\) a b = (a, b) Source #

type (\/) a b = Either a b Source #

type Not a = a -> False Source #

Negation of a type. Because this is an arrow type alias, not-introduction and elimination are not part of this module.

type (<->) a b = (a -> b) /\ (b -> a) Source #

Iff. Some derived rules are defined for iff for the sake of completeness.

andIntro :: a -> b -> a /\ b Source #

andElimLeft :: (a /\ b) -> a Source #

andElimRight :: (a /\ b) -> b Source #

orIntroLeft :: a -> a \/ b Source #

orIntroRight :: b -> a \/ b Source #

orElim :: (a -> c) -> (b -> c) -> (a \/ b) -> c Source #

trueIntro :: True Source #

exFalso :: False -> a Source #

Ex Falso Quod Libet - it is recommended when writing functions of this form to use the EmptyCase extension, to make the compiler check that the type is uninhabited.

iffIntro :: (a -> b) -> (b -> a) -> a <-> b Source #

iffElimLeft :: (a <-> b) -> a -> b Source #

iffElimRight :: (a <-> b) -> b -> a Source #