The finite axiomatizability of $\mathsf{KP}$ revisited

Question

The related question is:

Is Kripke Platek theory finitely axiomatizable?

My questions are as follows:

Let $\mathsf{KP}$ be the Kripke Platek set theory with only $\Pi_1$-foundation, and without the axiom of infinity.

Let $\mathsf{KPI}=\mathsf{KP}+{}$ the axiom of infinity.

On page 165, line 17 of Mathias's paper The strength of Mac Lane set theory, it is claimed that $\mathsf{KPI}$ is finitely axiomatizable, and on page 47 of his handwritten notes Notes on set theory (see T215 there), this fact is proved.

Is $\mathsf{KP}$ also finitely axiomatizable?

In fact, I do not even know the following things about $\mathsf{KP}$:

1, Is "$x$ is finite" $\Delta_1^{\mathsf{KP}}$ ?

2, Can $\mathsf{KP}$ prove that "for all finite $x$, the power set of $x$ exists"?

3, Can $\mathsf{KP}$ prove that "if there is an infinite set, then $\omega$ exists"?

4, Can $\mathsf{KP}$ prove that "for all $x$, if $\mathrm{rank}(x)<\omega$, then $x$ is finite"?

5, In $\mathsf{KP}$, do we have the truth definition as in $\mathsf{KPI}$?

where "$x\in\omega$" is defined to be "$x$ and all its members are 0 or successor ordinals", and "$x$ is finite" is defined to be "$\exists n\in\omega\exists f($ $f$ is a bijection from $n$ onto $x$ $)$"; the rank function is defined in $\mathsf{KP}$ by the "definition by recursion" theorem.

My another related question about the finite axiomatizability of $\mathsf{KPI}$ is:

If we extend $\mathsf{KPI}$ to contain also $\Sigma_n$-separation, $\Sigma_n$-collection, and $\Pi_n$-foundation, is this extension still finitely axiomatizable?

---

Edit: The answer to the question 2 is affirmative, as shown in Proposition 2.13 on page 161 of Mathias's paper Weak Systems of Gandy, Jensen and Devlin.

Answer 1

I think the answer to questions 1,3,4 is affirmative. The sketch is as follows (maybe not right):

4 implies 3, and if 3 holds, then we have that

$x$ is infinite${}\leftrightarrow{}\exists y(y=\omega\wedge\forall z\in y\exists f(f\text{ is an injection from $z$ into $x$}))$

which is a $\Sigma_1$ formula. Hence 3 implies 1.

We need only to show 4 in $\mathsf{KP}$.

In $\mathsf{KP}$, we can define the transitive closure $\mathrm{TC}(x)$ of any set $x$, and we can prove that $y=\mathrm{TC}(x)$ is $\Delta_1^\mathsf{KP}$ (see D088, T089, T109 and T110 of Mathias's handwritten notes). By $\Sigma_1$-induction on $x$ we can prove that $\mathrm{rank}(x)=\mathrm{rank}(\mathrm{TC}(x))$. Let $x$ be a set such that $\mathrm{rank}(x)<\omega$. We need only to show that $\mathrm{TC}(x)$ is finite. Let $y=\mathrm{TC}(x)$. Let $h=\mathrm{rank}\upharpoonright y$. Then $h$ is a function from $y$ into a natural number. We can prove that for all $n\in\omega$, $\{z\in y\mid h(z)=n\}\subseteq\mathscr{P}(\{z\in y\mid h(z)<n\})$. Since "$n\in\omega\to\exists u(u=\{z\in y\mid h(z)<n\}\text{ and $u$ is finite})$" is a $\Sigma_1$ formula, by $\Sigma_1$-induction on $n$, we can prove that $\forall n\in\omega\exists u(u=\{z\in y\mid h(z)<n\}\text{ and $u$ is finite})$ (use also that "the power set of any finite set exists and is also finite", see Mathias's paper mentioned in the Edit). Since the range of $h$ is included in a natural number, $y$ is finite.