FOM: Infinity

[JoeShipman@aol.com]

The most interesting distinction between mathematical systems for the proverbial Man In The Street must be the one between finite mathematics and mathematics that uses infinity.  

This distinction has been satisfactorily formalized by the use of the strongly equivalent systems Peano Arithmetic (PA) and Finite Set Theory (the theory of the hereditarily finite sets, axiomatized by ZF with the Axiom of Infinity replaced by its negation).  (The equivalence follows from Godel's discovery that exponentiation is representable in terms of addition and multiplication.)

My question is, has any *systematic* effort been made to show that those well-known theorems of ordinary mathematics with finitary statements can be proved without using infinite sets?  This would require systematically going through the existing proofs, and I'm not aware of any such program.

Some examples:  The Prime Number Theorem is a theorem of PA.  The Four Color theorem is a theorem of PA (with a very lengthy proof).  The Graph Minor Theorem is NOT a theorem of PA (and is the ONLY theorem I can think of that is finitely stated, well-known to the general mathematical community, and known to be independent of PA).  The status of the use of Infinity in the proofs of the following theorems has not been shown as far as I know:

Faltings's Theorem (formerly Mordell conjecture)
Wiles's Theorem (formerly Fermat conjecture)
Classification of finite simple groups
Poincare Conjecture in dimensions 4 and up (for finitely presented manifolds)

Can anyone familiar with any of the proofs of these theorems discuss whether infinite sets are used in those proofs in an essential way?  Can anyone suggest other theorems as candidates for this type of investigation?

-- Joe Shipman