[FOM] Intuitionists and excluded middle

[Hendrik Boom]

On Thu, Oct 20, 2005 at 03:48:35PM +0200, Andrej Bauer wrote:
> 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).

Let me put my intuitionistic hat on.  Everything I say here will be
in intuitionistic language.

There are two truth values, "true" and "false".  A statement p has the truth
value "true" if is is provable, "false" if it is disprovable.  Thus whether
p has a truth value doesn't depend on whether I have already proved it
or disproved it.  Mind you, I may only know whether it has a truth value,
and which one, once I have proved or disproved it.

For me to be able to assert that every sentence has a truth value,
I would have to have a general proof that every sentence can be
proved or disproved.

> 
> 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.

Once you say "formal theory", things change.  We have to distinguish
between reasoning, which I do by thinking, and formal deduction, which I
do by manipulating symbols according to rules.  We have to distinguish
between proof within the theory, and proof about the theory.

It's reasoning about the theory that leads us to understand whether
sentences are valid in a model, given the definition of the model.
Let's say that the model gives us a (possibly partial) mapping from
formal statements to the values "true" and "false".  I'll further
assume that the axioms and rules of deduction of the theory lead
us from statements that are mapped "true" to statements that are
also mapped "true", otherwise there's not much point in considering
the model.

Now suppose that this model maps every statement of the theory
onto "true" or "false".  (Remember, interpret this constructively.)
Then the model gives us a decision procedure for the formal
theory (except that it might assign truth values to propositions
that are neither provable nor nonprovable), and the formal system
is likely a subtheory of a rather simple classical theory.

This is quite different from formal proof within the formal theory.  Being
formal, the theory could formalize classical, constructive, modal, or
even unintelligible reasoning.


> 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.


Interpreted informally, if every sentence either has a truth-value
or not, then we ould have a decision procude te determine whether
sentences were decidable.
Interpreted formally,  it all depends on the model involved.
If it is such as to map sentence to either "true" or "false"
then we have a (subtheory of a) decidable theory.  I guess I
wasn't considering such theories when I made the statement.

> 
> 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.

If we *define* a truth value to be "true" or "false", as I did, there are
only two truth values.  The set of truth values has quite precise
cardinality, and it is an integer.  But we do end up with propositions
for which we may not know which, if any, of the two truth values they have.
> 
> 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

I've found that discussing intuitionistic logic using a classical
metalogic can be confusing, unless one is extremely formal.  The
original papers on intuitionism didn't even make the distinction
between reasoning and metareasoning -- a naive logic in the style
of naive set theory.

Just sticking the word "constructively" in an otherwise classical
argument isn't enough.  I once saw a construction of an ordinal
number followed by the assertion that it was constructive.  The
author further explained, "Suppose it were not constructive", and
then proceeded to derive a contradiction!

On the other hand, the double-negation translation provides a way
to embed classical-equivalent statements within constructive
language.

My apologies if my unheralded use of perhaps idiosyncratic
intuitionistic terminology caused confusion.  If other
intuitionistic/constructive terminology is in commom
use these days, I stand ready to be updated.

-- hendrik