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

[Kanovei]

  From: Stephen G Simpson <simpson at math.psu.edu>
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.

V.Kanovei