FOM: intuitionistic and classical truth

[William Tait]

Neil,

Concerning

> Bill Tait says that for a mathematical proposition A, A is equivalent
> to the proposition that A is true.
>
I actually said something stronger: I quote myself: ``For
a  mathematical proposition A (as opposed to a formal sentence
interpreted in a structure), the proposition that A is true is the same
as the proposition A.'' For what would count as a proof of the former
other than a proof of the latter?

> Moreover, the only warrant for
> asserting A would be a proof of A.
>
> The classicist and intuitionist would both agree with these points.
> Where they part company is in saying *what truth consists in*. For the
> intuitionist, "A is true" is (analytically, conceptually) equivalent
> to "There exists a proof of A".
>
I don't understand (nor did Frege) what you (or Dummett) mean by
``saying  *what truth consists in*''. To say what it means for A to be
true, I can repeat it or translate it into German  or whistle it or go
on and explain further the meanings of the words occuring in A. But what
more could I do?

It follows from this that to say that, for the intuitionists, ``A is
true'' is equivalent for intuitionists to ``A is provable'' is to say
that, for them, the latter is equivalent `(analytically, conceptually)'
to A. I would agree that (anyway, for the intuitionists) to understand A
is to know what would count as a proof of it.


> From that conceptual identification the intuitionist then argues
> further that the proofs whose existence constitute truth should not
> contain any strictly classical moves.  Thus the intuitionist ends up
> saying, in effect, that "A is true" is (analytically, conceptually)
> equivalent to "There exists a (suitably intuitionistic) proof of A".
>
> The further argument just referred to is pretty involved; and it is at
> this locus that Dummett's contribution is most important.
>
First, I would say that you are speaking here of Dummett's
reconstruction of the intuitionist position, not about Brouwer of
Heyting, for example.

But, anyway, the analysis does not depend on your `conceptual
identification'; it depends only on the view that a proposition is
completely given when it is specified what counts as a proof of it. One
then defines logically complex propositions by specifying what counts as
their proofs in terms of what counts as proofs of their components.

Sofar, this is a tenable view also on the classical conception of
mathematics.  The `further argument', that it leads to a constructive
conception of logic, is presumably the argument that Dummett has given
in print. I have argued elsewhere that it is not sound.

I think that, at this point, we are in an `is---is not' situation.

Bill Tait