Числовые системы. Определение целых чисел.

[ArshakA]

Я предлагаю короткое и простое определение целых чисел в рамках формальной математики.
Вначале договоримся о следующем синтаксисе:
1)Введение нового объекта:
$\mapsto$ идентификатор "название"
(вообще говоря необходимости в названии нет);
2)Введение нового условия:
условие
(в записи условия могут использоваться булевы операции, кванторы общности и существования, а также имена переменных)
3)Все функции (кроме логических операций) записываются в общем виде $f(a)$, а все отношения (и логические операции) записываются привычным способом $a$\sim$b$
Система задается одновременным выполнением всех записанных в ней условий над всеми описанными в ней объектами. Под объектом понимается что угодно. Не делается никаких различий между множествами, операциями, отношениями, числами, матрицами, фигурами и т.п. Считается что любой объект может выступать в качестве функции и любой в качества аргумента. Логические операции и отношение принадлежность ($\in$) считаются уже определёнными.
Итак, опишем целые числа.

Целые числа
$ \mapsto \; \mathbb{Z} \quad $ "целые числа"
$ \mapsto \; 0 $ "ноль"
$0\in\mathbb{Z}$
$ \mapsto \; \prime $ "штрих"
$ \mapsto \; \prime\prime $ "анер"
$\forall n \in Z : (\prime (n) \in \mathbb{Z}) \; \wedge \; (\prime\prime (n) \in \mathbb{Z}) $
$ \mapsto \; > $ "больше"
$\forall n \in Z : (\prime (n) > n) \; \wedge \; (n >\prime\prime (n)) $
$\forall n,m,k \in Z : ((n>m)\wedge(m>k))\Rightarrow (n>k) $
$ \mapsto \; = $ "равно"
$\forall n \in Z : n=n $
$\forall n,m \in Z : ((n>m)\vee(m>n)) \; \Leftrightarrow \; \neg(n=k) $
Всё

То же самое по русски:
Вводится объект "целые числа"
Вводится объект "ноль"
Ноль принадлежит целым числам
Водится объект "штрих" (да эта операция будет использоваться традиционным образом ($\prime(a)=a+1$), но для этого мы не нуждаемся ни в каких дополнительных определений. Все свойства всех описанных операций следуют из названных далее условий)
Вводится объект "анер" (по смыслу противоположен штриху)
Для любого объекта принадлежащего "целым числам" (далее просто целое число) и штрих и анер от него являются целыми числами
Вводится объект "больше"
Штрих от любого целого числа больше самого числа, а само число больше своего анера
"Больше" обладает транзитивностью
Вводится объект "равно"
Каждое целое число равно само себе
Для каждой пары целых чисел одно не равно другому тогда и только тогда, когда либо первое больше второго, либо второе большего первого.

Если всё верно и данный набор условий действительно полноценно описывает целые числа, тогда этот способ намного лучше (элегантней) расширения натуральных чисел, которые надо сначала описать через аксиомы Пеано.

[arseniiv]

У вас нельзя показать, что $\prime(\prime\prime(n)) = \prime\prime(\prime(n)) = n$.

Плюс, было бы неплохо иметь сложение и умножение, а не только $<$.

Плюс, неплохо было бы изучить стандартный способ определения аксиоматической теории первого порядка, чтобы записывать всё компактнее и понятнее для большинства тех, кому могла бы быть интересной аксиоматизация $\mathbb Z$.

-- Сб июл 09, 2016 22:19:25 --

Вообще, предлагаю вместо $\prime(n),\prime\prime(n)$ писать $Sn,Pn$ или хотя бы $n',n''$ — и набирать, и читать удобнее.

[ArshakA]

Цитата:

У вас нельзя показать, что $\prime(\prime\prime(n)) = \prime\prime(\prime(n)) = n$.

Спасибо, подумаю о этом

Цитата:

Плюс, было бы неплохо иметь сложение и умножение, а не только $<$.

