[FOM] Intuitionists and excluded-middle
Todd Wilson
twilson at csufresno.edu
Wed Oct 12 18:41:14 EDT 2005
Arnon Avron wrote:
> "not A" means that there is a procedure that transforms
> any proof of A to a proof of an absurdity [...] Although I have some problems in understanding
> the intuitionists' explanations (how can a procedure
> transform one thing to another which by definition does not exist?),
>
This is possible only if the first thing "does not exist" in the same
sense. For example, the proposition
not not (A or not A)
is seen to be valid under this interpretation, since, given a supposed
proof, P, of "not (A or not A)", we can first construct a proof P1 of
"not A" (take a given proof of "A", use it to give a constructive proof
of "A or not A", and invoke P to get a proof of absurdity), second
construct a proof P2 of "not not A" (similarly take a proof of "not A",
use it to give a constructive proof of "A or not A", and invoke P), and
finally invoke P2 on P1 to get a proof of absurdity, showing that P
could not have existed in the first place.
> I am somehow able to make (classical!) sense of them, and even
> see circumstances in which intuitionistic logic can be quite useful.
> Hence I do not have a serious problem with the way intuitionists apply
> their notions. I do have some reservations about the fact that they
> insist on using words like "not" and "or" in a way which is very different
> from the ordinary meanings of these words, but if this would make
> them happy, I am ready to leave these words to them, and use
> "c-not", "c-or" etc for the classical notions
Intuitionistic and classical propositional logic of course agree when
restricted to decidable statements. Significantly, these include at
least the (provably) Delta_1 formulas of arithmetic. In general, the
Intuitionist can always choose to understand classical statements using
a double-negation or negative translation, for example understanding "A
c-or B" as "not not (A' or B')", where A' and B' are the translations of
A and B, in effect replacing the assuredness of the classical
mathematician with the more tentative conviction that the opposite will
never be proven. Indeed, "not not A" acts as a kind of consistency
statement about "A", but it is a very special kind, since the
simultaneous granting of "real truth" to all such "tentative truths"
leads the Intuitionist not to a contradiction -- as one might naively
suppose after encountering many examples where S + A and S + B are both
consistent, but S + {A,B} is not -- but rather to classical logic.
Todd Wilson
Department of Computer Science
California State University, Fresno
More information about the FOM
mailing list