FW: paradoxes and intuitionist logic

[Francois-Rene Rideau]

> 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).
Oh, you mean the ``deduction theorem'' (a metatheorem), don't you?

> Equivalently, it can be stated as a set of axioms like this:
> S: (X -> Y -> Z) -> (X -> Y) -> X -> Z
> K: X -> Y -> X
You can deduce a deduction theorem from a system composed of such axioms,
but the theorem is a global property of the system that I'm not convinced
is invariant when you add new axioms.

Note that the deduction theorem can be seen as the fact that you can
abstract over any hypothesis, i.e. as the expressibility of a lambda
construct in the proof language of your system...

> 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. 
That's the principle of bounded quantification:
the variable introduced by a quantifier (forall, lambda, exists, witness)
MUST always be bounded by a small enough set, type, etc,
so that it be possible to have a well-founded semantics to logical sentences.

> 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,
by ensuring strong normalization of the calculus, such as in Coq
(i.e. every term reduces into a normal form in finite time).
The disadvantage is that such a type system
is incompatible with Turing-equivalence of the calculus.
For this reason, some use non-decidable type-systems (such as system F),
where the user has to help the system find the right type.

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.
Instead of having a limited static semantics for "valid obs",
you have the fullest possible "dynamic" semantics.

> 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

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

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

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

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é