FOM: Intuitionism (Tait)

[Neil Tennant]

On Tue, 18 Jun 2002, Sean C Stidd wrote:

> ... or if
> proof just is proof-in-a-system, does being able to 'observe' the truth
> of this argument show that we have some kind of access to mathematical
> truth that outstrips the reach of proof?

No. It just means that we have to keep expanding our proof systems in
order to prove, formally, propositions tha we have proved informally. This
is a theme also of Harvey Friedman's work--which aims at showing the need
for large-cardinal axioms in set theory, in order to prove simple-seeming
statements of ordinary mathematics.

> I don't think any of this is exactly relevant to the incompleteness
> result proper, since you don't need to know that the sentence is true for
> the semantics-syntax disconnect. (Because you've assumed bivalence &
> excluded middle either the sentence or its negation will be true and
> unprovable.) 

You don't need the classical assumptions of bivalence in the
metalanguage (or excluded middle in the object language). The proof that
the undecidable sentence is one that ought to be asserted is completely
intuitionistic.

> But two questions seem worth answering: (1) If Godel's
> 'metamathematical demonstration' cited above is one we ought to accept as
> valid, what are the philosophical and/or mathematical consequences, if
> any, beyond those of the incompleteness theorem of doing so? 

Siince I believe the antecedent of this conditional question is true, I
shall address it, rather than the follow-up question (2). I believe the
philosophical consequences are confined to the open-ended nature of proof;
and they do not justify anti-mechanism in the philosophy of mind.

Neil Tennant