$ \mapsto \; + $ "сложение"
$\forall n \in Z : +(n,0)=n $
$\forall n,m \in Z : +(n,\prime(m))=\prime(+(n,m))$
$\forall n,m \in Z : +(n,\prime\prime(m))=\prime\prime(+(n,m))$
$ \mapsto \; - $ "вычетание"
$\forall n \in Z : -(n,0)=n $
$\forall n,m \in Z : -(n,\prime(m))=\prime\prime(-(n,m))$
$\forall n,m \in Z : -(n,\prime\prime(m))=\prime(-(n,m))$
$ \mapsto \; \times $ "умножение"
$\forall n \in Z : \times(n,0)=0 $
$\forall n,m \in Z : \times(n,\prime(m))=(+(\times(n,m),n))$
$\forall n,m \in Z : \times(n,\prime\prime(m))=(+(nm,-(0,n)))$
Можно ещё и деление и любые какие угодно душе операции

-- 09.07.2016, 20:44 --

Цитата:

Вообще, предлагаю вместо $\prime(n),\prime\prime(n)$ писать $Sn,Pn$ или хотя бы $n',n''$ — и набирать, и читать удобнее.

Мне без разницы. Просто у меня

Цитата:

Считается что любой объект может выступать в качестве функции и любой в качества аргумента

И тогда скобочная форма более универсальна, но против удобства возражать не буду

[Dmitriy40]

Простите, что-то я не заметил где именно заложено перечисление всех целых чисел? Ведь не введён объект "единица" как минимальная разница между соседними целыми числами, а значит любые операции могут ходить лишь по выделенному подмножеству целых чисел (например лишь по чётным числам со знаком и нулём). Или даже ещё смешнее, только по простым числам (плюс два разных знака плюс ноль)! Вроде при этом все аксиомы выполняются ... Или я не прав и что-то проглядел?

[ArshakA]

Цитата:

а значит любые операции могут ходить лишь по выделенному подмножеству целых чисел

Вот именно только по ним они и будут ходить. Т.е. других чисел и не будет. А любое такое подмножество целых чисел обязательно будет иметь взаимно однозначное отображение на сами целые числа т.е будет эквивалентно им. Если записи $1+3=5$, $1+5=7$ и $1+7=11$ Вам не нравятся, то просто пишите вместо вместо $5$ - $4$, вместо $7$ - $5$, а вместо $11$ - $6$, сути и содержания это не меняет, меняется только форма записи, только символы.

[Dmitriy40]

А в варианте с простыми числами? Тоже можно построить взаимно однозначное соответствие? Ну возможно, типа номер простого числа ... Но будет ли это так же удобно как и обычное определение?
Всё равно не понимаю как без определения понятий "следующее" и "предыдущее" число (для чего и нужна единица) и утверждений об их единственности строить множество "целых" чисел. Вернее определения добавить похоже можно, но вот их практическая реализация может стать любой сколь угодно сложной - в зависимости от выбора подмножества целых чисел (уже даже с простыми числами будут огромные проблемы, а числа бывают и посложнее).

[arseniiv]

ArshakA в сообщении #1136816 писал(а):

Мне без разницы. Просто у меня

Цитата:

Считается что любой объект может выступать в качестве функции и любой в качества аргумента

И тогда скобочная форма более универсальна, но против удобства возражать не буду

В такой универсальности нет не только нужды, но даже и обоснования. Нет смысла образовывать термы ${+}(0),S({+},0,0),0({<})$, у всех символов фиксированная арность. Потом, если уж писать скобочно, так надо поступать и со всем остальным — ${\vee}({<}(m,n),{<}(n,m))$ и т. п..

Dmitriy40 в сообщении #1136822 писал(а):

Простите, что-то я не заметил где именно заложено перечисление всех целых чисел? Ведь не введён объект "единица" как минимальная разница между соседними целыми числами, а значит любые операции могут ходить лишь по выделенному подмножеству целых чисел (например лишь по чётным числам со знаком и нулём).

Не, вот сейчас определением умножения единицу зафиксировали… точнее, это только шаг в нужную сторону.

Если серьёзнее, то я здесь вижу попытки сделать по образу и подобию аксиоматизации натуральных чисел. Но куда тогда потерялась аксиома $Sn=Sm\Rightarrow n=m$? Или схема индукции?

