5

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}$.

goblin GONE
  • 67,744

2 Answers2

4

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.

Luca Bressan
  • 6,845
  • Are you sure? According to wikipedia we have that: "Abstractly, a type constructor is an $n$-ary type operator taking as argument zero or more types, and returning another type." Not that wikipedia is super-reliable or anything, but it sounds to me like all the types already exist in some sense. Granted there may be a subtlety here that I'm missing. – goblin GONE Sep 11 '13 at 18:17
  • 1
    Well, you can formalize type theory inside a possibly non-constructive set theory, but this is not what we want to do. The same thing could be said also for category theory, for example. The only type constructors that "exist" are those we have used in the rules that define the types we have declared. – Luca Bressan Sep 11 '13 at 18:22
  • Not that I'm arguing or anything, but that doesn't really "feel" dynamic to me. In particular, if $X$ and $Y$ are types, and I can immediately refer to the elements of $X \times Y$ without constructing anything, then it feels like the entity $X \times Y$ already existed before I ever made reference to it. To make it dynamic, you'd have to use "Let" statements. As in: let $\Pi$ instantiate $X \times Y$. Then for all $z \in \Pi$ we have $\Pi_X(z) \in X$. – goblin GONE Sep 11 '13 at 18:27
  • 1
    You can't immediately refer to the elements of $X \times Y$. First you have to say how these elements are formed, i.e. give a introduction rule for the type $X \times Y$. Then, if you have elements $x \in X$ and $y \in Y$, you can say that $\langle x , y \rangle \in X \times Y$. But the rules of the type must be declared first. – Luca Bressan Sep 11 '13 at 18:54
  • Fair enough! $!,$ – goblin GONE Sep 11 '13 at 18:58
  • Okay, this is totally cool. But how would you create a new real number system? I'm worried that the answer is very different to the classical answer (say, by Dedekind cuts, or by Cauchy sequences) since the goals of constructive mathematics don't always coincide with those of the mathematics that I know and love. – goblin GONE Sep 13 '13 at 20:17
  • Indeed the answer is different. One can construct the so called computable numbers: they form a real closed field, i.e. they satisfy the same first-order properties of real numbers – but not all properties. Some results about real numbers will not be true anymore, other propositions may be true while they were not for "classical" real numbers. Of course, if your view of mathematics is classical as in Platonist, your original question doesn't really make sense :) – Luca Bressan Sep 13 '13 at 20:27
  • Oh I'm no Platonist. I'm not even sure that arithmetical sentences above $\Pi_1$ have objective truthvalues. I guess you could say I value convenience and simplicity. And since classical mathematics is very very symmetrical and convenient (I mean, have you tried comparing classical first-order logic to first-order intuitionistic logic? In terms of simplicity, there's simply no comparison), hence my interest in non-constructive, or "classical" mathematics. However, classical mathematics has its inconveniences arising from the inability to construct new entities. Hence the original question! – goblin GONE Sep 13 '13 at 20:39
  • Anyway, it sounds like I should learn about type theory. Perhaps I'll be able to extract the "extensibility" aspect while bypassing the "constructibility" aspect somehow. – goblin GONE Sep 13 '13 at 20:41
  • Well, I guess that if you work in dependent type theory, you can add the Principle of Excluded Middle as an axiom, by declaring that there is an element of type $\prod X., (X \lor \neg X)$. I'm not sure what would be the consequences of this assumption for the things you want to do, though. – Luca Bressan Sep 13 '13 at 21:02
  • Luca, I have heard that types are terms in Martin-Lof, thus we can meaningfully ask the question: "Are types $X$ and $Y$ equal?" However, you seem to be saying that in (a trivially extended) simply typed lambda calculus, types are never equal, unless they look equal. Have I understood correctly? – goblin GONE Sep 14 '13 at 06:05
  • In some sense, yes. $\lambda$-calculus can be endowed with different notions of equality, but the most natural one is syntactic equivalence, denoted by $\equiv$ (which usually includes also $\alpha$-conversion, e.g. $\lambda x. x \equiv \lambda y. y$). Therefore it's natural to consider syntactic equivalence for types as well: there's no other canonical notion of equality. On the contrary, Martin-Löf's type theory can deal "natively" with many different equalities. I suggest you look at G. Sambin's notes "Intuitionistic Type Theory" to see what I mean; you can find them online. – Luca Bressan Sep 14 '13 at 07:33
  • Thanks, I'm reading them as we speak ! – goblin GONE Sep 14 '13 at 07:59
  • Hey, is there a type theory where the following general pattern of reasoning can be formalized? Let $n$ denote a fixed but arbitrary element of $\mathbb{N}.$ Now replace $n$ with $n+3$. Now square it. Therefore $n \geq 9$. (This example is interesting to me because we're actually changing the value of $n$). – goblin GONE Oct 13 '13 at 18:43
3

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.

Neil Barton
  • 1,037
  • 5
  • 13
  • That Linnebo and Studd stuff looks promising. A big +1 for those references. As for IZF and CZF, I don't think they're "constructive" in the sense that I was meaning in the question. You're still defining $\mathbb{R}$ by "searching" for a set, rather than creating it out of thin air, so to speak. – goblin GONE Sep 12 '13 at 00:54
  • I do see your point; the relevant axioms (subset collection etc), given the use of existential quantifiers, seem to be stating the existence of a set that is "out there". I think that most constructive views will want the following; "given such and such axioms for constructing sets, then what exists". This seems appropriately constructive, however, if you have literal ongoing construction of mathematical entities you are going to face problems from a foundational perspective; what was once false will soon be true! This sort of thing is around in the Philosophy literature. – Neil Barton Sep 12 '13 at 01:10
  • Yes that is a fair point. I think we'd have to distinguish between collections that are "already completed" (which we might call "sets" and whose constituents we might call "elements") as compared to collections that are "constantly in the process of being completed" (which, we might call "classes" and whose constituents we might call "objects", in deference to the lingo of object-oriented programming). Furthermore, we'd want certain properties of classes (e.g. their cardinality) to remain "hidden," so that the truthvalues of sentences aren't changing. – goblin GONE Sep 12 '13 at 10:53
  • Yes, this sounds very like a constructive interpretation of what Linnebo and Studd say. Certainly for Linnebo, proper classes are `intensional' notions; they are able to change members according to evaluation at different possible worlds of the cumulative hierarchy. (though I should add that Linnebo is keen not to give a constructive interpretation to his modal operators for philosophical reasons, or at least not have such an interpretation forced upon him). – Neil Barton Sep 14 '13 at 02:28
  • Like I said, it looks like a promising lead. Its not quite what I'm looking for though. See, the forever-in-construction world of Linnebo and Studd "lives" in well-ordered time. In particular, linear time. This means we cannot actually choose how to build the universe; thus, in some sense, their world is already built. What I really want is time that can branch like a poset. That way, the writer can actually choose which branch to go down. – goblin GONE Sep 14 '13 at 05:37