Does the degree of impredicativity always matter in type theory?

86 Views Asked by At

My question here is actually about whether different degress of impredicativity matter? To show that, lets confine ourselves with the following predicative formalism.

Language: multi-sorted first order logic

Primitives: $0, S, =, \in$

Syntatical restrictions include: $x_i \in y_{i+1}; x_i=y_i, S(x_0) $.

For convenience if a variable is written in un-indexed manner, then it's of sort zero; so $x$ is in reality $x_0$. The symbol $\mathbb N$ shall be left unindexed, though it is an object of sort 1.

Axioms:

Extensionality: $\forall x_{i+1} \, \forall y_{i+1} \, (\forall z_i (z_i \in x_{i+1} \iff z_i \in y_{i+1}) \to \\x_{i+1}=y_{i+1})$

Comprehension: $\exists x_{i+1} \forall y_i (y_i \in x_{i+1} \iff \phi(y_i))$

Define: $\mathbb N= \{x: x=x\}$

Naturals: $0 \in \mathbb N \\ x \in \mathbb N \to S(x) \in \mathbb N \\ S(x)\neq 0 \\ S(x)=S(y) \to x=y $

Induction: $\forall X_1: 0 \in X_1 \land \forall n (n \in X_1 \to n+1 \in X_1) \to \mathbb N \subseteq X_1 $

Now $\phi(y_i)$ is predicative ($0$-impredicative) if and only if the maximal sort a variable occurring in it can take is $i$.

$\phi(y_i)$ is $n$-impredicative if and only if the maximal sort a variable occurring in it can take is $i+n$.

Call the the above theory with the restriction of comprehension to $n$-impredicative formulas as: $\sf TTP_n$

Now we know from $\sf NF$ that $\sf NFP$ is weaker than $\sf PA$, while $\sf NFI$ is as strong as second order arithmetic, while if we allow $2$-impredicativity then we get full $\sf NF$, and further increase of degree of impredicativity is idle, so we still get just $\sf NF$. [see here and here]

Is it the same situation with the above type theory? In other words, is $\sf TTP_2$ equal in strenght to $\sf TTP_{n+2} $ ?

1

There are 1 best solutions below

0
On BEST ANSWER

Yes. Predicative type theory plus the axiom of union, which looks up only one type, is full impredicative type theory. The situation in type theory is the same as in NF.