Dmitriy40 в сообщении #1136830 писал(а):

Всё равно не понимаю как без определения понятий "следующее" и "предыдущее" число (для чего и нужна единица)

Единица для этого не нужна, посмотрите аксиомы арифметики. Даже если мы начинаем натуральный ряд с неё, она связана с $Sn$ только через сложение, и это вообще определение сложения, а не $S$, потому что можно обойтись и без сложения.

Dmitriy40 в сообщении #1136830 писал(а):

Но будет ли это так же удобно как и обычное определение?

В любом случае, до определения целых чисел снисходят не очень часто после того как разобрались с ним, а особенно занялись алгеброй и взяли себе определение более идейное (например, свободная абелевая группа, порождённая одним элементом, или бесконечная циклическая группа). Хотя мне кажется, что нет нужды чем-то заменять обычное.

Dmitriy40 в сообщении #1136830 писал(а):

Вернее определения добавить похоже можно, но вот их практическая реализация может стать любой сколь угодно сложной

Не очень понятно, при чём тут практическая реализация. Мало кто реализует натуральные числа, записывая их в унарной системе счисления (ближайшему аналогу к термам $0,S0,SS0,\ldots$); потом, даже у арифметики есть нестандартные модели, а мы имеем в виду обычно только одну.

[Dmitriy40]

arseniiv в сообщении #1136834 писал(а):

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

Я имел в виду что можно неожиданно получить невычислимые (или трудновычислимые, как простые) числа в списке что затруднит операции в такой алгебре даже ручкой на бумаге в любых обозначениях (вплоть до того что не удастся сравнить два числа между собой). Взаимно однозначное соответствие с целыми будет, но указать конкретную пару в таком соответствии станет архисложно (типа - номер первого простого числа после $3^{7185}$?).

[arseniiv]

Эмм. Ну так если сказать «кольцо, полученное из бесконечной циклической группы $Z$ с образующим $a$ введением умножения $m\cdot n = f^{-1}(m)(n)$, где биекция $f\colon\varphi\in\mathrm{End}(Z)\mapsto\varphi(a)$», то этому определению ведь тоже такая штука с простыми числами удовлетворять будет. Тут разницы никакой, важно только доказать, что хоть одна алгебраическая система удовлетворяет требованиям, или, говоря логически, что у данного множества аксиом есть модель. Потом модели, изоморфные данной, автоматически берутся в расчёт. Другое дело, что могут быть неизоморфные этой модели. Вот предложенному в этой теме списку аксиом, если их привести в порядок, заменяя, в частности, ограниченные кванторы обычными, убрав $0\in Z$ (коль константа присутствует в языке, она должна представляться в модели каким-то элементом), etc., удовлетворяет не обязательно что-то изоморфное $\mathbb Z$. Правда, я другую модель пока не вижу, но и не думал об этом специально (если бы порядка не было, можно сразу бы кучу конечных колец предложить).

[ArshakA]

Цитата:

Потом, если уж писать скобочно, так надо поступать и со всем остальным — ${\vee}({<}(m,n),{<}(n,m))$ и т. п..

да я так и хотел сначала, но слишком не читаемо получилось. Поэтому я решил договорится, что

Цитата:

3)Все функции (кроме логических операций) записываются в общем виде $f(a)$, а все отношения (и логические операции) записываются привычным способом $a \sim b$

Но вообще это не существенно. Как Вам удобно так и пишите (главное, что бы понятно было)

Цитата:

В такой универсальности нет не только нужды, но даже и обоснования. Нет смысла образовывать термы ${+}(0),S({+},0,0),0({<})$

