FOM: Bishop's mathematics; Tait/finitism

[Stephen G Simpson]

Antinino Drago writes:
 > Bishop's mathematics, which is well-defined both in mathematical
 > terms (no more than potential infinity) and in logical terms
 > (non-classical logic)

It's not clear to me that `Bishop-style constructivism' is
welldefined.  From the philosophical standpoint, Bishop's subjectivist
ideas seem somewhat incoherent, though not as bad as those of his
predecessor Brouwer.  From the standpoint of f.o.m. and mathematical
logic, there are many decisions to be made beyond rejection of actual
infinity and the law of the excluded middle.  There has been a lot of
research toward formalization of the mathematics of Brouwer and
Bishop, but nothing very conclusive.  See for instance the book by
Michael Beeson.

 > common reference about "finite" mathematics is Tait "Finitism",
 > J. Phil. 1981 which moreover is in my opinion unsatisfactory in
 > identifying "finitism" with primitive recursive functions.

Rather than `primitive recursive functions', I think it would be more
accurate here to refer to PRA, the formal system of primitive
recursive arithmetic.

Tait in his 1981 paper argued that Hilbert's finitism is formalized by
PRA.  This conclusion is widely accepted in the f.o.m. literature.  I
certainly accept it; see e.g. my paper on Hilbert's program
<http://www.math.psu.edu/simpson/papers/hilbert/> and my book
`Subsystems of Second Order Arithmetic'
<http://www.math.psu.edu/simpson/sosoa/>.

Mr. Drago, why don't you accept Tait's conclusion?

-- S. Simpson

Name: Stephen G. Simpson
Position: Professor of Mathematics
Institution: Penn State University
Research interest: foundations of mathematics
More information: www.math.psu.edu/simpson/