                           premise.demon.co.uk
        peter 7721 Oct 13 11:57
      /home/peter/half/Boole.half

November 9, 1997

Time-stamp:  "1997-10-13 11:57:01 peter"
#include "./standard.half"

This file contains basic theories for the empty set, the singleton set, and the booleans.

Contents

1 Theory of empty set 1

2 Theory of a singleton 2

3 Boole’s theory 4

1 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!

2 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

3 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:

• 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);

• distribution laws, for addition and multiplication in exponential position, and for addition in multiplier position.

• laws that relate finite sums to general sigma (over a family), and general sigma to multiplication.

• laws that relate finite products to general products (over a family), and general products to exponentiation.

• laws that involve 0, 1, and exponentiation

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