FW: paradoxes and intuitionist logic

[btanksley@hifn.com]

This message is in MIME format. Since your mail reader does not understand
this format, some or all of this message may not be legible.

------_=_NextPart_000_01BEE835.38CDCDF8
Content-Type: text/plain;
	charset="iso-8859-1"

This got emailed to me instead of the list...  Here it is.


------_=_NextPart_000_01BEE835.38CDCDF8
Content-Type: message/rfc822
Content-Description: Re: paradoxes and intuitionist logic

Message-ID: <199908162212.PAA14540@bespin.dhs.org>
From: iepos@tunes.org
To: btanksley@hifn.com
Subject: Re: paradoxes and intuitionist logic
Date: Mon, 16 Aug 1999 15:12:54 -0700
MIME-Version: 1.0
X-Mailer: Internet Mail Service (5.5.2448.0)
Content-Type: text/plain;
	charset="iso-8859-1"

[Charset iso-8859-1 unsupported, filtering to ASCII...]
> >From: iepos@tunes.org [mailto:iepos@tunes.org]
> >Subject: paradoxes and intuitionist logic
> 
> >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.
> 
> Only if you fail to typecheck your variables.
> 
> >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
> 
> The trouble is, what are you allowed to substitute for the variables?
> Obviously, you can only substitute things which have possible boolean
> answers (as an example, you can't set x to any natural number and expect
> anything to make sense).  Paradoxes cannot have boolean answers, so
> substituting them into these laws is simply ignoring type safety.

This does seem to be the case, indeed. However, without the example
of this kind of paradox there would be people who would be convinced
that it would be okay to formulate implication for unrestricted obs,
with "implications" like "1 -> 2" being taken as true, since "1" certainly
is not true and thus the condition is unmet. although it seems quite
dangerous to take "~1", i don't think it is correct or necessary
to toss out "1 -> 2" entirely because it does not "typecheck";
instead, it seems best to me simply to refuse to apply certain
reasoning patterns to it (reasoning patterns which are reserved to
propositions).

> 
> Things which can be substituted into these laws are called 'propositions'.

this kind of restriction does seem to me to be the right way to go.
However, it is not obvious that even this approach is safe. Before the
paradoxes appeared, it seemed safe to formulate a set of truths
(that is, a category, such that everything either belonged to it
or did not belong to it), however it turns out that this leads to
problems -- or does it? is there a paradox that uses the excluded
middle but not the deductive theorem? now that i think about it,
all the paradoxes i've seen involve the deductive theorem.

anyhow, if it is unsafe after all to formulate a set of truths, then
one should take caution formulating a set of propositions also
(i suppose one could define it as an indefinite "set"; that is, one
without an excluded middle).

on the question of the excluded middle, the first paradox that comes
to mind as a possible problem is russell's. for, consider the
ob "x.~(x x)" (the set of all sets that do not contain themselves).
If we call that set R, then by lambda we have 'R R = ~(R R)'.
this seems on the verge of a problem, however there could be
systems in which equality does not imply logical equivalence (i.e.,
implication both ways). actually, a system with lambda (or combinators)
seems best formulated to me when equality is not taken as primitive
at all, in which a beta-reduction can only take place on previously
proved statements. However, if the I rule of deductive theorem is
admitted, it must be restricted, because if it was not then
we could have 'R R -> R R' and thus 'R R -> ~(R R)' by reduction;
also we would have by I again '~(R R) -> ~(R R)'. then, by the excluded
middle, we would have '~(R R)' (the excluded middle admits
'(x -> y) -> (~x -> y) -> y'). but we would also have '~(R R) -> ~(~(R R))'
and then an inconsistency. however, it seems to me that none of this
would happen if we rejected the 'I' rule of deductive theorem, even
in the presence of the excluded middle.

hmmm... the excluded middle is still not obvious to me though. i would
be interested if anyone knows of any paradoxes involving it but
not the deductive theorem. on the other hand, is it possible that the
excluded middle could be proven as I have formulated it
('all y.(x -> y) -> ((all z.x -> z) -> y) -> y'), at least if
'x' obeys the deductive theorem?

> 
> >- iepos
> 
> -Billy
> 

hmm... thanks for your comments... could anyone else shed some light?

- iepos

------_=_NextPart_000_01BEE835.38CDCDF8--