-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 yesterday
  • $\begingroup$ EDIT: $\mathbb{N}=\{n : \forall(k\leq n), \neg(k<k)\}$ $\endgroup$ Commented yesterday

1 Answer 1

0
$\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$

You must log in to answer this question.

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