FW: paradoxes and intuitionist logic

[Francois-Rene Rideau]

On Mon, Aug 16, 1999 at 04:53:57PM -0700, iepos@tunes.org wrote:
> in my last post, I missed something that seems important...

>> 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)'.
And the paradox is that since by excluded middle,
you have either R R or ~(R R), then by this equivalence,
you have both a proposition and its negation, and hence a contradiction.

> so, it sounds like unrestricted excluded middle is just about as
> bad as unrestricted deductive theorem...
Just what do you call "deductive theorem"?

Note that removing the rule of excluded middle is precisely
what intuitionnistic logics and constructive logics are all about...
they amount to considering only the objective provability of statements,
not their hypothetical and unreachable (hence meaningless) "truth"...

> some systems (Coq?) seem to fear this kind of issue and thus formulate
> the set of propositions _outside_ the system; that is, the set of
> propositions cannot be refered to within the system as a first-class
> set. this means a whole static type system is necessary.
Type systems are the way we've done ever since Russell & Whitehead's
Principia Mathematica.

> this
> is very messy, and it seems like there must be a better approach.
So I'd like to believe.

Regards,

[ "Faré" | VN: Уng-Vû Bân | Join the TUNES project!   http://www.tunes.org/  ]
[ FR: François-René Rideau | TUNES is a Useful, Nevertheless Expedient System ]
[ Reflection&Cybernethics  | Project for  a Free Reflective  Computing System ]
The Constitution may not be perfect, but it's a lot better than what we've got!