FW: paradoxes and intuitionist logic

[iepos@tunes.org]

> > 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...
> 
> The classical solution is to have a static type system
> prevent construction of such paradoxical objects,

I'm not really sure what you mean by "construction" of an object;
i guess you mean that the type system forbids the object from
being represented at all, since it is deemed "meaningless".
To me, this seems like a horrible hack (albeit maybe a useful one). 

> The solution I've proposed in my master's thesis
> (and reused in my lambdaND paper) is to instead remark
> that termination of evaluation can be used
> as the ultimate criterion of well-formedness of terms:
> you thus consider a (non-deterministic) call-by-value lambda-calculus
> extended with logic primitives, with convergence towards values
> as the very intuitionnistic "truth" of a logical statement.

Hmm... I don't think I quite understand how your system would work.
Surely there will be expressions with normal forms that represent
absurd statements (or non-statements, like numbers and sets), right? 
Anyway, your system is more ambitious than what I've been looking
for, in that it is not only a logic system (axioms and rules of
inference) but a way for the logic to be carried out (i.e., a calculus). 
This doesn't seem like a bad approach, since a calculus is going to
be necessary at some point if we want computers to be able to
do automated reasoning. Anyway, I'll have to look back over your paper,
since I think I got lost near the end last time (:-)).

> 
> > 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
> In most typed calculi, the type is not an additional condition,
> but a part of the quantification: all x:prop .
> In Coq, the above is (x,y,z:Prop)(x->y->z)->(x->y)->x->z

That's right. But there seems to me to be interest in a system
in which a condition is not a necessary part of quantification
(or if it is, it is at least a "first-class" type, that can
be talked about within the system).

> > 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
> Would need an additional condition "x well-formed",
> maybe implicitly given by the quantifier that binds x
> (in my master's thesis system, all quantifiers were over values,
> not expressions, although for any expression E, (lambda () E)
> was a value suitable protecting expression E).

I think you may have misunderstood what I meant by "all f". I mean what
is sometimes written as "for all x, f(x)"; for sanity's sake, i
mean to use a system based on combinators instead of bound variables,
so there is no possibility for clashes. By "all", I mean Curry's
"universal generality" which he writes using a symbol that looks
kind of like pi.

Anyhow... I don't see the need for the "x well-formed" condition,
In fact, if it rules out 'x's involving paradoxes (applications
of Y and kin, things that may not have normal forms), then the resulting 
system is unacceptable to me, since it can occasionally be useful to talk 
about these paradoxes (for instance, so that the system itself could 
state paradoxes' paradox-hood). remember that i hope to prevent faulty 
reasoning about paradoxes by restricting specific reasoning patterns
rather than tossing them out of the system entirely. 

> > 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.
> I think the system I proposed kind of fits your requirements,
> although I don't know if it is very practical.

hmm.. well your lambdaND approach did avoid external types, didn't
it? i still don't really understand how logic would take place
in that system, but i'm still certainly interested in it...

> 
> > regarding the intuitionist rejection of the excluded middle, i ask, 
> > "why?"
> Constructivism (see Brouwer).
> Only consider as "existing" objects that can be readily constructed;

again, not sure what you mean by "construct". if you mean
"represent finitely in some system", then many paradoxical
objects would be taken to "exist", since they can be
represented finitely in many systems using Y. anyway, i usually
take existence to be at-least-one-memberness (of a set); that is, 
i say that set F exists iff "all x.prop x -> (all y.F y -> x) -> x".
but i think by "exists" in this case you mean "well-formed-ness",
which seems irrelevant to me...

> only consider as "true" assertions what can be readily proven.
> This leads to rejecting excluded middle,
> since (G_del helping) we know that we cannot (in general)
> ensure that the unprovable be provably false.
> 
> > i am wondering if it can be shown that the excluded middle
> > follows from deductive theorem.
> Certainly not. The deduction theorem holds in intuitionnistic logic.

uhh... that does not mean that the excluded middle can't be derived,
when stated in a specific form perhaps. as i understand it, there
is no known intuitionist refutation of the excluded middle (no
counter-example, at least when the deductive theorem holds); they
merely do not naively accept it. anyway, if the deductive
theorem holds universally in the logic, then something is clearly
wrong with it, given all the paradoxes that can be derived...
but i suppose they work around that by basing their system on a
static type system, or bound variables (ooh, what fun :-)).

> 
> 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 ]
> As far as natural selection applies to the human world, we don't ever get to
> "let nature decide", because we ARE part of that nature that decides. Hence,
> any claim to "let the nature decide" is just a fallacy to promote one point
> of view against others, or to ignore one's responsibilities.
> 		-- Far_

heh heh. i really should stop worrying about all this theoretical stuff
and work on a real system, but anyway, this stuff does seem sort of
important, or it will be eventually...

- iepos