[FOM] Intuitionists and excluded middle

[Andrej Bauer]

Keith Brian Johnson wrote:
> Taking "having a truth-value" to mean "having a constructible proof"
> or, alternatively, taking it to mean "having been constructibly
> proven," I can't see the meaning of denying either (a) or (b), at least
> not while holding time and claimant fixed.

Keith almost surely does not mean to say what he says. For
"to have a truth value" does not mean "to have a constructive proof"--a
sentence could have a truth value and no proof, constructive or
otherwise (consider the sentence "0 = 1" whose truth value is "false"
and has no proof, hopefully).

Do "constructivists" and "intuitionists" really claim that truth is the
same thing as constructive provability? I understand that there may be
philosophical and pre-mathematical discussions about the meaning of
constructive mathematics in which this is claimed, but I would expect a
modern _mathematical_ view to distinguish between provability in a
formal system and validity in a model, even for intuitionistic theories.

Hendrik Bloom claimed that:

(a) intuitionistists deny that every sentence either has a
    truth-value (possibly more than one) or does not.

(b) intuitionists deny that every sentence either has exactly one
    truth-value or has none.

I do not know about "intuitionists", but I can tell you that in toposes,
which are models of (a certain kind of) intuitionistic theories, there
is the object of truth values, Omega (often named "the object of
propositions", which strictly speaking is a misnomer as propositions may
be open). Sentences are interpreted as elements (global points) of
Omega. Thus, each sentence has precisely one truth value, namely the one
assigned to it under the interpretation in the model. This falsifies
both (a) and (b) because:

(a) every sentence has a truth-value in any model.

(b) every sentence has exactly one value in any model.

If Keith and Hendrik meant "true" when they wrote "has a truth value",
then, well, then please be more careful.

One last remark: it seems that a lot of confusion around here arises
from misunderstanding of how the size of a set can or cannot be measured
in intuitionistic mathematics. Let Omega be the set of truth values
(i.e. the powerset of a singleton). We have the following;

- "Omega has at least two elements", meaning: true and false are
  distinct elements of Omega,

- "Omega does not have more than two elements", meaning: there is no
  truth value which is distinct from both true and false.

However, we cannot prove that "Omega has exactly two elements", meaning
 that each truth value is equal either to true or to false, because that
is just a reformulation of LEM.

In other words, intuitionistically, we cannot prove that the set of
truth values has a size which is an integer. The question "how many
truth values are there?" cannot be answered with a natural number--an
assumption easily made by a classical mathematician.

Andrej Bauer