[FOM] Some informative questions about intuitionistic logic and mathematics

[Richard Heck]

>1) Is there a definable (in the same way implication is definable 
>in classical logic in terms of disjunction and negation) unary
>connective @ of intuitionistic logic such that for every A, B we have
>that (DNE) A and @@A intuitionistically follow from each other,
>and (EFQ) B intuitionistically  follows from the set {A, at A}?
>  
>
I think the answer to this question is "No". It's easy to prove that it
is if we're allowed /reductio/, since we can show that (%) and reductio
for @entail that ~A and @A are interderivable:
[1] (1) ~A Premise
[2] (2) A Premise
[1,2] (3) Falsum /ex falso quodlibet/ for ~
[1] (3) @A (1)[2]reductio for @
and /mutatis mutandis/ back the other way, in which case we need EFQ for
@ and reductio for ~. But then, of course, we have DNE for ~, by DNE for @.

It's hard to get moving without reductio, since then we have no
introduction rule for "@". But the proof that @A entails ~A survives, of
course, and it's worth noting that we don't need (DNE) either way for
the proof of equivalence. What this shows is that the standard
intuitionistic introduction and elimination rules for ~ fix its meaning
up to interderivability.

>2) Can one define in intuitionistic logic counterparts of the  
>classical connectives so that the resulting translation 
>preserves the consequence relation of classical logic? (Obviously,a
>negative answer to question 1 entails a negative one to question 2).
>  
>
If the consequence relation for classical logic held, then we would have
reductio for @. But then @A is interderivable with ~A, by the foregoing.
So the answer is "No".

Of course, there is a translation that meets a weaker condition that
does preserve the classical consequence relation, namely: Put double
negations everywhere you can fit them. This does not meet the condition
in (2) because it translates p by ~~p (more generally, an atomic
sentence by its double negation), whereas (2) allows us to muck about
only with the connectives.

>3) In several postings it was emphasized  that LEM applies
>in intuitionistic logic to "decidable" relations. Is there
>an intuitionist definition of "decidable" according to which
>this claim conveys more than a trivial claim of the form "A implies A"?
>  
>
"A is decidable" means: A v ~A. An n-ary relation R is decidable if:
(x_1)...(x_n)(Rx_1...x_n v ~Rx_1...x_n). Obviously, those are
classically equivalent to "If A, then A". I hope that doesn't cause
these explanations to meet with disapproval!

>4) Some postings mentioned also "undecidable" relations (or predicates).
>What is the definition of "undecidable" here? is a relation P
>intuitionistically undecidable if there is procedure that produces
>a proof of absurdity from a procedure that given any x either provides
>a proof of P(x) or a procedure that carries any proof of P(x) to
>a proof of absurdity?
>  
>
Yes. So no /proposition/ is /un/deciable---we can never prove: ~(A v
~A)---though a relation can be undecidable, since we can (given
appropriate assumptions) sometimes prove: ~(x)(y)(Rxy v ~Rxy). See below.

>5) Does an intutionistically-undecidable predicate intutionistically-exist?
>  
>
It's provable in intuitionistic analysis that: ~(x)[x<0 v ~(x<0)]. The
proof uses the so-called continuity principles; the theory of choice
sequences plus the continuity principles is therefore inconsistent with
classical logic. There's an easy proof based upon Brouwer's uniform
continuity theorem, which says that every total function on the real
line is everywhere uniformly continuous. (It too rests upon the
continuity principles, and its proof is /not/ easy. One might be getting
the sense that the continuity principles are pretty dang strong.)
Suppose, for /reductio/, that (*) (x)[x<0 v ~(x<0)]. Define f(x) = 0, if
x<0; 1, otherwise. By (*), f(x) is total. But f(x) is not continuous at x=0.

This may seem surprising. We have:
(i) ~(x)(Fx v ~Fx).
But as an consequence of the fact that the double negation of excluded
middle is always provable, we also have:
(ii) (x)[~~(Fx v ~Fx)].
That is, to be sure, /classically/ inconsistent with (i), but it is not
intuitionistically inconsistent with (i). That is a reflection of the
fact that
~(x)(Fx) & ~(Ex)(~Fx)
is, while clasically contradictory, intuitionistically consistent. We're
just talking about the case where Fx is an instance of excluded middle.

The fact just mentioned is a too-little noticed feature of
intuitionistic logic, in my view. It's sometimes said, for example, that
an intuitionist cannot /deny/ the law of bivalence but must only refuse
to assert it. If, however, bivalence is distinguished from excluded
middle and taken to be the claim that every sentence is either true or
false (=not true), then this is mistaken: An intuitionist can perfectly
well claim that not every sentence is either true or false. It is
perfectly consistent (by her standards) for her also to claim that there
is no sentence that is neither true nor false.

There's a nice application in the theory of vagueness: If one's logic is
intuitionsitic, then one can assert that not every man is either bald or
not bald---that's what there being "borderline cases" amounts to---but
still deny that there are any men who are neither bald nor not bald,
thus denying that there is some "third status" for people to have. One
might take this claim to imply that not every proposition is true or
false: In particular, it is not the case that, for all x, the
proposition asserting of x that x is bald is true or false.

That won't solve the Sorities paradox by itself, but it gives one some
helpful resources.

Richard Heck

-- 
==================================================================
Richard G Heck, Jr
Professor of Philosophy
Brown University
http://bobjweil.com/heck/
==================================================================
Get my public key from http://sks.keyserver.penguin.de
Hash: 0x1DE91F1E66FFBDEC
Learn how to sign your email using Thunderbird and GnuPG at:
http://dudu.dyn.2-h.org/nist/gpg-enigmail-howto