hout-0.1.0.0: Non-interactive proof assistant monad for first-order logic.

Copyright (c) Isaac van Bakel 2020 BSD-3 ivb@vanbakel.io experimental POSIX Safe 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

# 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 #

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 #