FOM: role of formalization in f.o.m.
Kanovei
kanovei at wmwap1.math.uni-wuppertal.de
Tue Jun 1 02:15:41 EDT 1999
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
More information about the FOM
mailing list