-2
$\begingroup$

Logic: Bi-sorted first order logic with equality, first sort written in lower case range over natural numbers, the second sort written in upper case range over sets of naturals, "$=$" has no syntactical restriction, "$\in$" only occurs syntactically from first to second sort, "$||$" is a partial unary function symbol syntactically limited to occur only from second sort to first sort.

Sorting: $x \neq Y$

Extensionality: $\forall z \, (z \in X \leftrightarrow z \in Y) \to X=Y $

Comprehension: $\exists X \forall y \, (y \in X \leftrightarrow \phi(y))$

Define: $X=\varnothing \iff \forall y: y \notin X$.

Elements: $\forall x \exists Y: x=|Y|$

Zero: $\exists x: x = | \varnothing |$

Define: $S=\{k\} \iff \forall y \, (y \in S \leftrightarrow y=k)$

Successors: $ a=|X| \to \exists b: b=|X \cup \{y\}|$

Closure: $Y \subseteq X \land \exists a: a=|X| \to \exists b: b=|Y|$

Define: $a < b \iff \exists X \exists Y \subsetneq X: a=|Y| \land b=|X|$

Actuation: $\forall X \forall a: a < |X| \to \exists Y \subsetneq X: a=|Y|$

Ordering: $X \neq \varnothing \to \exists y \in X \forall z \in X: y \leq z$

Can this theory interpret $\sf PA$? I mean one can define Successor, addition and multiplication on the naturals, but I'm not sure if the last can be proved total.

$\endgroup$
2
  • $\begingroup$ Your theory has a model where "natural number" is interpreted as "countable ordinal", and "$|X|$" is interpreted as the order type of $X$ (defined whenever $X$ is countable), and "$n<m$" is interpreted as asserting the existence of a nontrivial order-embedding $n\to m$. Induction fails under this model & semantics, and we even have $n<n$ for all infinite ordinals $n$, so your axioms cannot prove $\sf{PA}$ outright. However, we can still interpret $\sf{PA}$ by restricting to the subset $\mathbb{N}=\{n : \neg(n<n)\}$. $\endgroup$ Commented Dec 11 at 12:16
  • $\begingroup$ EDIT: $\mathbb{N}=\{n : \forall(k\leq n), \neg(k<k)\}$ $\endgroup$ Commented Dec 11 at 12:24

1 Answer 1

1
$\begingroup$

Yes we can interpret Peano Arithmetic, but only by restricting to a subclass. As I noted in a comment, there's a model of your axioms where the assertion $\forall n, \neg(n<n)$ fails, so we cannot simply prove the $\sf{PA}$ axioms. However, this is the only point of failure, and we can interpret $\sf{PA}$ by restricting to a suitable subclass. Recovering addition is simple, and we can get multiplication by searching for a set encoding an arithmetic progression of a particular length. The relevant definitions of the interpretation are given below. $$\begin{align} \mathbb{N} &:= \{n : \forall(k\leq n), \neg(k<k)\} \\ 0 &:= |\emptyset| \\ \operatorname{S}(n) &:= \min\{k\in\mathbb{N} : n<k\} \\ n-m &:= |\{x\in\mathbb{N} : m\leq x < n\}| \\ n+m &:= \min\{y\in\mathbb{N} : n\leq y \land y-n=m\} \\ \mathcal{M}(S,d) &:\equiv 0\in S\subseteq\mathbb{N} \land \forall(x\in S), \neg(0<x<d)\land(d\leq x \implies x-d\in S) \\ n\cdot m &:= \begin{cases} \max(S) &: n\neq 0 \land \mathcal{M}(S,n) \land |S|=m+1 \\ 0 &: n=0 \end{cases} \end{align}$$

The basic idea is that the relation $\mathcal{M}(S,d)$ indicates whether when $S$ is an initial segment of the set of multiples of $d$. For $n>0$, it can be shown that there's a unique $S$ obeying $|S|=m+1$ and $\mathcal{M}(S,n)$, and we can simply define $n\cdot m = \max(S)$ for that $S$. This fails in case $n=0$, so we just handle that case separately. Once you've proved the basic properties of successors and finite cardinality, there are standard techniques to prove everything else. I'll give proofs for how to establish those "basic properties" from your axioms, and everything is either trivial or follows from some obvious application of induction.


Zero, Wellfoundedness, Successors, Induction.

Lemma: $a<b<c \implies a<c$
proof: Since $b<c$ then there's $B\subsetneq C$ with $b=|B|$ and $c=|C|$, and since $a<|B|$ then via Actuation we find $A\subsetneq B$ with $a=|A|$, and now $A\subsetneq C$ which implies $a<c$. $\square$

