Formalizing set theory in weak logics, searching for the weakest logic with G\"odel's incompleteness property

TL;DR

This paper demonstrates that set theory can be formalized within a very weak logical system, equivalent to certain algebraic and modal logics, which also exhibit G"odel's incompleteness property, thus identifying the weakest logic with this property.

Contribution

It formalizes set theory in a weak logic equivalent to Boolean algebra with closure operators and multi-modal logic, improving previous results on formalizing set theory without variables.

Findings

Set theory can be formalized in a weak logic equivalent to Boolean algebras with closure operators.

The logic [S5,S5,S5] has G"odel's incompleteness property.

Finitely generated free Df_3's are not atomic.

Abstract

We show that first-order logic can be translated into a very simple and weak logic, and thus set theory can be formalized in this weak logic. This weak logical system is equivalent to the equational theory of Boolean algebras with three commuting complemented closure operators, i.e., that of diagonal-free 3-dimensional cylindric algebras (Df_3's). Equivalently, set theory can be formulated in propositional logic with 3 commuting S5 modalities (i.e., in the multi-modal logic [S5,S5,S5]). There are many consequences, e.g., free finitely generated Df_3's are not atomic and [S5,S5,S5] has G\"odel's incompleteness property. The results reported here are strong improvements of the main result of the book: Tarski, A. and Givant, S. R., Formalizing Set Theory without variables, AMS, 1987.