paradoxes and intuitionist logic

[iepos@tunes.org]

i've been doing a bit of thinking about the paradoxes and haven't
come to any really good answers and am wondering if any of you have.

one of the most paradoxes occurs when reasoning on a statement
that says "this statement is not true". One first supposes that it
is true; then it follows that it is not true. This is a contradiction,
so the assumption must have been not true. So, the statement is not
true; but this is precisely what the statement says, so we have
admitted the statement. So there is an inconsistency in this logic.
Unfortunately, the inconsistency is not caused merely by the funny
nature of the English language; the argument can be formalized in
a fairly simple sound-appearing logic using the Y combinator (or
lambda term) to achieve the self-reference.

When formalized, the argument usually uses a form of "reductio ad absurdum",
a reasoning pattern that says that if something leads to a contradiction
then it is not true. Some people have tried to avoid the problem by
rejecting reductio ad absurdum along with the excluded middle, 
double-negation, and deMorgan's laws; these kinds of logics are
called "intuitionist" I think. these logics usually retain the
deductive theorem, or a set of axioms like these (I use "->" to represent
implication (if-then)):

I: x -> x 
B: (x -> y) -> (z -> x) -> z -> y
C: (x -> y -> z) -> y -> x -> z
W: (x -> x -> y) -> x -> y
K: x -> y -> x

some people seem to think that these logics solve the problem of
paradoxes (Fare i think hints this in his lambda-nd paper), and I
think that they do actually, _but not when a lambda (with a beta-reduction
rule at least) or an equivalent set of combinators is admitted_.
the fact is, if you have the previously mentioned W and I axioms
along with lambda and modus ponens, then you're toast. anything can
be proven, in this way (note the use of the Y combinator, which can
be written as a lambda term)... 

1. (Y x.x -> z) -> (Y x.x -> z) [by I rule]
2. (Y x.x -> z) -> (Y x.x -> z) -> z [by reduction of the second Y on #1]
3. (Y x.x -> z) -> z [by W rule, modus ponens on #2]
4. ((Y x.x -> z) -> z) -> z [by reduction of the Y on #3]
5. z [by modus ponens on #3 and #4]

the argument is similar to the following: consider the statement
"if this statement is true, then Z". Suppose it is true, then
the condition would be met and Z follows; so if the statement is
true, then Z. This is precisely what the statement says, so Z follows
by modus ponens.

it seems we must give up the deductive theorem (f leads to g, therefore
'f -> g') to remove the inconsistency. anyway, that seemed to be
curry's conclusion in the first volume of  his old book. hmmm...
i'd like to know what others think now.

one other note. I noticed that conjunction ("&") and disjunction ("|")
have nice definitions in terms of universal quantification ("all")
and implication:

x&y = all z.(x -> y -> z) -> z
x|y = all z.(x -> z) -> (y -> z) -> z

the usual properties of & and | quickly follow. also, we define
negation in this way:

~x = all z.x -> z

now, consider '~x | x' (the excluded middle). Written in the terms
above, we have:

all z.((all f.x -> f) -> z) -> (x -> z) -> z

now, the W rule follows from this excluded middle in a fairly simple
system... we can instantiate the 'z' to 'x -> z' (for arbitrary 'z')
and get:

((all f.x -> f) -> x -> z) -> (x -> x -> z) -> x -> z

the head of the implication is an instance of one of the
axiom schemas of a sensible system (universal instantiation), so
'(x -> x -> z) -> x -> z' can be derived for arbitrary 'z' if
'x' obeys the excluded middle. this seems interesting because the W
rule is the one that seems to be causing the problems, but it
can be derived by very sound means if the subject obeys excluded
middle.

anyway... chew on this i guess.
i'd like to know what you guys think...

- iepos