Lemma: $a\leq b$ or $b\leq a$
proof: Apply Ordering to the set $X=\{a,b\}$. $\square$

Define $\mathbb{N} := \{n : \forall(k\leq n), \neg(k<k)\}$, and $0:=|\emptyset|$

Theorem: $\mathbb{N}$ is wellordered by the $<$ relation.

Theorem: $\forall(n\in\mathbb{N}), \forall(k<n),k\in\mathbb{N}$

Theorem: $\forall x, \neg(x<0)$, and $0\in\mathbb{N}$, and $0=\min(\mathbb{N})$
proof: If $x<0$ then $x<|\emptyset|$ and thus $\exists X\subsetneq \emptyset, n=|X|$, but $X\subsetneq \emptyset$ is impossible, hence $\neg(x<0)$. The other two results follow immediately from that. $\square$

Define $n+1 := \min\{k\in\mathbb{N} : n<k\}$ for non-maximal $n\in\mathbb{N}$

Lemma: $n+1=m+1 \implies n=m$, for non-maximal $n,m\in\mathbb{N}$

Theorem: $\forall S, S=\emptyset \iff |S|=0$
proof: The forward implication is the definition of $0$. Conversely if $S\neq \emptyset$ then there's $Z\subsetneq S$, and if we also had $|S|=0$ then $\exists k, k=|Z|$ via Closure, but now $k<0$ which is impossible. $\square$

Theorem: $\forall(n\in\mathbb{N}), \forall(A : n=|A|), \forall(x\notin A), |A\cup\{x\}|\in\mathbb{N}$
proof: By contradiction suppose not, then let $n$ be the least counter example. Since $|A\cup\{x\}|\notin\mathbb{N}$, we find $k\leq |A\cup\{x\}|$ with $k<k$, and via Actuation we infer $\exists(B\subseteq A\cup\{x\}), k=|B|$. Every such $B$ has $B\setminus\{x\}\subseteq A$ and thus $|B\setminus\{x\}|\leq n$ which puts $|B\setminus\{x\}|\in\mathbb{N}$. Via wellfoundedness of $\mathbb{N}$, select $B$ so as to minimize the value $M=|B\setminus\{x\}|$. Since $k<k=|B|$, we find $C\subsetneq B$ with $|C|=k$, and clearly $C\subseteq A\cup\{x\}$ so that $M\leq|C\setminus\{x\}|$ via minimality of $M$. We must have $x\in C$, since otherwise we'd get $C\subseteq A$ and $k=|C|\leq |A|\in\mathbb{N}$ so that $k\in\mathbb{N}$, contradicting the fact that $k<k$. It now follows that $C\setminus\{x\}\subsetneq B\setminus\{x\}$ and therefore $|C\setminus\{x\}|<|B\setminus\{x\}|$, but this implies $M<M$, contradicting the fact that $M\in\mathbb{N}$. $\square$

Theorem: $\forall(n\in\mathbb{N}), \forall(A : n=|A|), \forall(x\in A), |A\setminus\{x\}|+1 = |A|$
proof: By contradiction suppose not, then let $n$ be the least counter example. Let $k=|A\setminus\{x\}|$ so that $k<n$ and thus $k+1\leq n$. If we had $k+1=n$, then $|A\setminus\{x\}|+1 = k+1 = n = |A|$ as required, so we must consider $k<k+1<n$. Since $k+1<n$, we find $B\subsetneq A$ with $k+1=|B|$, and we must have $x\in B$ since otherwise $B\subseteq A\setminus\{x\}$ implies $k+1\leq k$, a contradiction. Since $B\subsetneq A$ then select $y\in A\setminus B$ where necessarily $y\neq x$, and now observe $B\setminus\{x\}\subseteq A\setminus\{x,y\}$ so that $|B\setminus\{x\}|\leq|A\setminus\{x,y\}|$. Finally, via minimality of $n$ we infer $|B\setminus\{x\}|+1 = |B| = k+1$ and thus $|B\setminus\{x\}|=k$, and similarly $k=|A\setminus\{x,y\}|+1$. This implies $|A\setminus\{x,y\}|<k=|B\setminus\{x\}|$, a contradiction as expected. $\square$

Corollary: $\forall(n\in\mathbb{N}), \forall(A : |A|=n), \forall(x\notin A), |A\cup\{x\}|=|A|+1$
proof: Since $|A\cup\{x\}|\in\mathbb{N}$ and $A\subsetneq A\cup\{x\}$ then $n<|A\cup\{x\}|$ and thus $n+1$ exists. Our theorem now gives the desired conclusion. $\square$

