[FOM] Intuitionists and excluded middle

[Ron Rood]

Keith Brian Johnson wrote on 18 okt 2005 at 05:32 (Europe/Amsterdam):

>>> (Let us call such proofs proofs by *strong* reductio, in
>> contradistinction from proofs which proceed by *weak* reductio. The
>> latter proceed from the assumption that a proposition is true, via a
>> contradiction, to the conclusion that this proposion is false. Note:
>> if
>> one accepts proofs by strong reductio, then one is also committed to
>> accepting proofs by weak reductio. Proofs by weak reductio are
>> acceptable in intuitionistic propositional logic; proofs by strong
>> reductio are not)
>
> I'm puzzled as to how one might accept one but not the other.

A proof by strong reductio schematically proceeds as follows:

not-p
.
.
q and not-q
p.

A proof by weak reductio schematically proceeds as follows:

p
.
.
q and not-q
not-p.

Proofs by strong reductio are admissible in classical logic, as are 
proofs by weak reductio. Proofs by strong reductio are not admissable 
in intuitionist logic, but proofs by weak reductio are.

in order to see the point, note that a proof by strong reductio can be 
"decomposed" into a proof by weak reductio plus an application of the 
elimination rule of double negations:

1.	not-p
	.
	.
	.
k.	q and not-q
k+1.	not-not-p		from 1 and k by weak reductio
k+2.	p			elimination rule

A "shortcut proof" from line 1, via the contradiction on line k, to 
line k+2, snipping the step on line k+1, is a proof of p by strong 
reductio. In some sense, then, elimination of double negations can be 
considered a "hidden component" of proofs by strong reductio, the other 
component being a weak reductio. However, elimination of double 
negations is not allowed in intuitionist logic. Thus, one can get a 
good feel of why proofs based on strong reductio are intuitionistically 
inadmissable.


> It seems
> to me that if I accept that every sentence either has a truth-value
> (possibly more than one) or does not; and if I more strongly accept
> that every sentence either has exactly one truth-value or has none;
>

I might add that Gödel proved that intuitionistic logic is not an 
n-valued
logic, for any n. See K. Gödel. "Zum intuitionistischen 
Aussagenkalkül." In:
K. Gödel. Collected works, vol. I, Feferman et al (eds.), pp.222-5.

Ron Rood