[FOM] Formalization Thesis: A second attempt

Vaughan Pratt pratt at cs.stanford.edu
Wed May 26 03:05:49 EDT 2010

```
On 5/25/2010 8:57 AM, Paul Budnik 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
```