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.FirstOrder

Description

This module contains type aliases for first-order logic constructions which are expressed as Haskell types, based on those in Hout.Logic.Intuitionistic. This gives definitions for

• the universal quantifier
• the existential quantifier
• first-order equality

It also gives the natural deduction rules for these constructions, though they are not very useful to the programmer.

Synopsis

# Documentation

data Witness (a :: k) where Source #

A witness of a kind inhabitant. Witnesses can be constructed for the Type kind, Constraint kind, or any data kind.

Constructors

 Witness :: (a :: Type) -> Witness a Because Type is the only kind of habitats, it is the only constructor for which we can demand an inhabitant ConstraintWitness :: Witness (a :: Constraint) DataKindWitness :: Witness (a :: (k :: Type))

data Exists k (p :: k -> *) where Source #

The existential quantifier, parameterised by a kind. The predicate itself is required to return a Type, since Exists carries the proof term. If k is Type, then Exists also carries the witness term in a Witness.

Constructors

 Exists :: Witness (a :: k) -> p a -> Exists k p

data Forall k (p :: k -> *) Source #

The forall quantifier. As with Exists, the predicate is required to return a Type. Despite forall being a Haskell built-in, the lack of support for impredicative types means that a newtype is declared for usability.

Constructors

 Forall (forall (a :: k). p a)

data Equal (a :: k) (b :: k) where Source #

Type level equality, parameterised by a kind.

Constructors

 Refl :: Equal a a The unique equality constructor - pattern matching on Refl allows the compiler to deduce that a and b must unify.

existsIntro :: Witness (a :: k) -> p a -> Exists k p Source #

existsElim :: (forall (a :: k). Witness a -> p a -> b) -> Exists k p -> b Source #

Exists elimination, as a continuation.

Note that this has to be expressed in this continuation style because existential types are not allowed in the return type

forallIntro :: (forall (a :: k). p a) -> Forall k p Source #

forallElim :: Forall k p -> p (a :: k) Source #

eqSym :: Equal a b -> Equal b a Source #

eqTrans :: Equal a b -> Equal b c -> Equal a c Source #

eqRewrite :: Equal a b -> p a -> p b Source #

Rewrite by equality.

This could be expressed as an -, but -> is easier to use. The power of the rule is not affected.