Why is excluded middle called "excluded middle"?

[Martin Escardo]

(Or "excluded third" in other languages.)

In a recent talk, in the course of a proof in a certain constructive
system, I needed to use the observation that (internally in that
system), there is no truth value other than true or false. People were
puzzled (but they shouldn't have been, of course).

This is the case, for instance, in the internal language of any topos.
We have, where Omega is the object of truth values,

(1) not(exists p:Omega. p/=true /\ p /= false),

which is another way of saying that

(2) not(exists p:Omega. not p /\ not(not p)),

because we have

(3) p=true <-> p and also p=false <-> not p.

Then a member of the audience said: "So, excluded middle does hold in
constructive mathematics", which caught me by surprise. I couldn't
disagree with this (terminological) view, of course: (1) is precisely
excluding truth values other than true or false.

While (2) is clear, (1) of course depends on (3), which is a particular
case of propositional extensionality, namely p<->q iff p=q, which we may
not always have, but we do have in toposes and other situations. The
fact that *externally* we can see different truth values (say, in
toposes) only obscures this discussion.

In any case, what constructive mathematics says is that there is a big
leap from saying that there is no truth value other than true or false
to saying that given any truth value we can establish which among true
or false it is.

So perhaps excluded middle (in its received meaning), should not be
called "excluded middle".

Martin

[Kreinovich, Vladik]

I agree that it would be nice to change the terminology but this is tough.

I think it is easier to explain if instead of formal not so clear descriptions, we use the usual intuitive idea that in constructive mathematics, Ex Ax means that we can construct an object x for which Ax is true, and, similarly, A \/ B means that we can constructively point out whether A is true or B is true.

From the viewpoint of this interpretation, the statement A \/ ~A is clearly not true, since otherwise we would have an algorithm that, given a formula A, tells whether it is true or not -- which, since Gödel's result, it known to be impossible.

Your statements (1) and (2), in these terms, basically say that ~~(A \/ ~A), i.e., that it is impossible to have both ~A and ~~A. This double negation of the law of excluded middle (for the lack of better term) is definitely constructively true.
________________________________________
From: construc...@googlegroups.com <construc...@googlegroups.com> on behalf of Martin Escardo <m.es...@cs.bham.ac.uk>
Sent: Thursday, November 19, 2015 4:16 PM
To: construc...@googlegroups.com
Subject: Why is excluded middle called "excluded middle"?

because we have

Martin

--
You received this message because you are subscribed to the Google Groups "constructivenews" group.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Martin Escardo]

On 19/11/15 23:26, Kreinovich, Vladik wrote:
> I agree that it would be nice to change the terminology but this is tough.

(I don't want to change terminology, of course, but it clearly comes
from a misunderstanding.)

> I think it is easier to explain if instead of formal not so clear descriptions, we use the usual intuitive idea that in constructive mathematics, Ex Ax means that we can construct an object x for which Ax is true, and, similarly, A \/ B means that we can constructively point out whether A is true or B is true.
>
> From the viewpoint of this interpretation, the statement A \/ ~A is clearly not true, since otherwise we would have an algorithm that, given a formula A, tells whether it is true or not -- which, since Gödel's result, it known to be impossible.
>
> Your statements (1) and (2), in these terms, basically say that ~~(A \/ ~A), i.e., that it is impossible to have both ~A and ~~A. This double negation of the law of excluded middle (for the lack of better term) is definitely constructively true.

Yes. Precisely.

The need for this observation (that there is no p:Omega that is
simultaneously different from true and false) occurred in a constructive
proof that for any f:Omega->2 (where 2~1+1, the booleans, or the
decidable truth values, or the binary numbers), we have that either
f(p)=0 for all p:Omega or else f(p)=1 for some p:Omega.

(Which I offer to you as a puzzle.)

Martin

[Mark van Atten]

On a related terminological note: There is also the `quartum non datur'.

Here is for example how Oskar Becker presents matters
in his `Mathematische Existenz' (1927). On p.497, he considers
the following three possibilities:

(1) p holds
(2) not-p holds
(3) p does not hold

and goes on to say that, if one accepts equivalence of (2) and (3),
one has `tertium non datur'. If one distinguishes them, one has
`quartum non datur', for (1)-(3) form a complete disjunction.

Oskar Becker, 1927, `Mathematische Existenz. Untersuchungen zur Logik
und Ontologie mathematischer Phänomene', Jahrbuch für Philosophie und
phänomenologische Forschung, VIII: 439–809. (Facsimile reprints in
book form Max Niemeyer Verlag, Halle a/d Saale 1927 and Tübingen 1973)

Mark.

[Martin Escardo]

On 20/11/15 14:18, Mark van Atten wrote

In my understanding, when I say that p does not hold I mean that not(p)
holds and so (2) is the definition of (3).

But perhaps (3) can be understood meta-linguistically: we can't prove
that p holds.

We can consider, for instance, p = the parallel postulate for Euclidean
geometry. We don't say that it doesn't hold. We rather say that it is
not provable (or disprovable) from the other axioms.

We often hear statements such as "excluded middle (EM) doesn't hold in
Martin-Loef type theory" or "function extensionality (funext) doesn't
hold in (intensional) Martin-Loef type theory" and so on. These
statements, indeed, are not facts expressible in MLTT: neither them nor
their negations are provable internally in MLTT. They are independent of
MLTT, or undecided by MLTT, in the same way that the parallel postulate
in Euclidean geometry is undecided by the other axioms.

Similarly, in the free topos, the axiom of choice "doesn't hold". Or
more precisely, we can't prove it, but also we can't prove its negation.

In all cases above, we have a statement which is said to not hold, but
actually this is a meta-theoretic property of the system to which the
statement belongs.

Again this is similar to what we have in toposes: externally, we may see
a proliferation of truth-values, certain toposes (even in boolean
toposes). But, internally, it is impossible to have a truth value other
than false or true.

Peter Aczel has a nice terminology for such things, perhaps better than
"Brouwerian counter examples": he calls them (constructive) taboos.

But you can equally regard the parallel postulate of Euclidean geometry
as a taboo, in the same vein.

Martin

[Henri Lombardi]

See

http://www.springer.com/us/book/9783319194936

Springer LNM 2138
Constructive Commutative Algebra
Projective Modules Over Polynomial Rings and Dynamical Gröbner Bases

Authors: Yengui, Ihsen


Henri