A weak set theory that proves its own consistency

In the paper we introduce a weak set theory $\mathsf{H}_{<\omega}$ . A formalization of arithmetic on finite von Neumann ordinals gives an embedding of arithmetical language into this theory. We show that $\mathsf{H}_{<\omega}$ proves a natural arithmetization of its own Hilbert-style consistency. Unlike some previous examples of theories proving their own consistency, $\mathsf{H}_{<\omega}$ appears to be sufficiently natural. The theory $\mathsf{H}_{<\omega}$ is infinitely axiomatizable and proves existence of all individual hereditarily finite sets, but at the same time all its finite subtheories have finite models. Therefore, our example avoids the strong version of G\"odel second incompleteness theorem (due to Pudl\'ak) that asserts that no consistent a theory interpreting Robinson's arithmetic $\mathsf{Q}$ proves its own consistency. To show that $\mathsf{H}_{<\omega}$ proves its own consistency we establish a conservation result connecting Kalmar elementary arithmetic $\mathsf{EA}$ and $\mathsf{H}_{<\omega}$. We also consider the version of $\mathsf{H}_{<\omega}$ over higher order logic denoted $\mathsf{H}^{\omega}_{<\omega}$. It has the same non-G\"odelian property as $\mathsf{H}_{<\omega}$ but happens to be more attractive from a technical point of view. In particular, we show that $\mathsf{H}^{\omega}_{<\omega}$ proves a $\Pi_1$ sentence $\varphi$ of the predicate-only version of arithmetical language iff $\mathsf{EA}$ proves that $\varphi$ holds on the superexponential cut.