FW: paradoxes and intuitionist logic

[iepos@tunes.org]

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

I mean the theorem (well it is more of a reasoning pattern than a
theorem in a specific system, i guess) that says that if A leads to B then 
'A -> B' (where '->' is implication).  Equivalently, it can be stated as a 
set of axioms like this:

S: (X -> Y -> Z) -> (X -> Y) -> X -> Z
K: X -> Y -> X

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

hmm... i've obviously missed the boat :-)

but it is beginning to look to me like restricting axioms to applicable
types (sets, things with a particular property, whatever you want to
call it) is a really good idea. in the case of the deductive theorem,
the restriction would be to propositions. 

and the restriction will certainly not always be to propositions.
as another example, in a naive formulation of number theory, we might 
have (in addition to ordinary theorems about equality) these 
unrestrained theorems:

(x+y) + z = x + (y+z)
x + (-x) = 0

the (unsound) rationale is that since we made up '+', '-', and '0'
we can say anything about their relationship we want to. however,
if self-reference is allowed (which must be, if the system has an
even half-decent combinatory base), then it is fairly easy to
prove that "0 = 1" (and that 0 equals anything, for that matter,
and thus everything is equal to everything else). this is because
we have an ob "Y x.x+1" which is equal to itself plus one; if
the system was suitably restricted, it would be impossible to
show that this ob was a number, but in the unrestricted system,
problems are bound to occur... 

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

well, I don't see why the type system couldn't be formulated within
the system. For instance, the deductive theorem could be formulated
as ordinary axioms in the system like this:

all x.all y.all z.prop x -> prop y -> prop z -> (x->y->z)->(x->y)->x->z
all x.all y.prop x -> prop y -> x -> y -> x

there would then be an unrestrained universal instantiation rule
that says if "all f" ('f is a universial set') is proven then "f x" 
('f contains x as a member') can be derived (there is
no need to restrain the rule, since if "all f" is proven, then it
is necessarily a proposition). also there would be unrestrained
modus ponens and unrestrained combinator/lambda reduction.
this way, there would be no need for an external type system.
are there problems with this approach? or is it just that the
improvement is considered as merely technical with no practical
benefit; this may be so in systems like Coq, but in a reflective
system that has to reason about itself, the simpler 'itself' is,
the better.

regarding the intuitionist rejection of the excluded middle, i ask, 
"why?". it clearly leads to paradox when unrestrained, but the 
deductive theorem also leads to paradox when unrestrained yet
intuitionists seem to accept it. my question is: are there statements
that are propositions in the sense of the deductive theorem but
which lead to paradoxes when the excluded middle is also assumed
for them. if this can be shown, then it would be clear that the
deductive theorem and excluded middle are two separate properties
(well, with some overlapping). on the other hand, i am wondering
if it can be shown that the excluded middle follows from deductive
theorem.

> 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!
> 

Thanks for your comments.

- iepos