43
$\begingroup$

I am wondering if there is a foundation of mathematics where not sets or "set-like objects" (such as objects of a suitable topos as in ETCS) are the primitive notion, but rather lists. These lists (aka sequences, tuples, ...) should be mathematical objects denoted as $[a_1,a_2,\dotsc]$ with an information in which position an element $a_i$ occurs, and of course the elements may appear multiple times. The length of a list does not have to be finite, but if it helps to answer the question feel free to make this assumption, thus answering the question in finitism. Generally, they should be indexed by (an equivalent of) ordinal numbers.

The question is partially motivated by the observation that in many programming languages lists are actually more common and also the building blocks of more complex objects. Here, sets are often seen as derived from lists or special lists, namely lists in which the order does not matter and in which no element appears twice. In the set-theoretic foundations I am aware of, it is vice versa: lists are special sets. So my question is basically if we can turn this paradigm around and see lists as the primary notion and build mathematics around it?

Maybe I did not use the right search terms, and surely I am not an expert in foundation of mathematics, but I cannot find any such approach. And I find it hard to come up with something on my own, because every axiom for lists I can think of involves set-like objects in the end. It feels like set theory (and category theory of course, but here we also have sets of objects etc. so this does not get us out of the paradigm) permeates every thought.

For instance, what are the indices of the list elements, or how do they behave, when we are not allowed to talk about sets and hence of ordinal numbers? How can we even formulate that each list and every position yields an element without talking about maps? The "cheap" way out is to define sets as special lists as above and write down the ZFC axioms in terms of these special lists - but of course it would be much more satisfactory to develop something which does not just use ZFC as an intermediate step.

I am aware that the whole idea might not work at all. In this case, an answer is also appreciated explaining why it does not work.


Just to give Andreas Blass' comment extra visibility: Oliver Deiser has developed such a theory, called Axiomatic List Theory, in his Habilitationsschrift (in German), an excerpt of which has been published as well (in English).

  • Deiser, Orte, Listen und Aggregate, Habilitationsschrift, Link
  • Deiser, An axiomatic theory of well-orderings, The Review of Symbolic Logic, 4(2), 186-204, Link
$\endgroup$
12
  • 3
    $\begingroup$ When developing finitistic mathematics in PA or other theories of arithmetic, (finite) sets are often coded as lists, which are in turn typically coded as numbers. But (at least in the parts of the literature I know), this is typically viewed as using arithmetic as a foundation for the finitistic fragment of mathematics, not as aiming to be a foundation for all of mathematics; and in the end the primitive objects are usually numbers, not lists. So I guess this isn’t quite what you want. $\endgroup$ Commented Oct 17, 2023 at 20:56
  • 21
    $\begingroup$ .Oliver Deiser has worked out two versions of foundations, one based on lists and one on multisets. This is in his book "Orte, Listen, Aggregate" (and his Habilitationsschrift with the same title). $\endgroup$ Commented Oct 17, 2023 at 21:14
  • 4
    $\begingroup$ @AndreasBlass By reading a few pages, this seems to be the perfect answer for my question! (You can also post it as an answer, I will accept it.) What surprises me is that the book was written in 2009. Not in 1909. It seems to be such a, well, fundamental idea. (Also, that it is written in German. Well, good for me, but not for most mathematicians, I would say.) I will read it now :-), thanks a lot! $\endgroup$ Commented Oct 17, 2023 at 21:33
  • 4
    $\begingroup$ A fun side note: An ordinal-indexed list of Booleans is equivalent to a surreal number, just like how a list of digits represent a binary number. $\endgroup$
    – Trebor
    Commented Oct 18, 2023 at 2:18
  • 4
    $\begingroup$ @Trebor One important difference, however, is that the theory of the surreal field is decidable, since it is the theory of a real-closed field, whereas the theory of arithmetic is not. One cannot use the surreal field as a foundational system, because it is decidable. We cannot even encode finite combinatorics, Turing machines, etc into the surreals. $\endgroup$ Commented Oct 18, 2023 at 11:45

4 Answers 4

31
$\begingroup$

Andreas Blass has already provided a good reference in the literature, but unfortunately I cannot read German, so I've had to make do with writing my own answer.

As you observed, you're clearly not going to get away from the abstract concept of 'collections of objects,' since it's pretty fundamental in mathematics, but I would argue that ordinals are not an intrinsically set-theoretic notion any more than, say, well-founded trees are. This isn't to say that these ideas aren't important in set theory, but I would say that if one were really committed to formalizing mathematics 'without sets,' eschewing ordinals or well-founded trees because of their applicability in set theory wouldn't really be a good idea.

