1
$\begingroup$

I am trying to formally construct the usual partial ordering LTE from Peano's 5 Axioms. Would the following construction work?

$$\forall a,b: [(a,b)\in LTE \iff(a,b)\in N^2$$

$$\land ~ \forall c\subset N^2:[\forall d\in N: [(d,d) \in c]$$

$$ \land ~ \forall d,e:[(d,e)\in c \implies(d, S(e))\in c]$$

$$\implies (a,b) \in c]]$$

where $N$ is the set of natural numbers and $S$ is the usual successor function on $N$.

EDIT:

Informally, for all $x,y\in N$, we can recursively define $\le$ on $N$ as the "smallest" set of ordered pairs of natural numbers that satisfies:

$$x \le x$$

$$x\le y \implies x\le S(y)$$

$\endgroup$
11
  • 1
    $\begingroup$ In the second line, you switch from defining $LTE$ to making a statement about all relations, which seems like it's not what you want. $\endgroup$
    – Misha Lavrov
    Apr 20, 2021 at 22:14
  • 2
    $\begingroup$ LTE means.... what? $\endgroup$
    – Lee Mosher
    Apr 20, 2021 at 22:28
  • $\begingroup$ @LeeMosher LTE (less than or equal) is a set of ordered pairs of natural numbers. $\endgroup$
    – Dan Christensen
    Apr 20, 2021 at 22:29
  • $\begingroup$ I think your definition is fine: You are saying that $a \le b$ holds if whenever $R$ (which you call $c$) is a relation on $N$ that is reflexive and is such that $d\mathrel{R}S(e)$ whenever $d\mathrel{R}e$, then $a\mathrel{R}b$.That says that $(\le)$ is the intersection of all reflexive relations $R$ such that $(S \circ R) \subseteq R$, which is true. $\endgroup$
    – Rob Arthan
    Apr 20, 2021 at 22:46
  • 1
    $\begingroup$ Do note that the definition involves some second-order logic, though. Unless you're considering $N$ as being a set within some first-order set theory such as ZFC, or something along those lines. $\endgroup$
    – Daniel Schepler
    Apr 20, 2021 at 23:23

1 Answer 1

Reset to default
-1
$\begingroup$

(Answering my own question)

Thanks all for your help, but I didn't find my construction here to be very workable. I was trying to avoid using an addition function to "simplify things." That was probably a mistake.

Using Peano's Axioms, some basic set theory and a form of natural deduction, I formally constructed (in order) the function $+$ and the relations $\leq$ and $\lt$ as sets of ordered n-tuples such that, for all $x, y \in N$ we have:

$x+0 = x$

$x+S(y) = S(x+y)$

$x\leq y \iff \exists z\in N: x+z=y$

$x \lt y \iff x\leq y ~\land ~ x\neq y$

Everything then fell into place. I was just now able to derive the usual fundamental properties of $+$, $\leq$ and $\lt$ for a larger project that I am working on.

$\endgroup$

You must log in to answer this question.

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