Feferman's extensional and intensional applications of the method of arithmetization

Question

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 extensional if essentially only numerically correct definitions are needed, or intensional if the definitions must more fully express the 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.

Answer 1

As indicated by Feferman, the key distinction is between two sorts of arithmetical definitions of certain concepts (like "being the Gödel number of a theorem of a given theory"). Suppose I have some set $S$ of integers in mind and I propose a formal definition of it in some theory $T$, i.e., a formula $\phi(x)$ intended to "mean" that $x$ is a member of $s$. There are several ways to make this "intended" explicit. Probably the weakest is that, if $n$ is a natural number and $\bar n$ is a standard numeral for it, then $\phi(\bar n)$ should be provable in $T$ if and only if $n\in S$. Slightly stronger would be requiring that $T$ should prove $\phi(\bar n)$ when $n\in S$ and should refute $\phi(\bar n)$ when $n\notin S$. (My "slightly stronger" presupposes that $T$ is consistent.) Either of these would be seem to fit what Feferman calls "numerical correctness" of $\phi(x)$ as a definition of $S$. His concept of "expressing the notions" refers to stronger requirements on $\phi(x)$, but the exact nature of those requirements will depend on $S$ and on the particular application.

Suppose, for example, that $S$ is (in Gödel-numbered form) the set of theorems of some theory, and let me save TeX-coding by identifying formulas with their Gödel numbers. Then if $S$ contains both the formula $a$ and the implication $a\to b$, then it will also contain $b$; i.e., it is closed under modus ponens. One might want (or need) this property of $S$ to be provable in $T$ under the definition $\phi$, i.e., one might require that $T$ proves the general statement $$ \forall x\forall y((\phi(x)\land\phi(I(x,y)))\to\phi(y)), $$ where $I$ refers to a definition of implication via Gödel numbering. This property and similar ones may be needed in order to formalize in $T$ certain arguments (even trivial arguments) about provability. The need for such properties, going beyond numerical correctness, is what makes an argument intensional in Feferman's classification.