Категорически не согласен. Если в рамках конкретной системы нет нужды в подобных термах - то никто не заставляет их использовать. Но вообще запрещать - нельзя. Вы говорите нет смысла, но ведь сама по себе никакая запись смысла не имеет. Смысл вкладываем в неё мы, договариваясь, что значит тот или иной символ (и та или иная композиция символов). Поэтому стоит договорится, что $0(+)=0$,а $0(-)=-1$ как смысл сразу появится. Мы ничего не тереям, а получаем полную свободу возможностей.
А по поводу арности.. можно вообще считать, что все операции унарны. Один единственный аргумент - множество, состоящее из нескольких элементов (необязательного одного типа) с которыми и работает функция.То есть арность функции - дело договорённости. Впринципе любая функция может быть хоть бесконечноарна (самый простой вариант - никак не реагируя на лишние аргументы) , хоть унарна.

Цитата:

убрав $0\in Z$ (коль константа присутствует в языке, она должна представляться в модели каким-то элементом)

если я правильно понял(скорее всего нет), вы хотите сказать, что любой явно введённый объект пренадлежит описываемой структуре. Тогда и штрих, и анер, и больше, и равно тоже целые числа?

[Someone]

ArshakA в сообщении #1136889 писал(а):

вы хотите сказать, что любой явно введённый объект пренадлежит описываемой структуре. Тогда и штрих, и анер, и больше, и равно тоже целые числа?

arseniiv в сообщении #1136810 писал(а):

неплохо было бы изучить стандартный способ определения аксиоматической теории первого порядка

[arseniiv]

(Начал писать до ответа Someone, так что та же мысль ниже ещё раз повторяется.)

ArshakA в сообщении #1136889 писал(а):

Смысл вкладываем в неё мы, договариваясь, что значит тот или иной символ (и та или иная композиция символов).

Вот потому стоит почитать про языки первого порядка. Как интерпретируется любой такой язык, задаётся однозначно, и обычно языков первого порядка хватает. Если нам нужна какая-то другая логика — модальная, второго порядка, и т. п., смысл формул и там будет некоторым обобщением этого. Как показывает практика, выразительности допуск записей $0({+})$ не добавляет. Впрочем, можно при желании свою теорию оформить как расширение какой-то теории множеств, язык которой был уже расширен термами вида $f(\ldots)$ (хотя некоторые способы сделать что-то похожее без повреждения единственности чтения кого-то могут не устраивать), но это явно overkill, когда нужна теория только целых чисел и ничего больше.

ArshakA в сообщении #1136889 писал(а):

А по поводу арности.. можно вообще считать, что все операции унарны. Один единственный аргумент - множество, состоящее из нескольких элементов (необязательного одного типа) с которыми и работает функция.То есть арность функции - дело договорённости. Впринципе любая функция может быть хоть бесконечноарна (самый простой вариант - никак не реагируя на лишние аргументы) , хоть унарна.

Это тоже вредно. Если вы собираетесь со своей теорией что-то существенное делать, такие вольности будут мешать, и немало. Уж не говорю о том, что применение нераспространённого вида языков для такой задачи неблаготворно скажется на числе читателей. Почитайте всё-таки про языки первого порядка — например, Верещагин, Шень, Языки и исчисления (гл. Языки первого порядка, но стоит почитать с начала) (если вдруг: то, что я выше кое-где называл языком, там зовётся сигнатурой).

ArshakA в сообщении #1136889 писал(а):

если я правильно понял(скорее всего нет), вы хотите сказать, что любой явно введённый объект пренадлежит описываемой структуре. Тогда и штрих, и анер, и больше, и равно тоже целые числа?

Вот потому и нужно зафиксировать у них арность. Нульарная операция естественно соответствует константе, так что нульарный функциональный символ $0$ должен интерпретироваться константой. Унарный ф. символ $S$ должен интерпретироваться унарной операцией, и т. п..

[ArshakA]

Цитата:

Но куда тогда потерялась аксиома $Sn=Sm\Rightarrow n=m$? Или схема индукции?

Т.е. если $f(1)$ - верно и $f(n) \Rightarrow f(n+1)$ то $\forall n :f(n) $ - верно? Если вы об этом, тогда объясните зачем это аксиматизировать. Докажем справедливость вышесказанного. $\forall n :f(n) $ - верно, тогда и только тогда, когда $ f(n-1) $ верно. Анологично$ f(n-1) \Leftrightarrow f(n-2)$ , а значит $ f(n) \Leftrightarrow f(n-2)$ и так далее. Из конечности $n$ следует, что когда-нибудь мы дойдем до $ f(n) \Leftrightarrow f(1)$ . А так как $f(1)$ верно, то и $f(n)$ верно, что и требовалось доказать. ( Это общими словами. Если, что можно формализовать. )

