[Prev][Next][Index][Thread]
erratum: Undecidabilty of System F
I am grateful to Henk Barendregt, Martin Hoffmann, and Pawel Urzyczyn
who have pointed out the problem with unjustified "extraction term
from termination proof" trick, which I used to construct the term
$f_p$ in the very end of my proof of undecidability of F published in
the "types" mailing list this summer. Therefore I withdraw my claim
till I find satisfactory reparation or another proof. I am awfully
sorry for creating confusion. I would like to thank Jean-Jacques Levy
and Roberto Amadio for useful discussions.
Sergei Vorobyov
----------------------------------------------------------------
Postscript: here are some explanations
> Henk Barendregt writes:
>
> You have a term f^ p Q x representing f_p x where Q is a proof of
> Inf(X_p). If X_p is infinite (provably so), then this gives a term
> for f_p. If X_p is not infinite we have nothing, it seems.
> Martin Hoffmann writes:
>
> The thing I don't understand is how you obtain a lambda term f_p in
> case p does not have a solution. The only thing which comes to mind
> would be to take the lambda term corresponding to \x . mu y>x .
> "enum(y) solves p" where we use some coding of the mu operator. Of
> course this term is not F typable in case p has no solution, but I
> don't see why it should have an F type in case there is such a
> solution!! Girard's theorem only says that there is an equivalent
> function which does have an F type. Well, ok, I suppose you're trying
> to overcome that by applying f_p to 0. But even then the only thing
> you get is that in case p has a solution then there is a beta-redex of
> f_p 0 which has an F-type, but f_p 0 itself need not have one!!!
> Pawel Urzyczyn writes:
>
> I think there is a gap in your proof on the bottom of p. 4, where you
> claim that there is a uniformly defined term representing the function
> f_p. To extract the proof from the proof of formula above you need to
> provide a PROOF of X, i.e., you actually have to provide a full
> definition of X. An universal formula is like an abstraction that
> awaits an argument. In fact you contradict yourself claiming on line
> 3 bottom-up that the uniformly defined term f_p^ is of TYPE omega ->
> to omega. Yes, it is,provided f_p is total, otherwise you don't have
> defined f_p at all. (If f_p : omega -> omega then of course f_p0:omega
> and is typable.)
I can only add that the function $f_p$ can be easily and directly
F-defined for any decidable $p$ without any reference to Girard's
theorem and any $\mu$-operator. And the theorem itself gives no way to
do it uniformly. Indeed, if $p$ has no solutions we have nothing.