Упорядочение натуральных чисел

[Picchio dal Pozzo]

Здравствуйте!

Допустим, мы ввели натуральные числа (начиная с единицы) по Пеано. Я видел книги, в которых порядок на $\mathbb{N}$ вводится через операцию сложения: $m<n \stackrel{def}{\Leftrightarrow} \exists p : m+p=n$, а иного способа ввести порядок не видел (или не помню). На уровне бытовой очевидности кажется, что порядок возникает сразу из отображения следования, ещё до сложения. Можно ли написать $m<n \stackrel{def}{\Leftrightarrow} \exists p : S^p(m)=n$, или это будет нехорошо?

[svv]

Простите, я совершенно не разбираюсь в этой теме, но мне стало интересно: а $m+p$, случайно, не определяется, как $S^p(m)$?

[Picchio dal Pozzo]

svv в сообщении #1604129 писал(а):

а $m+p$, случайно, не определяется, как $S^p(m)$?

Сложение вводится двумя аксиомами: $n+1 = S(n)$, $n+S(m) = S(n+m)$. В итоге-то оно так и выходит, что $m+p = S^p(m)$, но меня смущает, что порядок, который (опять же, на уровне моей бытовой очевидности) кажется более фундаментальным, чем сложение, описывается после сложения. То ли это не более чем вопрос удобства, то ли есть какая-то логическая тонкость, которой я не вижу.

[KhAl]

Зависит от того, с какой целью Вы вводите натуральные числа по Пеано. С общематематической точки зрения -- можно. С формальной -- нельзя, потому что $S^p(m)$ (именно с $p$ сверху) это какой-то новый значок, правила работы с которым не определены, соответственно, про него ничего нельзя доказать на том уровне строгости, для которого придуманы аксиомы Пеано. Как Вам такие "аксиомы Пеано"?
$\forall x\; \left( x = 1 \text{ или } \exists p\; x = S^p(1) \right)$
$\forall x\; \forall y\; x+y = S^{y}(x)$
$\forall x\; \forall y\; x \cdot y = \underbrace{x + x + ... + x}_{y \text{ раз}}$

Да, $<$ можно определить до сложения, аксиоматически (кванторы доставить):
$\begin{xy}*{\text{1. неверно, что } x < x};p+L;+R**h@{-}\end{xy}$ (следует из $2$)
2. $x < y \Leftrightarrow y = S(x) \text{ или } \exists z\; \left( x < z \text{ и } y = S(z) \right)$

[epros]

Picchio dal Pozzo в сообщении #1604128 писал(а):

Можно ли написать $m<n \stackrel{def}{\Leftrightarrow} \exists p : S^p(m)=n$, или это будет нехорошо?

Это будет хорошо, только если в сигнатуру теории добавить обозначение, а в аксиоматику - определение для операции $S^p(m)$. Но это не нужно, потому что в сигнатуре и аксиоматике теории уже есть операция сложения, предназначенная для того же самого.

-- Вс авг 06, 2023 11:19:15 --

Picchio dal Pozzo в сообщении #1604131 писал(а):

но меня смущает, что порядок, который (опять же, на уровне моей бытовой очевидности) кажется более фундаментальным, чем сложение, описывается после сложения.

Не смущайтесь, порядок записи аксиом для определения теории не имеет значения.

-- Вс авг 06, 2023 11:35:13 --

Хотя, если рассуждать с точки зрения "осмысленных расширений" теории, то я не вижу разумного способа расширить арифметику без сложения на отношение порядка. Вам просто будет сложно придумать, как конечной формулой можно определить порядок через однократный инкремент. В конечном итоге Вы придёте к тому, что в эту формулу вошьёте обе аксиомы сложения.

[KhAl]

epros в сообщении #1604145 писал(а):

Хотя, если рассуждать с точки зрения "осмысленных расширений" теории, то я не вижу разумного способа расширить арифметику без сложения на отношение порядка. Вам просто будет сложно придумать, как конечной формулой можно определить порядок через однократный инкремент. В конечном итоге Вы придёте к тому, что в эту формулу вошьёте обе аксиомы сложения.

Ага, теория натуральных чисел в сигнатуре $\langle 1;\, =;\, S \rangle$ допускает элиминацию кванторов, так что любая формула в этой сигнатуре эквивалентна безкванторной. Можно проверить, что среди безкванторных формул нет такой, которая равносильна $x < y$

[Picchio dal Pozzo]

KhAl, epros, благодарю! Последние сообщения -- как раз то, что мне надо. Буду ещё разбираться.