[FOM] Foundational Status of a proof of the Cayley-Hamilton theorem

[Alasdair Urquhart]

Michael Soltys's PhD thesis at the University of Toronto (2001) supervised
by Stephen Cook has some detailed discussions of these and related
questions.  I served on Soltys's committee, and I recall talking
with him about the Cayley-Hamilton theorem at the time.

I'm not sure if his thesis is available online, but you could write
him directly for a copy.

On Sat, 22 Sep 2018, joeshipman at aol.com wrote:

> The Cayley-Hamilton theorem states that any square matrix over a commutative ring R satisfies its characteristic polynomial.
> For any specific n, this is an obviously finitary statement that can be proven, if true, simply by multiplying everything out and applying the standard algebraic
> manipulations. For example, in the 2x2 case, the symbolic determinant of A-xI, where A is
> (a b)
> (c d)
> is (a-x)(d-x)-bc = x^2 - (a+d)x + ad - bc
> and applying that to A gives
> (aa+bc-aa-ad-ad-bc ab+bd-ab-bd)
> (ac+cd-ac-cd bc+dd-ad-dd+ad-bc)
> which is the zero matrix.
> 
> Thus, the theorem as stated is Pi^0_1 : it states that for any N, a certain (polynomial time) program P(N) has a certain output (the zero matrix). It's hardly
> even algebra, because it can be regarded as purely combinatorial.
> 
> But here's my favorite proof. Consider NxN matrices over the complex numbers. Those matrices A which have full rank and distinct eigenvalues have a basis of
> eigenvectors that gives a diagonalizer, an invertible NxN matrix D such that DA(D^-1) has the eigenvalues down the main diagonal and 0s elsewhere. Such an A
> clearly satisfies its characteristic polynomial. However, those A are dense in the N^2-dimensional space of matrices. Therefore the N^2 entries in the output
> P(N), which are polynomials in the N^2 variables corresponding to the matrix elements, are zero on a dense set of complex numbers, and any multivariate polynomial
> which is 0 on a dense set must be identically 0.
> 
> Question: in how weak a theory can "this proof" be carried out, and is the theorem provable in any theory weaker than that? In precisely what sense does this
> proof "require" more than a proof that doesn't pass through the complex numbers?
> 
> -- JS