M. E. Maietti and G. Sambin

Intensionality vs. extensionality: a solution with two levels of
abstraction.


Some precise results show that extensionality of a theory is
incompatible with its effectiveness, when this is meant to include
consistency with the axiom of choice and internal Church thesis. This
looks as an obstacle to the project of formalization of mathematics in a
computer language, since the latter is by definition effective while the
former is extensional by tradition.
There is a way out (which we first proposed at TYPES '04) which is very
natural, although contrary to established tradition. That is to
introduce two theories: a ground type theory, which is a sort of
idealized programming language and thus is intensional, and an
extensional theory, suitable to develop (constructive) mathematics. The
novelty lies on the link between the two theories: the extensional
theory is to be obtained from the intensional one by abstraction, that
is by "forgetting" some information, and this is to be done in such a
way that implementation is always possible, that is, by forgetting only
those pieces of information which can be restored at will. This
requirement is not as trivial as it may look at first: the second
incompleteness theorem by Gödel says that the normalization process of
a formal system will always be a source to restore information, which is
not available within the system itself.