solidot新版网站常见问题,请点击这里查看。
消息
本文已被查看3347次
Polymorphism and the obstinate circularity of second order logic: a victims' tale. (arXiv:1710.10205v1 [math.LO])
来源于:arXiv
The investigations on higher-order type theories and on the related notion of
parametric polymorphism constitute the technical counterpart of the old
foundational problem of the circularity (or impredicativity) of second and
higher order logic. However, the epistemological significance of such
investigations, and of their often non trivial results, has not received much
attention in the contemporary foundational debate. The results recalled in this
paper suggest that the question of the circularity of second order logic cannot
be reduced to the simple assessment of a vicious circle. Through a comparison
between the faulty consistency arguments given by Frege and Martin-L\"of,
respectively for the logical system of the Grundgesetze (shown inconsistent by
Russell's paradox) and for the intuitionistic type theory with a type of all
types (shown inconsistent by Girard's paradox), and the normalization argument
for second order type theory (or System F), we indicate a bunch of subtle
mathem 查看全文>>