{-
\begin{verbatim} Time-stamp: "1997-10-13 11:57:01 peter" #include "./standard.half" \end{verbatim}
\newcommand{\defocc}[1]{\framebox{\emph{#1}}} % Defining occurrence
This file contains basic theories for the empty set, the singleton set, and the booleans.
\tableofcontents
-}
{-
\section{ Theory of empty set }
-}
empty
= {- defines .set, .fun -}
theory
{
set = data {} : Set
,
i ( me : set )
= theory
{
elim = case me of {} : ( A : Type )-> A
, {- in particular, elim (( z : Set )-> A z) -}
elim' = case me of {} : ( A : Pow set , z : set )-> A z
,
True = elim Set : Set
,
pred = elim ((x:True)->set)
: ( x : True )-> set
,
o ( other : set )
= theory
{ eq = elim set : set
}
: Theory
}
: Theory
,
fun ( A : Type )
= \ x -> (i x).elim A
: ( x : set )-> A
}
: Theory
,
N0 = {- traditional name -}
empty.set
: Set
,
n0 = empty.set : Set
, n0T = \ a -> (empty.i a).True : Pow n0
, n0p = \ a -> (empty.i a).pred : ( a : n0 , b : n0T a )-> n0
, n0E = empty.fun (Pow n0) : ( i : n0 )-> Pow n0
{- This still satisfies reflexivity! -}
{-
\section{ Theory of a singleton }
-}
,
singleton
= {- theory of singleton set -}
theory
{
set = data { $0 } : Set
,
element = $0 : set
,
i ( me : set )
= theory
{ elim = \ A a -> a {- don't bother to case it -}
: ( A : Type )-> OP A
, True = {- decoding as a set -}
empty.set {- well, it must decode to false! -}
: Set
, pred = empty.fun set : ( x : True )-> set
, o ( other : set )
= {- -}
theory
{ eq = element : set
}
: Theory
}
: Theory
,
True = {- decode as a set -}
\ a -> empty.set
: Pow set
,
pred = \ a -> empty.fun set
: ( x : set, y : True x )-> set
}
: Theory
,
N1 = {- a traditional name -}
singleton.set
: Set
{- we will make this into a transition system later -}
, n1 = singleton.set : Set
, n1T = singleton.True : Pow n1
, n1p = singleton.pred : ( i : n1, j : n1T i )-> n1
, n1E {- Equality on Singleton -}
= \i j->n1 : (i : n1)-> Pow n1
{-
\section{ Boole's theory } The theory of classical truth-values, called after Boole (1815-1864) who when 32 published the Mathematical Analysis of Logic.
Boole's insight was that there is striking similarity between logical operations and arithmetical operations.
Many arithmetical laws lift directly to logical laws, if 0 is interpreted as Falsity, 1 as Certainty, disjunction and conjunction as addition and multiplication, and the exponential as implication. In particular: \begin{itemize}
\item both (0,add) and (1,mul) are monoids, so we have access to a "Sigma" and "Pi" notation, or variadic sums and products over finite lists (over sets if addition and multiplication are commutative and idempotent);
\item distribution laws, for addition and multiplication in exponential position, and for addition in multiplier position.
\item laws that relate finite sums to general sigma (over a family), and general sigma to multiplication.
\item laws that relate finite products to general products (over a family), and general products to exponentiation.
\item laws that involve 0, 1, and exponentiation
\end{itemize}
Whatever conception we have of the value of a proposition, we may call such a thing a "truth value". Truth values certainly have an arithmetical structure, whether or not we think it is precisely a Boolean algebra.
-}
, Bool = theory
{ t = data { $0, $1 } : Set
, true = $1 : t
, false = $0 : t
, {- Bool -}
elim ( A : ( i : t )-> Type )
= \ tt ff x ->
case x of { $0 -> ff, $1 -> tt }
: ( tt : A true
, ff : A false
, x : t
)-> A x
, {- Bool -}
i ( me : t )
= {- Bool.i me -}
theory
{ elim' ( A : ( x : t )-> Type )
= \ tt ff ->
case me of { $0 -> ff , $1 -> tt }
: ( tt : A true, ff : A false )-> A me
, elim1 ( A : Type )
= \ a a1 ->
elim (\junk->A) a a1 me
: BINOP A
, True = {- decoding as a set -}
elim1 Set N1 N0
: Set
, {- Bool.i me -}
{- abandoned. What's wrong? -}
pred = \ i1 ->
elim (\i2-> t)
[(singleton.i i1).elim]
[(empty.i i1).elim] me
: ( i1 : True )-> t
, {- Bool.i me -}
pred = case me of
{ $0 -> empty.fun t
, $1 -> \ junk -> $0
}
: ( i : True )-> t
, {- Bool.i me -}
neg = case me of
{ $0 -> $1
, $1 -> $0
}
: t
, {- Bool.i me -}
o ( other : t )
= let
{ not_other
= case other of { $0 -> $1, $1 -> $0 }
: t
}
in
theory
{ {- (Bool.i me).o other -}
and = case me of { $0 -> me , $1 -> other } : t
, or = case me of { $0 -> other, $1 -> me } : t
, imp = case me of { $0 -> neg, $1 -> other } : t
, lt = case me of { $0 -> other, $1 -> neg } : t
, xor = case other of { $0 -> me, $1 -> neg } : t
, eq = case other of { $0 -> neg, $1 -> me } : t
} {- (Bool.i me).o other -}
: Theory
, {- Bool.i me -}
it = me : t
}
: Theory
} {- Bool -}
: Theory
,
{- We will make this into a transition system later. -}
n2 = Bool.t : Set
, n2T = \ x ->(Bool.i x).True : Pow n2
, n2p = \x ->(Bool.i x).pred : ( x : n2, i : n2T x )-> n2
,
n2E = {- Equality between booleans -}
\ x y ->
let
{ e = ((Bool.i x).o y).eq : n2
}
in (Bool.i e).True
: ( i : n2 )-> Pow n2