First order axioms for sequence theory?

214 Views Asked by At

In a set the repetition and order of the elements does not matter.

In a multiset the order fo the elements does not matter, but the repetitions do.

In a sequence both the order and the repetition matter.

Is there any first order logic and axiomatic formulation of sequences, more or less comparable to the ZFC axioms of set theory?

1

There are 1 best solutions below

0
On BEST ANSWER

I'm not sure that I correctly identified the point of your question. So please let me know whether the following answer is what you are looking for:

Within any reasonably rich set theory we can formalize the notion of multisets and sequences. $\operatorname{ZFC}$ is, obviously, an overkill to do so. But it's the theory most mathematicians (even if they don't know it explicitly) are familiar with. So, for the sake of this answer, let's work within $\operatorname{ZFC}$.

The "standard" approach to multisets and sequences, within $\operatorname{ZFC}$ is as follows:

Step 1. Unordered pairs.

Let $V$ be our set theoretic universe. We want to find a (definable class function) $$ \langle, \rangle \colon V \times V \to V, \ (x,y) \mapsto \langle x, y \rangle $$ that satisfies the fundamental property of a pairing function. Namely, for all $a,b,c,d \in V$,

$$\langle a,b \rangle = \langle c, d \rangle \iff a = c \wedge b = d$$

The Kuratowski pairing function $$ \langle a, b \rangle := \{ \{a\}, \{a,b\} \} $$ does provably satisfy this condition (in $\operatorname{ZFC}$).

Step 2. Cartesian products.

Once we have a pairing function, we can define the Cartesian product of two sets $X,Y$ as $$ X \times Y := \{ \langle x,y \rangle \mid x \in X \wedge y \in Y \}. $$

(This apparently circular use of Cartesian products can be avoided by a taking a little more care and talking about the actual formula defining the pairing function above.)

Step 3. Functions.

Once we have Cartesian products, we can define functions. A function $f$ with domain $X$ and range $Y$ is a subset $$ f \subseteq X \times Y $$ such that for all $x \in X$ there is a unique $y \in Y$ such that $\langle x, y \rangle \in f$.

Step 4. Multisets.

By the axiom of infinity, the set of natural numbers (including $0$!) $\mathbb N$ exists. A multiset $M$ with domain $X$ is a function $$ M \colon X \to \mathbb N $$ $x \in X$ is a member of $M$ iff $M(x) > 0$ and $M(x)$ is the multiplicity of $x$ in $M$.

It's easy to define the usual operations on multisets. For example, if $M, N$ are multisets with domain $X$ and $Y$ respectively, we can define the union multiset $M \sqcup N$ with domain $X \cup Y$ as follows:

$$ M \sqcup N \colon X \cup Y \to \mathbb N, \ z \mapsto M(z) + N(z). $$

Step 5. Sequences.

A (countable) sequence $S$ with domain $X$ is a function $$ S \colon \mathbb N \to X $$ where $S(n)$ is the $n$-th element of the sequence $S$.

Viewed this way multisets and sequences are sort of dual notions and - modulo the intended interpretation - actually are the same objects when there domain happens to be $\mathbb N$.