It is entirely possible to give a relatively self-contained theory of ordinal-indexed lists of ordinals that is equiconsistent with $\mathsf{ZFC}$. I will sketch such a theory. Furthermore, I would argue that this theory is no more 'set-theoretic' than, say, second-order arithmetic formalized in terms of numbers and sequences of numbers.


The theory has two sorts $\def\Ord{\mathrm{Ord}}\Ord$ and $\def\Lst{\mathrm{Lst}}\Lst$ (for ordinals and lists of ordinals, respectively). I'll use the convention that lowercase Greek letters represent ordinals and lowercase Latin letters represent lists.

As primitive symbols, we have a constant $0$ in $\Ord$, a binary relation $\leq$ on $\Ord$, and two functions $(x,\alpha) \mapsto x_\alpha : \Lst \times \Ord \to \Ord$ and $\ell : \Lst \to \Ord$. $x_\alpha$ is meant to be the $\alpha$th element of the list $x$ and $\ell(x)$ is meant to be the length of the list $x$. We'll use the convention that if $\alpha \geq \ell(x)$, then $x_\alpha = 0$.

We have the following axioms and axiom schemas.

  • Linear order with least element: $\leq$ is a linear order on $\Ord$ with least element $0$.

  • List extensionality: $x = y$ if and only if $\ell(x) = \ell(y)$ and for all $\alpha < \ell(x)$, $x_\alpha = y_\alpha$.

  • List padding: For any $\alpha \geq \ell(x)$, $x_\alpha = 0$.

  • Successor: For every $\alpha$, there is a $\beta > \alpha$.

  • Supremum: For every $x$, there is an $\alpha$ such that $\alpha \geq x_\beta$ for all $\beta$.

  • Infinity (existence of a limit ordinal): There is an $\alpha > 0$ such that for all $\beta < \alpha$, there exists a $\gamma < \alpha$ with $\beta < \gamma$.

  • Well-ordering: For any formula $\varphi(\alpha,\bar{\beta},\bar{x})$ and parameters $\bar{\beta}$ and $\bar{x}$, if there is an $\alpha$ such that $\varphi(\alpha,\bar{\beta},\bar{x})$ holds, then there is a least such $\alpha$.

  • List comprehension: For any formula $\varphi(\alpha,\beta,\bar{\gamma},\bar{x})$, parameters $\bar{\gamma}$ and $\bar{x}$, and ordinal $\delta$, if $(\forall \alpha < \delta )\exists ! \beta \varphi(\alpha,\beta,\bar{\gamma},\bar{x})$, then there is a $y$ such that $\ell(y) = \delta$ and for each $\alpha < \delta$, $\varphi(\alpha,y_\alpha,\bar{\gamma},\bar{x})$ holds.

Given a list $x$ and an ordinal $\alpha$, write $x \ll \alpha$ to mean that $\ell(x) < \alpha$ and for all $\beta$, $x_\beta < \alpha$.

  • List bounding: For any formula $\varphi(x,\alpha,\bar{\beta},\bar{y})$, any parameters $\bar{\beta}$ and $\bar{y}$, and any ordinal $\gamma$, there is an ordinal $\delta$ such that for all lists $x \ll \gamma$, if there is an $\alpha$ such that $\varphi(x,\alpha,\bar{\beta},\bar{y})$ holds, then there is an $\varepsilon \leq \delta$ such that $\varphi(x,\varepsilon,\bar{\beta},\bar{y})$ holds.

These axioms are far from optimal (for instance we could combine successor and supremum by requiring that $\alpha > x_\beta$ for all $\beta$), but I think they're a reasonably well-motivated set of principles for capturing the notion of collections of ordinal-indexed lists of ordinals that are 'complete' (in roughly the same way that models of $\mathsf{ZF}$ are 'complete').

It's fairly immediate that $\mathsf{ZF}$ (and therefore $\mathsf{ZFC}$) interprets this theory by looking at the class of ordinals and functions $x : \alpha \to \Ord$. Conversely, to show that this theory interprets $\mathsf{ZFC}$, we need to roughly do the following:

  • Show that well-ordering and list comprehension allow you to perform transfinite induction.

  • Use this to show that Gödel's pairing function on ordinals is definable. (Specifically, show that we can uniformly build lists giving arbitrarily long initial segments of the projections of the pairing function.)

  • Define the notion of ordinal computation (with, e.g., ordinal Turing machines). Use some standard work in that area to show that we can interpret $\mathsf{KP} + {V=L}$ with some defined predicate membership predicate on $\Ord$.

  • Show that the interpreted copy of $L$ is closed under full replacement (by list comprehension and supremum), and show that it is closed under (internal) power set (by list bounding). Conclude that $L \models \mathsf{ZFC}$.