Цитата:

У вас нельзя показать, что $\prime(\prime\prime(n)) = \prime\prime(\prime(n)) = n$.

Да видимо придётся аксиматизировать

Цитата:

Вот предложенному в этой теме списку аксиом, если их привести в порядок, заменяя, в частности, ограниченные кванторы обычными, убрав $0\in Z$ (коль константа присутствует в языке, она должна представляться в модели каким-то элементом), etc., удовлетворяет не обязательно что-то изоморфное $\mathbb Z$

По этим словам ещё 2 вопроса: зачем заменять ограниченные кванторы обычными (ведь все ограничения сводятся к условию пренадлежности $\mathbb{Z}$), и какие ещё фактические (не поводу нетрадиционной формы записи) ошибки вы видите?

-- 10.07.2016, 02:28 --

Цитата:

Верещагин, Шень, Языки и исчисления

Спасибо! Прочту.

[arseniiv]

ArshakA в сообщении #1136908 писал(а):

Т.е. если $f(1)$ - верно и $f(n) \Rightarrow f(n+1)$ то $\forall n :f(n) $ - верно?

Она такова в арифметике, но здесь её надо будет подлатать.

ArshakA в сообщении #1136908 писал(а):

Если вы об этом, тогда объясните зачем это аксиматизировать.

Модели уж сильно неподходящие тогда появляются. Например, у аксиом

$$\begin{array}{l} 0\ne Sn, \\ Sm=Sn\to m=n, \\ m+0=m, \\ m+Sn=S(m+n), \\ m\cdot0=0, \\ m\cdot Sn=m\cdot n+m \end{array}$$

(для соответствующего языка) есть модель, которую можно получить, добавив к натуральным числам натуральночисленные многочлены и интерпретируя всё подобающе. Некоторые аксиомы индукции тут неверны и, в частности, не верно следующее из одной из них $n=0\vee\exists m(n=Sm)$.

ArshakA в сообщении #1136908 писал(а):

По этим словам ещё 2 вопроса: зачем заменять ограниченные кванторы обычными (ведь все ограничения сводятся к условию пренадлежности $\mathbb{Z}$), и какие ещё фактические (не поводу нетрадиционной формы записи) ошибки вы видите?

1. Просто потому что в язык нет нужды добавлять $Z$ и $\in$.
2.1. Например, недостаточно аксиом для определения равенства. Обычно его или вообще используют как логический символ, интерпретирующийся всегда как равенство, и тогда не нужна и аксиома $n=n$, или трактуют как обычный предикатный, и тогда используют какие-то из стандартных аксиом равенства, а модели ограничивают нормальными — в которых оно интерпретируется как равенство. Что так, что эдак, а у вас сейчас нельзя из $n=S0$ вывести $Sn=SS0$.
2.2. Для $<$, кажется, тоже недостаточно.
3. Я бы чисто по вкусу взял смену знака (унарный минус) вместо вычитания.

-- Вс июл 10, 2016 05:17:23 --

ArshakA в сообщении #1136908 писал(а):

Докажем справедливость вышесказанного. $\forall n :f(n) $ - верно, тогда и только тогда, когда $ f(n-1) $ верно. Анологично$ f(n-1) \Leftrightarrow f(n-2)$ , а значит $ f(n) \Leftrightarrow f(n-2)$ и так далее. Из конечности $n$ следует, что когда-нибудь мы дойдем до $ f(n) \Leftrightarrow f(1)$ . А так как $f(1)$ верно, то и $f(n)$ верно, что и требовалось доказать. ( Это общими словами. Если, что можно формализовать. )

Попробуйте формализовать. Интересно, какой большой кусок теории множеств вам понадобится…

[ArshakA]

arseniiv
Спасибо