[FOM] Formalization Thesis: A second attempt

[Vaughan Pratt]

On 5/25/2010 8:57 AM, Paul Budnik wrote:
> Vladimir Sazonov<vladimir.sazonov at yahoo.com>   wrote:
>> Mathematics ***is*** formalising of our thought and intuition.

> That seems too general. I see mathematics as formalizing what
> conclusions (theorems) are logically determined by assumptions
> (axioms).

Very interesting.  I see logic as formalizing the conclusions of 
mathematics.  I wonder how we arrived at such different viewpoints.

Actually I'm not sure anyone I know personally sees mathematics as 
formalizing the conclusions of logic, but those that do would surely 
have to be logicians rather than mathematicians.  Those mathematicians 
that care at all about axioms usually work backwards from what they just 
proved to see what axioms they had been assuming.  "Reverse mathematics" 
is a misnomer: mathematics is reverse logic and logic is reverse 
mathematics.  Anyone doing reverse mathematics is working backwards from 
the mathematics to figure out exactly what logical framework justifies 
their mathematics, which is where foundations began.

There is a belief in some circles today that all mathematics follows 
from one set of axioms, which seems to inform the current usage of 
"reverse mathematics" by characterizing it as subsetting this universal 
set.  While it is fair to say that those originating the 
universal-framework viewpoint were mathematicians, they were behaving as 
early logicians while they were developing it.  Only logically minded 
mathematicians care about a universal system of axioms in the sense of 
foundations.

Group theorists obviously care about the particular axioms of group 
theory (and likewise for other algebraic classes informing linear 
algebra, algebraic automata theory, algebraic number theory, algebraic 
logic, etc.), but axioms of that kind usually make no claim to 
universality (the Tarski-Givant thesis that the axioms of relation 
algebra are universal being a notable exception).

Algebraists might be described as midway between "ordinary" 
mathematicians and logicians.  Certainly logicians and algebraists both 
value axioms.  However whereas the former tend to judge them by their 
universality, the latter are more concerned for their applicability to 
their specific problem domain.  With these different motivations algebra 
would seem to have developed in competition with first order logic, and 
algebraists today are often seen to be ambivalent about whether the 
provenance of their subject is set theoretic or category theoretic.  For 
that matter so are modern logicians, though certainly at the end of the 
last millennium hardly any subscribers to FOM were prepared to stick up 
for category theory as such a provenance.

Vaughan Pratt