[FOM] Intuitionists and excluded-middle

[Todd Wilson]

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