understanding the reducibility axiom

Question

I am reading an english translation of Gödel's paper of the Incompleteness Theorem http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf

In there is mentionned the so called "reducibility axiom" (the comprehension axiom of set theory). I understand the comprehension axiom but i can't relate it to the description of the reducibility axiom that is described.

Here is how it is explained :

The variables of type 1 are natural numbers, elements of $\mathbb{N}$

The variables of type 2 are sets of natural numbers, or subsets of $\mathbb{N}$

The variables of type 3 are sets of sets of natural numbers, or sets of subsets of $\mathbb{N}$

And so on.

Let u be a "type n+1" variable.

Let v be a "type n" variable.

Every formula obtained from the schema

$\exists u \forall v \ (u(v) \iff a)$

"by inserting for v and u any variables of type n and n + 1 respectively and for a a formula that has no free occurrence of u. This axiom takes the place of the reducibility axiom (the comprehension axiom of set theory)."

I am not sure I understand, is it that we can replace or substitute a n-th order formula by a strictly equivalent first-order formula ?

Can someone help me understand this reducibility axiom.

Thank you.

Answer 1

The Axiom of reducibility was an axiom specific of W&R's system developed into Pincipia Mathematica : the so-called Ramified Type Theory.

You can see : Bernard Linsky, Was the Axiom of Reducibility a Principle of Logic?.

---

See : Alfred North Whitehead & Bertrand Russell, Principia Mathematica to *56 (2nd ed - 1927), page 56 :

The axiom of reducibility is the assumption that, given any function $\phi \hat x$, there is a formally equivalent predicative function, i.e. there is a predicative function [$\psi !$] which is true when $\phi x$ is true and false when $\phi x$ is false. In symbols, the axiom is:

$$(\exists \psi)(\forall x)(\phi x \equiv \psi ! x)$$

where [page 53] :

We will define a function of one variable as predicative when it is of the next order above that of its argument, i.e. of the lowest order compatible with its having that argument.