At the very beginning of Feferman's *Arithmetization of metamathematics in a general setting* it can be read:

The method of arithmetization, as developed by Gödel[10], exploits the possibility of defining within a formal theory $\mathcal{T}$, or in arithmetical theories closely related to $\mathcal{T}$, various syntactical and logical notions concerning $\mathcal{T}$. In broad terms, the applications of the method can be classified as being

extensionalif essentially only numerically correct definitions are needed, orintensionalif the definitions must more fullyexpressthe notions involved, so that various of the general properties of these notions can be formally derived.

He then proceeds to enumerate results of what he calls the extensional type (Gödel's first incompleteness theorem, non-definability of predicates in formal theories, undecidability of various theories and degrees of unsolvability of various theories), results of intensional type (Gödel's second incompleteness theorem, comparison of theories by relative consistency proofs and ordinal logics), a result of mixed character (the arithmetization of Gödel's completeness theorem for first-order logic), and finally of proofs which are "instances where intensional methods are used to deduce purely extensional results" (the proofs of non-finite axiomatizibility of various theories $\mathcal{T}$ obtained by showing $\mathcal{T}$ to be reflexive, i. e. that the consistency of every finite subtheory of $\mathcal{T}$ is provable in $\mathcal{T}$).

I guess that for the trained logician these examples suffice for him or her to get a clear sense of what is meant by intensional and extensional methods and results in this context, but this is not my case. I would be grateful if anyone could help to make these notions precise.

Thank you in advance.