Are there any foundations in which the universe itself gets dynamically extended?

In the foundations I'm familiar with, you don't ever "create" anything.

Take ZFC for example. If we need the real numbers, we search in our static universe for a set $\mathbb{R}$ of the correct cardinality such that its not-too-difficult to define some other sets, namely

$$+,\cdot,0,1,\leq$$

such that its not too difficult to show that $\mathcal{R} = (\mathbb{R},+,\cdot,0,1,\leq)$ satisfies the axioms of a complete ordered field. So in some sense, we're "searching" in a static universe, as opposed to "creating" in a dynamic universe. The only things that are changing are our definitions.

Are there any foundations in which the universe itself gets dynamically extended?

I'm not certain how this would work exactly, but perhaps something like this. Instead of having axioms postulating the existence of different entities (an empty set, a powerset etc.), we might instead have methods for constructing new entities (a new empty set, a new powerset, etc.).

Edit. Here's some more details about what I'm looking for.

Consider the following statement.

There exists $x$ such that for all $y$ we have $x \neq y$.

Clearly, its bogus. Now consider the following variant.

We can always construct a new entity $x$ such that for all previously existing $y$ we have $x \neq y$.

It would be nice if the above statement were true.

More ambitiously:

For all models $\mathcal{R}$ over a signature $\sigma$, we can construct a new (abstract) model $\mathcal{R}'$ over $\sigma$ equipped with an isomorphism $f : \mathcal{R}' \rightarrow \mathcal{R}$.

Solution 1:

This is exactly what happens in the constructive foundations that are based on a computational view of mathematics, for example Martin-Löf's type theory (both the extensional and the intensional one).

In these foundations, mathematical entities must be computable, so every set must be inductively generated. This means that until we don't say how the elements of a certain set are formed, it doesn't make sense to say that the set itself "exists".

I'll give you an example to explain why (or how) type theory can satisfy your request. I won't use Martin-Löf's type theory because in that system the rules are very long since they deal with equality in detail; what follows is based on (a trivial extension of) simply typed $\lambda$-calculus. I hope you're familiar with Gentzen-style sequent calculus: if you're not, I'll explain the notation.

Suppose that your initial universe contains only one basic set, namely, a set $B$ with two elements. The only other construction available is that of function sets, because there's nothing you can actually do without it since all computations come from abstraction and application. This means that your universe is presented through the following list of rules:

$B$-formation: this rule declares that we can talk about $B$ as a set. $$\vdash B \;\text{set} $$ $B$-introduction: this rule tells how canonical elements of $B$ are formed. $$\vdash \mathsf{0} \in B \quad \vdash \mathsf{1} \in B$$ $B$-elimination: this rule tells what information we can get from knowing that something is an element of $B$. $$\frac{\Gamma \vdash c \in B \qquad \Gamma \vdash d \in \alpha \qquad \Gamma \vdash e \in \alpha}{\Gamma \vdash \mathsf{R}_B (c, d, e) \in \alpha}$$ with the reduction rules that tell us what to do when $c$ is a canonical element: $$\mathsf{R}_B (\mathsf{0}, d, e) \rightsquigarrow d \qquad \mathsf{R}_B (\mathsf{1}, d, e) \rightsquigarrow e$$

Now, we could start enumerating all the different sets within our universe. They are: $$B,\quad B \to B,\quad B \to (B \to B),\quad (B \to B) \to B, \quad \dotsc$$

The notion of element equality, in this system, is supposed to correspond to the smallest equivalence relation containing reduction. The notion of set equality, instead, is purely syntactical. We don't have any extensionality rule here. This means that we can add to our list of rules some new rules for a set $C$, for example a set with three elements, and it will be different from $B$ – but even if the rules for $C$ had exactly the same form as those of $B$, in a way that would make $C$ another set with two elements, the constructors would be different. We could call them $\mathsf{0}'$ and $\mathsf{1}'$, or $\mathsf{a}$ and $\mathsf{b}$. These are all just symbols, they're not to be intended as variables: the fact that $B$ and $C$ are different comes from the fact that B and C are different letters!

I hope this clarifies my initial answer.

Solution 2:

In addition to Luca's nice suggestion, one might consider other constructive foundations such as $IZF$ (abbreviating "Intuitionistic Zermelo Fraenkel") or the more explicitly constructive $CZF$ (abbreviating "Constructive Zermelo Fraenkel") set theories.

$IZF$ incorporates the notion of `construction' via the use of an intuitionistic metatheory, whereas $CZF$ in addition to an intuitionistic metatheory has the following properties:

(i) Separation is restricted to bounded formulae.

(ii) Replacement is replaced by the following `Strong Collection Scheme':

$\forall a [\forall x \in a \exists y (\phi (x, y) \rightarrow \exists b (\forall x \in a \exists y \in b \phi (x, y) \wedge \forall y \in b \exists x \in a \phi (x, y))]$

(iii) Power Set is replaced by the following `Subset Collection Scheme' which allows us to construct the set of all definable subsets:

$\forall a \forall b \exists c \forall u [ \forall x \in a \exists y \in b \phi (x, y, u) \rightarrow \exists d \in x (\forall x \in a \exists y \in d \phi (x, y, u) \wedge \forall y \in d \exists x \in a \phi (x, y, y))]$

Where $c$ is not free in $\phi (x, y, u)$

Further, there is $KP$ (for Kripke-Platek set theory). This theory (though the metatheory is classical), restricts the subset collection scheme to $\Delta_0$ formulae (and so respects the idea of `constructing' subsets out of absolute formulae).

In addition one might consider the Univalent Foundations Project, which brings together some of the type-theoretic considerations mentioned by Luca with homotopy theory to provide a foundation that is more constructive in flavour. Unfortunately, I don't really have the knowledge to say any more than Luca; but should you be interested there is a collaborative book available for free:

http://homotopytypetheory.org/

Further, there is a completely different approach that might be of interest to you. Recent work by Linnebo and Studd has yielded modal set theories, where the notion of building up the layers of the cumulative hierarchy is treated more seriously. We add modal notions $\Box$ and $\Diamond$ which are to be read as "no matter how far the hierarchy is continued it will be the case that" and "the hierarchy can be continued so that". While their aim is not constructive, it certainly could be appropriated by a constructivist, where each $V_{\alpha}$ is thought of as being added in a constructive process.

Details of $IZF$ and $CZF$ can be found here:

http://plato.stanford.edu/entries/set-theory-constructive/index.html#1.3

http://plato.stanford.edu/entries/set-theory-constructive/axioms-CZF-IZF.html

A short discussion of $KP$ is available here:

http://plato.stanford.edu/entries/settheory-alternative/#ConSetThe

The Homotopy Type Theory book is available from:

http://homotopytypetheory.org/

Linnebo and Studd's work is contained in the following papers:

Studd, J. P. (2012). The Iterative Conception of Set: a (Bi-)Modal Axiomatisation. Journal of Philosophical Logic :1-29.

Linnebo, Øystein (2010). Pluralities and Sets. Journal of Philosophy 107 (3):144-164.

Linnebo, Øystein (2013). The Potential Hierarchy Of Sets. The Review of Symbolic Logic, 6, pp 205-228. doi:10.1017/S1755020313000014.