FW: paradoxes and intuitionist logic

[iepos@tunes.org]

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)'.
> 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.

i think this is incorrect, except for possibly some very fragile 
formulations. the thing to note is that if we have unrestricted
excluded middle then we have '(R R) | ~(R R)', which reduces
to '~(R R) | ~(R R)'. However, this does not necessarily imply
'~(R R)' (it would, if we had 'I' of course). however, under
my formulation of '~' and '|', it would be possible to derive
'R R -> z' for arbitrary 'z'. if the system permits reverse-reduction
of lambdas then it is possible to derive '(R R -> z) -> (R R -> z) -> z'
for arbitrary 'z', and thus we'll be able to prove 'z', anything...

so, it sounds like unrestricted excluded middle is just about as
bad as unrestricted deductive theorem... hmm... so, it will need
to be recognized that only some things ("propositions") have these 
properties. however, i don't see a clear intuitive way to tell
if things do. in particular, is it a (false) proposition to state
that a paradox is a proposition, or is it a paradox itself?
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. this
is very messy, and it seems like there must be a better approach. 
actually, it would not be a terrible problem if "statements"
of proposition-hood did not enjoy proposition-hood themselves,
as long as the system recognized it.

hmm...

- iepos