[TYPES] proofs of strong normalization for System F

[Wojtek Moczydlowski]

Given that AFAIR system F is equiconsistent with second-order arithmetic,
how could you expect any normalization proof not to involve universal 
quantification over all sets of terms/numbers?

Wojtek

On Tue, 14 Jul 2009, Matthias Blume wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Yes, indeed.
>
> Matthias
>
> On Jul 14, 2009, at 2:35 PM, Derek Dreyer wrote:
>
>> Yes, but the core of McAllester et al.'s proof still involves Girard's
>> method of interpreting a polymorphic type by universal quantification
>> over an arbitrary set.
>>
>> Derek
>>
>> On Tue, Jul 14, 2009 at 9:18 PM, Matthias Blume<blume at tti-c.org>
>> wrote:
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>>>  ]
>>>
>>> There is a 1995 paper in Information and Computation by McAllester,
>>> Kucan, and Otth titled "A Proof of Strong Normalization of F_2,
>>> F_omega and Beyond".  It seems to be somewhat different from the
>>> original Girard proof, but I have not checked the details.
>>>
>>> Matthias
>>>
>>> On Jul 14, 2009, at 1:38 PM, Derek Dreyer wrote:
>>>
>>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>>>>  ]
>>>>
>>>> Andrei,
>>>>
>>>> I would refer you to Jean Gallier's article, 'On Girard's "Candidats
>>>> De Reductibilité"', from the Odifreddi volume of Logic and Computer
>>>> Science, 1990, but perhaps you already know of it.  It is available
>>>> here:
>>>>
>>>> http://repository.upenn.edu/cgi/viewcontent.cgi?article=1739&context=cis_reports
>>>>
>>>> The article presents a number of different variations on Girard's
>>>> proof, such as typed vs. untyped formulations of the logical
>>>> relation,
>>>> in great detail.  It also covers the proof of strong normalization
>>>> for
>>>> F-omega.
>>>>
>>>> I'm not aware of any proof that departs significantly from Girard's
>>>> original idea.
>>>>
>>>> Best regards,
>>>> Derek
>>>>
>>>>
>>>> On Tue, Jul 14, 2009 at 8:16 PM, Andrei Popescu<uuomul at yahoo.com>
>>>> wrote:
>>>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>>>>>  ]
>>>>>
>>>>>
>>>>>
>>>>> Hello,
>>>>>
>>>>>
>>>>>
>>>>> I would like to learn about different proofs of strong
>>>>> normalization for System F and related systems (featuring
>>>>> impredicativity), and also about formalizations of such proofs.  In
>>>>> particular, I am curious if there are any proofs that depart
>>>>> significantly from Girard's original proof idea.
>>>>>
>>>>>
>>>>>
>>>>> Thank you in advance for any help with this,
>>>>>
>>>>>    Andrei Popescu
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>
>>>
>
>