Corollary: $\forall(n\in\mathbb{N}), n=0 \lor \exists(k<n), n=k+1$
proof: Via Elements we find $S$ with $|S|=n$, and if $S=\emptyset$ then $n=0$. Otherwise find $x\in S$ to infer $|S\setminus\{x\}|+1=|S|$, then letting $k=|S\setminus\{x\}|$ satisfies $k+1=n$. $\square$

Theorem: $(\phi(0) \land \forall(n\in\mathbb{N}), \phi(n)\implies\phi(n+1))\implies \forall(n\in\mathbb{N}), \phi(n)$
proof: Follows from wellordering plus the above corollary. $\square$

Theorem: $\forall(n\in\mathbb{N}), n+1=|\{x : x\leq n\}|$, hence $n+1$ always exists.
proof: When $n=0$ then $\{x : x\leq n\}=\{0\}$ and we verify $|\{0\}| = |\emptyset\cup\{0\}| = 0+1$. Assuming our claim holds at $n$, then $n+1$ exists, and we notice $(n+1)+1$ also exists since $n+1 = |\{x : x\leq n\}|<|\{x : x\leq n+1\}|\in\mathbb{N}$. We now easily verify $(n+1)+1 = |\{x : x\leq n+1\}|$, completing the induction. $\square$

This concludes an interpretation of the Theory of Successor. We've also recovered a recursive definition of finite set cardinality, namely $|S|=0\iff S=\emptyset$ and $|S\cup\{x\}|=|S|+1$ for $x\notin S$. That's all we really need to interpret $\sf{PA}$. From here, everything else is standard.


Addition and Subtraction

Definition: $y-n := |\{x : n\leq x < y\}|$ assuming $y\geq n$, undefined otherwise.

Lemma: $\forall(n\in\mathbb{N}), n-n=0$

Lemma: $\forall(n\leq y\in\mathbb{N}), (y+1)-n = (y-n)+1$

Lemma: $\forall(n\leq y<z\in\mathbb{N}), y-n < z-n$
proof: Follows by induction on $z>y$, using the previous lemma for both the base case and inductive step. $\square$

Theorem: $\forall(n,m\in\mathbb{N}), \exists!(y\in\mathbb{N}), n\leq y \land (y-n)=m$
proof: Existence follows by induction on $m$ using the first two lemmas above, and uniqueness is immediate from the last lemma above. $\square$

Definition: Let $n+m:=y$ denote the unique natural $y\geq n$ satisfying $y-n=m$.

Theorem: $\forall(n\in\mathbb{N}), n+0 = n$
proof: Follows from $n-n=0$. $\square$

Theorem: $\forall(n,m\in\mathbb{N}), (n+m)+1 = n+(m+1)$
proof: Follows from $(y+1)-n = (y-n)+1$ using $y=n+m$. $\square$

Corollary: $n+1 = n+(0+1)$
proof: $n+(0+1) = (n+0)+1 = n+1$. $\square$

Definition: Let $1:= (0+1)$, which unambiguously collapses successor notation into addition.

Lemma: $\forall(n,k\in\mathbb{N}), n\leq k \iff \exists(j\in\mathbb{N}), n+j=k$

This concludes an interpretation of Presburger Arithmetic. We infer $+$ is commutative and associative, and that $+,-,<$ are compatible with each other in the expected ways.


Multiplication

Lemma: $\forall(S\subseteq \mathbb{N}), 0<|S|\in\mathbb{N} \implies \exists(n\in S), n=\max(S)$
proof: Do an induction on $|S|$, using $\max(S\cup\{x\}) = \max\{x,\max(S)\}$. $\square$

Definition: $\mathcal{M}(S,d) :\equiv 0\in S\subseteq\mathbb{N} \land \forall(x\in S), \neg(0<x<d)\land(d\leq x \implies x-d\in S)$.

Lemma 1: $\forall(d\in\mathbb{N}), \mathcal{M}(\{0\},d)$

Lemma 2: $\forall(d\in\mathbb{N}), (\mathcal{M}(S,d)\land |S|\in\mathbb{N}) \implies \mathcal{M}(S\cup\{\max(S)+d\},d)$

Lemma 3: $\forall(d\in\mathbb{N}), (\mathcal{M}(S,d)\land |S|\in\mathbb{N} \land |S|>1) \implies \mathcal{M}(S\setminus\{\max(S)\},d)$

