Is Axiom IV of System P in Godel 1931 really the axiom of reducibility?

Question

System P in Gödel's original paper "On Formally Undecidable Propositions of Principia Mathematica and Related Systems" contains the following axiom schema:

IV. Every formula derived from the schema 1. $(∃u)( ∀v (u(v) ≡ f))$ on substituting for v or u any variables of types $n$ or $n + 1$ respectively, and for f a formula which does not contain u free. This axiom represents the axiom of reducibility (the axiom of comprehension of set theory).

I find the description of this as representing the axiom of reducibility puzzling. Firstly, the schema does not reflect my understanding of what the axiom of reducibility is (all properties and relations are co-extensive with first order properties and relations). Secondly, my understanding is that system $P$ is a simple rather than ramified type theory and so for it axioms of reducibility would be, at best, superfluous.

Why did Gödel state that it represented the axiom of reducibility?

Answer 1

See B.Russell, Mathematical logic as based on the theory of types (1908) for the original discussion of the axiom:

[ page 168 ] we will call this assumption the axiom of classes, or the axiom of reducibility.

The *12.1 axiom of Principia says that for any propositional function $\varphi$ there is a predicative propositional function that is coextensive with it:

$(\exists f) \ (\forall x) \ (\varphi x \equiv f ! x)$.

According to Principia, a "class" is a mere "façon de parler", a "logical fiction":

The characteristics of a class are that it consists of all the terms satisfying some propositional function, so that every propositional function determines a class, and two functions which are formally equivalent determine the same class [...] The incomplete symbols which take the place of classes serve the purpose of technically providing something identical in the case of two functions having the same extension.

The definition *20.1 intoduces contextually the expression "the class of $\psi$s is $f$" as meaning that there is a predicative function $\varphi !$ that is formally equivalent to $\psi$ and $\varphi$ is $f$.

And thus (see *20.3): $x \in \hat z(\psi z)$ if and only if there is a predicate expression $\varphi !$ such that $\varphi ! a$ and $\forall x(\psi x \equiv \varphi x)$.

By the axiom of reducibility, therefore, all propositional functions (i.e. open formulas), predicative or not, determine classes.

If we "cut off" the ramification, what is left is a hierarchy based on individuals and propositional functions of any order, and a predicative function is a propositional function $\varphi x$ whose order is the next above that of $x$.

Intuitively, if we "map" the hierarchy of orders (without ramification) on the cumulative hierarchy of sets what we get is that every open formula whose variables range over individuals is coextensive with a propositional function of the order next above that of the individuals, i.e. a class of individuals,

And so on for each "level" of the hierarchy.

But this is nothing different from Gödel's comprehension axiom :

for every formula $\alpha$ : $(\exists u)( \forall v \ (u(v) \equiv \alpha))$ [for $v$ of type $n$ and $u$ of type $n+1$].

---

It is a "long road" starting from Principles of Mathematics (1903), §84:

It only remains to say a few words concerning the derivation of classes from propositional functions. When we consider the $x$’s such that $\phi x$, where $\phi x$ is a propositional function, [...] we are considering, among all the propositions of the type $\phi x$, those that are true: the corresponding values of $x$ give the class defined by the function $\phi x$. It must be held, I think, that every propositional function which is not null defines a class, which is denoted by “$x$’s such that $\phi x$”.

The impact of the discovery of "the" contradiciton on the comprehension principle was deep:

But it may be doubted — ndeed the contradiction with which I ended the preceding chapter gives reason for doubting — whether there is always a defining predicate of such classes.

With the development of the Type Theory the self-applying construction $\phi (\phi)$ was avoided, but the need for comprehension is unavoidable; it was salvaged with the principle that every predicative function defines a class and with reducibility.