One thing to note is that this procedure will not produce a bi-interpretation with $\mathsf{ZFC}$. In order to get a bi-interpretation, we would need some axiom asserting that we can 'list' all of the lists $x\ll\alpha$ for any $\alpha$, but this axiom actually seems a lot less natural to me in this context than the others I've listed. (In particular, it has a far less canonical flavor, since it's literally a form of the axiom of choice, and it requires a moderately complicated defined notion like the pairing function to formalize.) The sketchiest one is of course list bounding, but in some sense that corresponds nicely to the semi-frequent opinion that the sketchiest axiom of $\mathsf{ZF}$ is power set.

$\endgroup$
2
  • 2
    $\begingroup$ Moreover, I actually suspect that this theory also isn't bi-interpretable with $\mathsf{ZF}$, but we'd need an expert on choiceless set theory to weigh in on that. $\endgroup$ Commented Oct 17, 2023 at 22:34
  • 7
    $\begingroup$ The theory TLO (transfinite lists of ordinals) you proposed is not bi-interpretable with ZF since ZF admits a model that has an automorphism of order 2 (by a classical result of Cohen), but no model of TLO has a nontrivial automorphism of finite order (any automorphism of finite order should be the identity on ordinals of the model, and this will imply via the Extensionality axiom for lists that the automorphism is also the identity on the lists of the model. I should also add that bi-interpretability of models preserves their automorphism groups. $\endgroup$
    – Ali Enayat
    Commented Oct 18, 2023 at 18:52
21
$\begingroup$

Peter Koepke and Martin Koerwien developed the theory of sets of ordinals as a foundation of mathematics, showing senses in which it is equivalent to ZFC as a foundation.

I view this as an answer to your question because a set of ordinals is essentially a transfinite binary sequence. So this is a foundation of mathematics built entirely on transfinite binary sequences, or lists as you described them. They show how to encode other mathematical objects into these lists and develop all the usual foundational theory.

$\endgroup$
5
  • $\begingroup$ In some pedantic sense the theory $\sf SO$ doesn't qualify for the OP specifications, since it does contain $\in$ among its primitives, even though this $\in$ is a flat kind of membership. But, I agree with you, that in essence a flat membership + ordered pairing would be essentially lists or sequences which is the essence of what the OP is speaking about. $\endgroup$ Commented Oct 18, 2023 at 18:40
  • $\begingroup$ If you think of sets of ordinals as sequences, then the $i\in x$ relation is just extracting the $i$th member of the list $x$. In SO, every ordinal is also a list, and so the theory is all about lists of lists of lists of lists, etc. $\endgroup$ Commented Oct 18, 2023 at 18:51
  • $\begingroup$ If "sets" of ordinals are sequences, and so those are the lists, then per $\sf SO$, none of those is an ordinal, then per this interpretation your statement that every ordinal is a list is violated. I think the proper way is to view lists in $\sf SO$ as set of ordinals that are pairs of ordinals. And still even an ordinal that is a pair of ordinals won't qualify as a list since it is not a set of ordinals. the $\in$ in $\sf SO$ cannot be viewed as extracting the $i$th member of a list. It is meant to denote flat membership, which the OP forbids. $\endgroup$ Commented Oct 18, 2023 at 19:35
  • 1
    $\begingroup$ I disagree. In SO the ordinals (or lists, whatever) are well-ordered in the theory, and so it is perfectly sensible to speak of the $i$th member of the list $x$, even when $i$ is itself a list. That is exactly the kind of thing one would want in a list-based foundations. $\endgroup$ Commented Oct 18, 2023 at 19:39
  • $\begingroup$ I know it can be done, but its not quite natural. SO discriminates between ordinals and sets of ordinals, you don't have an ordinal that is a set of ordinals. Its more natural to define "lists" as "sets of pairs of ordinals" and so they are sets of ordinals, and so by rules of SO they are NOT ordinals. If we define "lists" as ordinals, it won't be that natural, how you are going to define the $i$th item in them? It can be done of course, but not all that natural. $\endgroup$ Commented Oct 18, 2023 at 20:49
11
$\begingroup$

The OP allowed for a finitist answer. Here's an ultrafinitist one.

As noted in the question lists are just sequences. But sequences are just unary functions. So consider a first-order theory with two sorts, numbers and unary functions, with equality on the first sort. Represent the first sort by a small letter and the second sort by a capital letter. There is one constant, the first-sort $0$, and one 2-ary predicate $<$ relating first-sort things. The mathematical axioms are:

  1. $\forall x \thinspace ¬ x < 0$

  2. $\forall x \forall y (x = y \lor x < y \lor y < x)$

  3. $\forall x \forall y \forall z (x < y \land y < z \Rightarrow x < z)$

  4. Induction: $\phi(0) \land \forall n \forall m (\phi(n) \land \sigma n,m \Rightarrow \phi(m)) \Rightarrow \forall n \phi(n)$
    where: $\ \sigma x,y$ abbreviates $x < y \land ¬\exists z(x < z \land z < y) $

  5. Replacement: $\forall F \forall c \forall i \exists G \thinspace (G(i) = c \land F =_i G)$
    where: $\ F =_i G$ abbreviates $\forall x (x ≠ i \Rightarrow F(x) = G(x))$

Notable lack is the axiom:

(S) $\forall x \exists y (x<y)$

So as stated axioms 1-5 have as model the singleton universe {$0$}. Nonetheless this system can define addition, multiplication, and prove many arithmetic assertions. It is more mathematically interesting to exclude the axiom (S), I think, because one can then ask the question how the addition of binary (or $n$-ary...) functions improves the power of the system, which is not the case if the system includes (S), since then one can simply use natural numbers to code tuples and thus unary functions suffice to represent n-ary functions. See Can this weakish system of arithmetic express multiplication for second-sort numbers?.

$\endgroup$
2
  • $\begingroup$ Is this system first order? You are allowing quantification over functions? $\endgroup$ Commented Oct 19, 2023 at 12:42
  • $\begingroup$ Yes the system is first-order. Yes, it allows quantification over functions. See mathoverflow.net/questions/105234/… or plato.stanford.edu/entries/logic-many-sorted (see specifically 1.1 in the latter, where relations are used, but functions are just a special kind of relations). To be clear, no comprehension axiom is being assumed. $\endgroup$
    – abo
    Commented Oct 20, 2023 at 5:33
8
$\begingroup$

The original question was:

Can we use lists as the primary notion and build mathematics around it?

My answer is that any such approach runs into trouble very quickly, as can be gleaned from the following basic example from real analysis.

Let $f$ be a regulated function from reals to reals, i.e. the right and left limits $f(x+)$ and $f(x-)$ exist for all reals $x\in [0,1]$. Many proofs in analysis make use of the sets $C_f$ and $D_f$, which collect the reals where $f$ is continuous, resp. discontinuous. Now, the set $D_f$ is countable and can be written as the union of finite sets as follows: $D_f=\cup_k D_k$ where

$$ \textstyle D_k:= \{x \in [0,1]: |f(x)-f(x+)|>\frac{1}{2^{k}}\vee |f(x)-f(x-)|>\frac{1}{2^{k}} \}$$

One needs absurdly strong axioms (think second-order arithmetic) to show that $D_f$ can be written as a sequence of reals and that $D_k$ can be written as a finite list. The details may be found in [1, 2].

Thus, while your approach may be possible, it would look very strange from the point of view of e.g. reverse math.

References

1 Dag Normann and Sam Sanders, on robust theorems due to Jordan, Cantor, Weierstrass, and Bolzano, JSL, 2022.

[2] Sam Sanders, Big in Reverse Mathematics: the uncountability of the reals, JSL, 2023

$\endgroup$
4
  • 4
    $\begingroup$ Second-order arithmetic is absurdly strong? $\endgroup$ Commented Oct 18, 2023 at 18:24
  • 2
    $\begingroup$ I have known people to say that $I\Delta_0+ \textsf{EXP}$ is very strong. Second-order arithmetic is rather strong if one is doing basic math like "this set is finite or countable". $\endgroup$ Commented Oct 18, 2023 at 18:43
  • $\begingroup$ $D_k$ is a finite list? Is there a missing hypothesis? What about say the floor function, $D_1$ is infinite? $\endgroup$ Commented Oct 20, 2023 at 8:26
  • $\begingroup$ My mistake: I should have restricted to the unit interval (which is now in place). $\endgroup$ Commented Oct 20, 2023 at 9:32

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .