The Analogical Engine

The field with one element

The Anatomy of Integers and Permutations.

The best part is – they even made it into a screen play.

What’s the use of a matrix if you can’t find its characteristic polynomial? So, a very primitive haskell type for polynomials:

 
import MyPermutations
import MyMatrices
 
type Polynomial = [Int]
 
polySum :: Polynomial -> Polynomial -> Polynomial
polySum p q = if (length p >= length q) 
	then zipWith (+) p (q ++ [0,0..])
	else zipWith (+) q (p ++ [0,0..])
 
polyProduct :: Polynomial -> Polynomial -> Polynomial
polyProduct p q = map (polyProduct' p q) [0..((length p) + (length q) - 2)]
 
polyProduct' :: Polynomial -> Polynomial -> Int -> Int
polyProduct' p q k = sum [ ((p++[0,0..])!!i) * ((q++[0,0..])!!(k-i)) | 
                                         i <- [0..k] ]
 
.

Its not too much effort to generalize matrices with integer entries to matrices with polynomial entries:

 
type MatrixPoly = [[Polynomial]]
 
polyMatTranspose :: MatrixPoly -> MatrixPoly
polyMatTranspose ([]:xs) = []
polyMatTranspose xs = (map head xs):(polyMatTranspose (map tail xs))
 
polyMatProduct :: MatrixPoly -> MatrixPoly -> MatrixPoly
polyMatProduct m1 m2 = polyMatProduct' m1 (polyMatTranspose m2)
 
