The Sigma_1-definable universal finite sequence

TL;DR

This paper introduces a $oldsymbol{ extSigma_1}$-definable universal finite sequence in set theory, demonstrating its properties and implications for end-extension potentialism and modal logic, with new proof techniques and principles.

Contribution

It defines a $oldsymbol{ extSigma_1}$-definable universal finite sequence and proves its properties, advancing understanding of end-extension potentialism and modal logic in set theory.

Findings

The sequence is $oldsymbol{ extSigma_1}$-definable and provably finite.

The sequence is empty in transitive models.

Models can be extended to satisfy the end-extensional maximality principle.

Abstract

We introduce the $\Sigma_1$-definable universal finite sequence and prove that it exhibits the universal extension property amongst the countable models of set theory under end-extension. That is, (i) the sequence is $\Sigma_1$-definable and provably finite; (ii) the sequence is empty in transitive models; and (iii) if $M$ is a countable model of set theory in which the sequence is $s$ and $t$ is any finite extension of $s$ in this model, then there is an end-extension of $M$ to a model in which the sequence is $t$. Our proof method grows out of a new infinitary-logic-free proof of the Barwise extension theorem, by which any countable model of set theory is end-extended to a model of $V=L$ or indeed any theory true in a suitable submodel of the original model. The main theorem settles the modal logic of end-extensional potentialism, showing that the potentialist validities of the models of set theory under end-extensions are exactly the assertions of S4. Finally, we introduce the end-extensional maximality principle, which asserts that every possibly necessary sentence is already true, and show that every countable model extends to a model satisfying it.