Theorem: $\forall(d\in\mathbb{N} : d>0), \forall(S : \mathcal{M}(S,d)), |S|\geq 2 \implies \max(S)-d = \max(S\setminus\{\max(S)\})$
proof: Follows by induction on $|S|$. In the inductive step, decompose $S=Z\cup\{x,y,z\}$ where $Z\ll x<y<z$. Prove $y-d=x$ from inductive premise using $\mathcal{M}(S\setminus\{z\},d)$ via lemma 3, then notice $x=y-d<z-d<z$. Infer $z-d\in S$, and since $x<z-d<z$ then $z-d=y$, completing the induction. $\square$

Theorem: $\forall(m,d\in\mathbb{N} : d>0), \exists!(S\subseteq \mathbb{N}), |S|=m+1 \land \mathcal{M}(S,d)$
proof: Existence follows by induction on $m$, trivially from lemmas 1 and 2. Uniqueness also follows by induction on $m$. For the inductive step, decompose $x=\max(S)$ and $Z=S\setminus\{x\}$, and infer $Z$ is unique by inductive premise and lemma 3. Use the previous theorem to prove $S=Z\cup\{\max(Z)+d\}$ so that $S$ is uniquely determined by $Z$, completing the induction. $\square$

Definition: Let $0\cdot n := 0$, and for $d>0$ let $d\cdot n := \max(S)$ where $S$ uniquely satisfies $|S|=n+1$ and $\mathcal{M}(S,d)$.

Theorem: $\forall(d\in\mathbb{N}), d\cdot 0 = 0$
proof: Trivial when $d=0$, and for $d>0$ we use the fact $\mathcal{M}(\{0\},d)$. $\square$

Theorem: $\forall(d,n\in\mathbb{N}), d\cdot(n+1) = (d\cdot n)+d$
proof: Trivial when $d=0$, and for $d>0$ we use the fact that $\mathcal{M}(S,d) \implies \mathcal{M}(S\cup\{\max(S)+d\},d)$, where $S$ is selected so that $|S|=m+1$. $\square$

This concludes an interpretation of Peano Arithmetic. Since you permitted the full comprehension schema for sets of numbers, we actually interpret second-order arithmetic. If the Comprehension schema was weakened to only permit finite sets, and Ordering was reformulated as a schema across statements rather than sets, then all our proofs would still follow ($\mathbb{N}$ is reframed as a virtual class) and the resulting theory would be mutually interpretable with $\sf{PA}$.

$\endgroup$
4
  • $\begingroup$ Thanks a lot for this very nice proof! I want to just try actualize what you said in the late lines. To be noted is that this theory I think is consistent with $\forall n: n \not < n$. But, anyhow what I was thinking goes on the other side of actually making $||$ total over all sets, defining $<$ as done in this posting, and weaken comprehension to $\forall n \exists! X \forall y (y \in X \leftrightarrow y \leq n \land \phi)$, then add the axiom $\forall n : n \not < n$. And rephrase Ordering in the way you said to apply over statements instead of sets. This would greatly simplify the axioms. $\endgroup$ Commented Dec 15 at 9:33
  • $\begingroup$ ...the only axioms needed would be the abovementioned Modified comprehension, then finiteness axiom of $n \not < n$, axiom of Elements, axiom of Actuation, and Ordering schema. $\endgroup$ Commented Dec 15 at 9:42
  • $\begingroup$ @ZuhairAl-Johar Yes, that would do it. The way I usually interpret $\sf{PA}$ via cardinality is to start with Theory of Successor, then axiomatize sets via Empty Set, Adjunction, and relatedly $\forall S, \forall x, \exists Z, Z=S\setminus\{x\}$. You can recover the wellorder $<$ from that, and define "finite sets" as bounded sets. Lastly, axiomatize cardinality via $|\emptyset|=0$ and $|S\cup\{x\}|=|S|+1$ for finite $S$ and $x\notin S$, then you interpret $\sf{PA}$ like in my answer. $\endgroup$ Commented Dec 15 at 19:05
  • $\begingroup$ Recovering the standard wellorder $<$ from my axioms is tricky, but basically we use $k<n \iff \exists S, k\in S\land n\notin S \land \forall(m\notin S), m+1\notin S$ as a definition and go from there. In your case it's more like we started with sets and then put numbers on top of them, and we needed to recover the successor function using $<$ rather than vice versa, but otherwise we interpret addition and multiplication in the exact same way. $\endgroup$ Commented Dec 15 at 19:13

You must log in to answer this question.

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