polyMatProduct' :: MatrixPoly -> MatrixPoly -> MatrixPoly
polyMatProduct' [] m = []
polyMatProduct' (r:rs) m = (polyFindRow' r m):(polyMatProduct' rs m)
 
polyFindRow' :: [Polynomial] -> MatrixPoly -> [Polynomial]
polyFindRow' r m = map (foldr (polySum) [0]) (map (zipWith (polyProduct) r) m)
 
polyDeterminant :: MatrixPoly -> Polynomial
polyDeterminant m = foldr (polySum) [0] (map (polyDetTerm m) 
                                           (allPermutedLists (length m)))
 
polyDetTerm :: MatrixPoly -> PermutedList -> Polynomial
polyDetTerm m p = map (\x -> (-1)^(sign p) * x) (polyDetTerm' m p)
 
polyDetTerm' :: MatrixPoly -> PermutedList -> Polynomial
polyDetTerm' _ [] = [1]
polyDetTerm' (m:ms) (p:ps) = polyProduct (m!!(p-1)) (polyDetTerm' ms ps)
 
polyMinor :: MatrixPoly -> [Int] -> [Int] -> MatrixPoly
polyMinor m rows cols = [ [ (m!!(i-1))!!(j-1) | j <- cols ] | i <- rows ] 
 
almostPolyMatInverse :: MatrixPoly -> MatrixPoly
almostPolyMatInverse m =  [ [ polyDeterminant $ polyMinor m (foo n i) (foo n j) 
                                        |  i <- [1..n] ] | j <- [1..n]]
	where n = length m
 
.

Finally:

 
charpoly :: Matrix -> Polynomial
charpoly m = polyDeterminant $ matPolyAdd (matToPolyMat m) 
      (diagonalPolyMat (take (length m) (repeat [0,-1])))
 
matToPolyMat :: Matrix -> MatrixPoly
matToPolyMat = map (map (\x -> [x])) 
 
matPolyAdd :: MatrixPoly -> MatrixPoly -> MatrixPoly
matPolyAdd = zipWith (zipWith (polySum))
 
diagonalPolyMat :: [Polynomial] -> MatrixPoly
diagonalPolyMat xs = diagonalPolyMat' (length xs) 1 xs
 
diagonalPolyMat' :: Int -> Int -> [Polynomial] -> MatrixPoly
diagonalPolyMat' _ _ [] = []
diagonalPolyMat' n k (x:xs) = ((take (k-1) (repeat [0])) ++ [x] 
         ++ (take (n-k) (repeat [0]))):(diagonalPolyMat' n (k+1) xs)
 
.

First thoughts on how to implement basic matrix funcitonality in haskell:

 
 
import MyPermutations
import Data.List
 
type Matrix = [[Int]]
 
matTranspose :: Matrix -> Matrix
matTranspose ([]:xs) = []
matTranspose xs = (map head xs):(matTranspose (map tail xs))
 
matProduct :: Matrix -> Matrix -> Matrix
matProduct m1 m2 = matProduct' m1 (matTranspose m2)
 
matProduct' :: Matrix -> Matrix -> Matrix
matProduct' [] m = []
matProduct' (r:rs) m = (findRow' r m):(matProduct' rs m)
 
findRow' :: [Int] -> Matrix -> [Int]
findRow' r m = map (foldr (+) 0) (map (zipWith (*) r) m)
 
determinant :: Matrix -> Int
determinant m = foldr (+) 0 (map (detTerm m) (allPermutedLists (length m)))
 
sign :: PermutedList -> Int
sign [] = 0
sign (x:xs) = (inversions' x xs) + (sign xs)
 
inversions' :: Int -> [Int] -> Int
inversions' k xs = length $ filter (\x -> (x < k)) xs
 
detTerm :: Matrix -> PermutedList -> Int
detTerm m p = (-1)^(sign p) * (detTerm' m p)
 
detTerm' :: Matrix -> PermutedList -> Int
detTerm' _ [] = 1
detTerm' (m:ms) (p:ps) = m!!(p-1) * (detTerm' ms ps)
 
minor :: Matrix -> [Int] -> [Int] -> Matrix
minor m rows cols = [ [ (m!!(i-1))!!(j-1) | j <- cols ] | i <- rows ] 
 
almostMatInverse :: Matrix -> Matrix
almostMatInverse m =   [ [ determinant $ minor m (foo n i) (foo n j) |
                                                   i <- [1..n] ] | j <- [1..n]]
	where n = length m
 
foo :: Int -> Int -> [Int]
foo n k = delete k [1..n]
 
.

Lets introduce a third internal representation of a coloured permutation as a pair:

 
[sigma, colourvector] 
 
.

where sigma is a vanilla permutation, and colourvector is a list of colours.

Coloured permutation matrices are always monomial matrices

 
gap> A := ColouredMatrix((1,2,3,4),[E(3),1,E(3)^2,E(3)]);
 
[ [ 0, 1, 0, 0 ], [ 0, 0, E(3)^2, 0 ], [ 0, 0, 0, E(3) ], [ E(3), 0, 0, 0 ] ]
 
gap> IsMonomialMatrix(A);                                
 
true
 
.

We need a function that translates a permutation matrix into a permutation.

 
pointToVector := function( n, k )
	local i, vect;
	vect := [];
	for i in [1..n] do
		vect[i] := 0;
	od;
	vect[k] := 1;
	return vect;
end;
 
vectorToPoint := function( vect )
	local k;
	k := 1;
	while (vect[k] = 0) do
		k := k + 1;
	od;
	return k;
end;
 
matToPerm := function( mat )
	local listperm;
	listperm := List( mat, row -> vectorToPoint( row ));
	return PermList(listperm);
end;
 
.

For example:

 
gap> sigma := PermutationMat((1,2,3),3);                 
 
[ [ 0, 1, 0 ], [ 0, 0, 1 ], [ 1, 0, 0 ] ]
 
gap> matToPerm(sigma);                                   
 
(1,2,3)
 
.

Its not much harder now to write a function which translates a coloured permutation matrix into our new internal representation for coloured permutations:

 
vectorToColour := function( vect )
	local k;
	k := 1;
	while (vect[k] = 0) do
		k := k + 1;
	od;
	return vect[k];
end;
 
colMatToColPerm := function( mat )
	local mat2, listperm, colours;
	mat2 := TransposedMat( mat );
	colours := List( mat2, row -> vectorToColour( row ));
	listperm := List( mat, row -> vectorToPoint( row ));
	return [PermList(listperm), colours];
end;
 
.

For example:

 
gap> colMatToColPerm( A );
 
[ (1,2,3,4), [ E(3), 1, E(3)^2, E(3) ] ]
 
.

Going the other way is slightly more tricky. Starting with GAP’s representation of a coloured permutation with colours on points as a permutation in which stabilizes:

 
[sigma, colourvect].
 
.

So, here goes:

 
extractColPerm := function( colperm, k,n )
	local i, points, images, sigma, colours;
	points := Filtered([1..n*k], i -> (i mod k) = 1);
	images := List(points, p -> p^colperm);
	sigma := PermList(List(images, i -> Int((i-1)/k + 1)));
	colours := List(images, i -> E(k)^((i mod k) - 1));
	return [sigma,colours];	
end;
 
.

Now lets test it:

 
gap> gapPerms := Elements(ColouredPerms(3,2));          
 
[ (), (4,5,6), (4,6,5), (1,2,3), (1,2,3)(4,5,6), (1,2,3)(4,6,5), (1,3,2), 
  (1,3,2)(4,5,6), (1,3,2)(4,6,5), (1,4)(2,5)(3,6), (1,4,2,5,3,6), 
  (1,4,3,6,2,5), (1,5,2,6,3,4), (1,5,3,4,2,6), (1,5)(2,6)(3,4), 
  (1,6,3,5,2,4), (1,6)(2,4)(3,5), (1,6,2,4,3,5) ]
 
gap> test := List(gapPerms, sigma -> extractColPerm(sigma,3,2));
 
[ [ (), [ 1, 1 ] ], [ (), [ 1, E(3) ] ], [ (), [ 1, E(3)^2 ] ], 
  [ (), [ E(3), 1 ] ], [ (), [ E(3), E(3) ] ], [ (), [ E(3), E(3)^2 ] ], 
  [ (), [ E(3)^2, 1 ] ], [ (), [ E(3)^2, E(3) ] ], [ (), [ E(3)^2, E(3)^2 ] ],
  [ (1,2), [ 1, 1 ] ], [ (1,2), [ 1, E(3) ] ], [ (1,2), [ 1, E(3)^2 ] ], 
  [ (1,2), [ E(3), 1 ] ], [ (1,2), [ E(3), E(3) ] ], 
  [ (1,2), [ E(3), E(3)^2 ] ], [ (1,2), [ E(3)^2, 1 ] ], 
  [ (1,2), [ E(3)^2, E(3) ] ], [ (1,2), [ E(3)^2, E(3)^2 ] ] ]
 
.

Finally we need to be able to go from our internal representation of a coloured permutation, to GAP’s representation.

 
foo := function( rootofunity, k)
	local power;
	power := 0;
	while not (rootofunity = E(k)^power) do
		power := power + 1;
	od;
	return power;
end;
 
gapPerm := function( sigma, colourvect, k, n )
	local i, images, oldcolours, newcolours;
	oldcolours := List([1..n*k], i -> ((i-1) mod k));
	newcolours := [];
	for i in [1..n*k] do
		newcolours[i] := (oldcolours[i] 
                           + foo(colourvect[Int( (i-1)/k ) + 1],k)) mod k;
	od;
	images := [];
	for i in [1..n*k] do
		images[i] := k*( (Int( (i-1)/k ) + 1)^sigma - 1) 
                                       + 1 + newcolours[i];
	od;
	return PermList(images);
end;
 
.

Final test:

 
gap> List(test, c-> gapPerm(c[1],c[2],3,2));      
 
[ (), (4,5,6), (4,6,5), (1,2,3), (1,2,3)(4,5,6), (1,2,3)(4,6,5), (1,3,2), 
  (1,3,2)(4,5,6), (1,3,2)(4,6,5), (1,4)(2,5)(3,6), (1,4,2,5,3,6), 
  (1,4,3,6,2,5), (1,5,2,6,3,4), (1,5,3,4,2,6), (1,5)(2,6)(3,4), 
  (1,6,3,5,2,4), (1,6)(2,4)(3,5), (1,6,2,4,3,5) ]
 
.

Yes, this code is ugly.

plain text version

Here is a function to produce a coloured permutation matrix in GAP:

 
ColouredMatrix := function( sigma, colours )
	local p,d;
	p := PermutationMat(sigma, Length(colours), Rationals);
	d := DiagonalMat(colours);
	return p * d;
end;
 
.

For example:

 
gap> A := ColouredMatrix((1,2,3,4),[E(3),1,E(3)^2,E(3)]);
 
[ [ 0, 1, 0, 0 ], [ 0, 0, E(3)^2, 0 ], [ 0, 0, 0, E(3) ], [ E(3), 0, 0, 0 ] ]
 
.

Remember that in GAP, the symbol E(3) denotes the primitive cube root of unity. Now we can diagonalize this matrix and find its eigenvectors:

 
gap> Eigenvalues(CF(12), A);
 
[ E(3), -E(3), E(12)^7, -E(12)^7 ]
 
gap> Eigenvectors(CF(12),A);
 
[ [ 1, E(3)^2, 1, 1 ], [ 1, -E(3)^2, 1, -1 ], [ 1, -E(12)^11, -1, E(4) ], 
  [ 1, E(12)^11, -1, -E(4) ] ]
 
.

Remember that in GAP CF(12) is the cyclotomic field extension containing all the twelth roots of unity.

To generate all the coloured permutation matrices of given dimensions we could do something like:

 
AllCombinations := function( k, n );
	if n = 1 then
		return List([1..k], i -> [i]);
	else return Concatenation(List([1..k], 
                                  i -> List( (AllCombinations( k, (n-1)) ), 
                                  ys -> Concatenation([i],ys)  ) 
                    ));
	fi;
end;
 
fish := function( xs, ys )
	local k, new;
	new := [];
	for k in [1..Length(xs)] do
		new[k] := ys[xs[k]];
	od;
	return new;
end;
 
AllColouredMatrices := function( k, n )
	local perms, colours, colourvectors, tori;
	perms := Elements(SymmetricGroup(n));
	colours := List([1..k],i -> E(k)^i);
	colourvectors := List(AllCombinations(k,n), xs -> fish(xs,colours));
	return Concatenation(List(perms, 
                                           sigma -> List(colourvectors, 
                                                  c -> ColouredMatrix(sigma,c) 
                                     )));
end;
 
.

Check it out:

 
gap> AllColouredMatrices(2,2);        
 
[ [ [ -1, 0 ], [ 0, -1 ] ], [ [ -1, 0 ], [ 0, 1 ] ], [ [ 1, 0 ], [ 0, -1 ] ], 
  [ [ 1, 0 ], [ 0, 1 ] ], [ [ 0, -1 ], [ -1, 0 ] ], [ [ 0, 1 ], [ -1, 0 ] ], 
  [ [ 0, -1 ], [ 1, 0 ] ], [ [ 0, 1 ], [ 1, 0 ] ] ]
 
gap> AllColouredMatrices(3,2);
 
[ [ [ E(3), 0 ], [ 0, E(3) ] ], [ [ E(3), 0 ], [ 0, E(3)^2 ] ], 
  [ [ E(3), 0 ], [ 0, 1 ] ], [ [ E(3)^2, 0 ], [ 0, E(3) ] ], 
  [ [ E(3)^2, 0 ], [ 0, E(3)^2 ] ], [ [ E(3)^2, 0 ], [ 0, 1 ] ], 
  [ [ 1, 0 ], [ 0, E(3) ] ], [ [ 1, 0 ], [ 0, E(3)^2 ] ], 
  [ [ 1, 0 ], [ 0, 1 ] ], [ [ 0, E(3) ], [ E(3), 0 ] ], 
  [ [ 0, E(3)^2 ], [ E(3), 0 ] ], [ [ 0, 1 ], [ E(3), 0 ] ], 
  [ [ 0, E(3) ], [ E(3)^2, 0 ] ], [ [ 0, E(3)^2 ], [ E(3)^2, 0 ] ], 
  [ [ 0, 1 ], [ E(3)^2, 0 ] ], [ [ 0, E(3) ], [ 1, 0 ] ], 
  [ [ 0, E(3)^2 ], [ 1, 0 ] ], [ [ 0, 1 ], [ 1, 0 ] ] ]
 
.

Of course there’s always more than one way of doing exactly the same thing, so:

 
ColouredPerms := function( k,n )
	local ck, sn;
	ck := CyclicGroup(IsPermGroup,k);
	sn := SymmetricGroup(n);
	return WreathProduct(ck,sn);
end;
 
.

For example:

 
gap> hyp2 := ColouredPerms(2,2);
 
Group([ (1,2), (3,4), (1,3)(2,4) ])
 
gap> Elements(hyp2);
 
[ (), (3,4), (1,2), (1,2)(3,4), (1,3)(2,4), (1,3,2,4), (1,4,2,3), (1,4)(2,3) ]
 
.

Here GAP is thinking of a signed permutation on symbols as regular permutations on symbols whose action by conjugation stabilizes the permutation:

A slightly larger example:

 
gap> hyp3 := ColouredPerms(2,3);
 
Group([ (1,2), (3,4), (5,6), (1,3,5)(2,4,6), (1,3)(2,4) ])
 
gap> Elements(hyp3);
 
[ (), (5,6), (3,4), (3,4)(5,6), (3,5)(4,6), (3,5,4,6), (3,6,4,5), (3,6)(4,5), 
  (1,2), (1,2)(5,6), (1,2)(3,4), (1,2)(3,4)(5,6), (1,2)(3,5)(4,6), 
  (1,2)(3,5,4,6), (1,2)(3,6,4,5), (1,2)(3,6)(4,5), (1,3)(2,4), 
  (1,3)(2,4)(5,6), (1,3,2,4), (1,3,2,4)(5,6), (1,3,5)(2,4,6), (1,3,5,2,4,6), 
  (1,3,6,2,4,5), (1,3,6)(2,4,5), (1,4,2,3), (1,4,2,3)(5,6), (1,4)(2,3), 
  (1,4)(2,3)(5,6), (1,4,6,2,3,5), (1,4,6)(2,3,5), (1,4,5)(2,3,6), 
  (1,4,5,2,3,6), (1,5,3)(2,6,4), (1,5,4,2,6,3), (1,5,3,2,6,4), 
  (1,5,4)(2,6,3), (1,5)(2,6), (1,5,2,6), (1,5)(2,6)(3,4), (1,5,2,6)(3,4), 
  (1,6,4,2,5,3), (1,6,3)(2,5,4), (1,6,4)(2,5,3), (1,6,3,2,5,4), (1,6,2,5), 
  (1,6)(2,5), (1,6,2,5)(3,4), (1,6)(2,5)(3,4) ]
 
.

To confirm my claim about commuting with the permutation

 
gap> Elements(Centralizer(SymmetricGroup(6), (1,2)(3,4)(5,6)));
 
[ (), (5,6), (3,4), (3,4)(5,6), (3,5)(4,6), (3,5,4,6), (3,6,4,5), (3,6)(4,5), 
  (1,2), (1,2)(5,6), (1,2)(3,4), (1,2)(3,4)(5,6), (1,2)(3,5)(4,6), 
  (1,2)(3,5,4,6), (1,2)(3,6,4,5), (1,2)(3,6)(4,5), (1,3)(2,4), 
  (1,3)(2,4)(5,6), (1,3,2,4), (1,3,2,4)(5,6), (1,3,5)(2,4,6), (1,3,5,2,4,6), 
  (1,3,6,2,4,5), (1,3,6)(2,4,5), (1,4,2,3), (1,4,2,3)(5,6), (1,4)(2,3), 
  (1,4)(2,3)(5,6), (1,4,6,2,3,5), (1,4,6)(2,3,5), (1,4,5)(2,3,6), 
  (1,4,5,2,3,6), (1,5,3)(2,6,4), (1,5,4,2,6,3), (1,5,3,2,6,4), 
  (1,5,4)(2,6,3), (1,5)(2,6), (1,5,2,6), (1,5)(2,6)(3,4), (1,5,2,6)(3,4), 
  (1,6,4,2,5,3), (1,6,3)(2,5,4), (1,6,4)(2,5,3), (1,6,3,2,5,4), (1,6,2,5), 
  (1,6)(2,5), (1,6,2,5)(3,4), (1,6)(2,5)(3,4) ]
 
.

What we need now is a way to translate between these two different representations of the same mathematical object.

plain text version

It is a saddening fact about the universe in which we inhabit that not every linear operator is diagonalizable over . Meet the irritating matrix:

This matrix is guaranteed to haunt your nightmares and shatter whatever cozy and comforting illusions you may have about linear algebra. Some people refer to it as the Jordan block, but I would like to reserve the letter J for the matrix:

So that the irritating matrix is equal to .

The characteristic polynomial of the by irritating matrix is:

This is also the minimum polynomial. The only matrices which commute with the irritating matrix are those of the form:

In other words, a basis for the commutant of the irritating matrix is given by . Equivalently, a basis for the commutant of the irritating matrix is given by the first powers of the irritating matrix (starting from zero).

Luckily for us, the irritating matrix is as bad as things ever get. Over the complex numbers, any linear operator can be put into block diagonal form with irritating matrices corresponding to various along the diagonal. The operator is diagonalizable if the irritating blocks are all of size one.

The “best” kind of matrices are those which are not only diagonalizable, but also have distinct eigenvalues. For example:

For these matrices the characteristic polynomial is equal to the minimum polynomial and contains no repeated roots. In this case:

The only matrices which commute with such a matrix are other diagonal matrices. Equivalently, a basis for the space of linear operators
commuting with the original operator is given by

To see the equivalence, note that to expand the diagonal matrix with eigehvalues in powers of the original matrix with eigenvalues you are looking for a polynomial

such that . Solving this linear system of equations involves inverting a vandermonde matrix, which is only possible if the eigenvalues are distinct.

If your operator is diagonalizable, but contains repeated eigenvalues, then the minimum polynomial still contains no repeated roots, but the characteristic polynomial does. For example:

Here the characteristic polynomial is: while the minimum polynomial is: .

The commutant of such a matrix is much larger than one with distinct eigenvalues. The commutant of our example matrix is:

where the stars denote possible nonzero entries.

Note finally, that both the irritating matrix and matrices with distinct eigenvalues have the property that we can find a vector such that the first powers of the matrix of form a basis. In the case of the irritating matrix take the vector:

In the case of the diagonal matrix with distinct eigenvalues take the vector:

This property can be used to characterize those matrices such that if commutes with then must be a polynomial in .

pdf version

For any finite group the group ring of is the group of formal linear combinations of elements of , with coefficients in and multiplication defined on the basis elements and then extended linearly:

Even though it is called a group ring this important object actually has the structure of a -algebra. That is it is both a ring, and a finite dimensional vector space over . In reading what follows it is important to keep clear in your mind when we are treating as a ring, and when we are treating it as a vector space over .

A representation of of a a -algebra on a finite dimensional vector space is an algebra homomorphism:

Here is the space of endomorphisms of . If is of dimension then once a basis has been chosen may be thought of as the algebra of by matrices.

Every representation of a group on a vector space lifts naturally to a representation of the algebra on the same vector space.

Since these two things are really “the same” in a certain category theoretical sense which I don’t really want to go into just now (I’m starting to sound like a physicist, aren’t I?), we usually drop the hat and swap back and forth freely between the representation of the group, and the representation of the associated group ring.

Now, there are two natural representations of on the group ring thought of as a vector space. Firstly, right multiplication:

given by:

and secondly left multiplication by the inverse:

given by:

The linear map:

is an intertwiner between these two representations. In other words, upto conjugation they are really the same representation

On the dual space of linear functions on we have:

given by:

One can check that:

Since the left and right actions clearly commute, we actually have a representation:

given by:

Similarly we have:

given by:

The linear map:

is an intertwiner between these two representations of .

The inverse map is given by:

We have all the ingredients now to prove the Artin-Wedderburn theorem for semisimple rings.

pdf version

A representation of a finite group is said to be irreducible if there is no nontrivial vector subspace of which is left stable under the action of .

If there is an inner-product lurking in the background, and is a unitary representation, then for every there exists a unique such that . If is such that:

Then it follows that is such that:

But since the representation is unitary, , thus every unitary representation of decomposes into an orthogonal direct sum of irreducible ones. This is the definition of semisimplicity.

Now fix some representation . If is irreducible, then the only maps with the property that for all the following diagram commutes:

are the scalar multiples of the identity.

To see this not that if is an eigenvalue of then the eigenspace of corresponding to is stable under all of and must thus be the whole space. Over every linear operator has at least one eigenvalue.

More generally, suppose that decomposes as:

If they are isomorphic, then we can write:

The which commute with the action of are now of the form:

Finally if is an arbitrary representation, and the underlying vector space decomposes as

This is more or less Schur’s lemma.

pdf version

Suppose we have almost any deduction system whatsoever. (I’m going to refine things and ask for more structure as we go along, but for now it will do.)

Our deduction system consists of a bunch of statements, and some rules for determining when some statements follow from others. It’s not much of a stretch to demand that given any statement , we will be able to prove from it, that is, that we have some trivial deduction . Also, in order to keep things interesting, if we have a deduction , and a deduction , we ought to have some way to join them into a deduction . This will be some sort of “concatenation of proofs”, but we’re not going to care how it’s implemented, just so long as it is associative, and the “identity deduction” above is an identity for it.

So, anyone who knows me well enough should know what’s coming now. We form a category whose objects are statements, and where the set of arrows are exactly the deductions . That is, the proofs of given . The identity arrows are given by trivial deductions, and the composition is our concatenation of proofs.

Let’s rediscover basic logical operations in terms of category theoretic constructions.

Starting simple, what would an initial object correspond to? Well, the property of an initial object is that for any we have a (unique) arrow This seems to suggest that ought to be a statement which is trivially false, as anything can be deduced from it.

How about a terminal object ? There we have for any , a unique arrow So this is behaving like something trivially true.

You might recall that in an arbitrary category with a terminal object, we often define an element of an object to be an arrow What would that be here? Well, it’s a proof of starting from something which is trivially true, or just a proof of Dually, a coelement of which is an arrow will be a proof of falsity from or a refutation of

How about the product of statements and ? Well, should be a statement which, according to the projection maps, implies both and and moreover, if any other statement implies both and then there must be a (unique) proof that implies making the following diagram commute:

These are the usual properties attributed to logical AND, so the existence of (finite) products is, modulo perhaps some squabbling about uniqueness of proofs, equivalent to the notion that we have statements representing the conjunctions of other statements.

In a similar fashion, the coproduct has essentially all the properties we’d expect from logical disjunction (OR) of statements.

How about exponential objects? Recall that if and are objects in some category , then an exponential object is an object of together with an arrow

so that whenever there is an arrow

we have that there is a unique arrow

such that the following diagram commutes:

In order to better follow this, we can try setting to be , in which case becomes simply an arrow and becomes an arrow which we can think of as an element of the exponential.

That is, every proof of should correspond to a proof that

So exponential objects correspond directly with implication.

What about logical negation? Well, we said earlier that an arrow would act like a refutation of so a natural thing to do would be to define to be

Okay, so if our deduction system is in fact a Cartesian closed category with coproducts, it means we have encodings of the usual logical operations. What about the usual properties of logical operations with respect to each other?

Firstly, can we prove the distributive laws? In classical logic, we have that

Secondly, do we get De Morgan’s laws for free, or do we need to add something more to this formulation?

I’ll leave those questions to be answered next time.

[pdf version]