The theory of hereditarily bounded sets

TL;DR

This paper proves that for any fixed natural number k, the structure of hereditarily bounded sets of size at most k is decidable, provides a complete axiomatization, and analyzes its complexity, contrasting it with hereditarily finite sets.

Contribution

It introduces a complete axiomatization and complexity bounds for the theory of hereditarily bounded sets of size at most k, a novel result in set theory.

Findings

The theory of hereditarily bounded sets of size at most k is decidable.

A complete axiomatization and quantifier elimination are provided.

The computational complexity of the theory is tightly bounded.

Abstract

We show that for any $k\in\omega$, the structure $(H_k,\in)$ of sets that are hereditarily of size at most $k$ is decidable. We provide a transparent complete axiomatization of its theory, a quantifier elimination result, and tight bounds on its computational complexity. This stands in stark contrast to the structure $V_\omega=\bigcup_k H_k$ of hereditarily finite sets, which is well known to be bi-interpretable with the standard model of arithmetic $(\mathbb N,+,\cdot)$.