FOM: role of formalization in f.o.m.

Kanovei kanovei at
Tue Jun 1 02:15:41 EDT 1999

  From: Stephen G Simpson <simpson at>
Date: Mon, 31 May 1999 19:36:19 -0400 (EDT)

> As a preliminary scheme that seems appropriate for discussing the
> current scene in f.o.m., I would propose to distinguish among:
>  1. rigorous mathematics, referring to normal 20th century standards
>     of mathematical rigor.  
>  2. metamathematics, i.e. rigorous arguments showing showing how
>     various pieces of rigorous mathematics can be codified in the
>     predicate calculus.
> ..............

There is another well defined case yet not fully classified 
by this scheme. 

1*. Rigorous mathematics which 
a) starts with an EXPLICITLY DEFINED list L of "postulates" 
b) predends that what follows is based on L and on nothing else, 
c) but, differently from 2, does not claim any adherence to 
any deduction system and may not mention any formal deduction 
at all. 

Example: Euclid, Hilbert. 

This is equal to Simpson's 1 IF we add to 1 that L=ZFC, say. 
This is also equal to Simpson's 2, IF we note that the 
rigogous mathematical reasoning is exactly the predicate 
calculus. Strangely, these two IFs appear to be very 
important for some mathematicians of undisputable greatness.


More information about the FOM mailing list