О символьной записи определений.

[melnikoff]

Определение 1. Пусть $a,\,b\in \mathbb{Z}$, причем $b\neq 0$. Число $a$ делится на число $b$ (пишут $a\vdots b$), если существует такое $c\in \mathbb{Z}$, что $a=cb$.

Правильно ли будет записать это определение так:
$a\vdots b \Longleftrightarrow^{def} a\in \mathbb{Z} \wedge b\in \mathbb{Z}\setminus \{0\}\wedge \exists c \left(c\in \mathbb{Z} \wedge a=cb\right)$?
Или так:
$a\vdots b \Longleftrightarrow^{def} a\in \mathbb{Z} \wedge b\in \mathbb{Z}\setminus \{0\}\wedge \exists c \in \mathbb{Z}: a=cb.$
Но тут возникает вопрос, правильно ли использован символ двоеточия, который читается тут как "такое, что"?
Примечание: не знаю как написать правильно символ кратности и как def написать над символом равносильности.

[mihailm]

Можно по-моему, и так и так.
Только зачем ограничивать делители ненулевыми значениями?

[melnikoff]

mihailm в сообщении #848615 писал(а):

Только зачем ограничивать делители ненулевыми значениями?

Такое определение дают во всех учебниках.

Есть более общий вопрос. Многие определения формулируются так:
Пусть $A$. Тогда $B \Longleftrightarrow^{def} C.$ Где $A, B, C$ – некоторые высказывания, а $B$ – вводимое понятие данным определением.
Это нужно понимать так:
$B\Longleftrightarrow^{def} A \wedge C$ ?

[mihailm]

Это не нужно

[melnikoff]

mihailm в сообщении #848618 писал(а):

Это не нужно

Тогда получится, что \forall c \{c\in\mathbb{Z}\Rightarrow $0=0\cdot c\}$. То есть частное от деления нуля на нуль однозначно не определено.

[mihailm]

Так это сплошь и рядом в кольцах, и что?

[Munin]

melnikoff в сообщении #848610 писал(а):

Примечание: не знаю как написать правильно символ кратности и как def написать над символом равносильности.

Для символа делимости, практически, \vdots - один из самых лучших вариантов. Можно сделать его отношением:
a\mathrel{\vdots}b $a\mathrel{\vdots}b$

Чтобы написать надпись над символом равносильности,
\stackrel{def}{\Longleftrightarrow} $A\stackrel{def}{\Longleftrightarrow}B$
Красивей так:
\stackrel{\mathrm{def}}{\Longleftrightarrow} $A\stackrel{\mathrm{def}}{\Longleftrightarrow}B$

[arseniiv]

melnikoff в сообщении #848617 писал(а):

Есть более общий вопрос. Многие определения формулируются так:
Пусть $A$. Тогда $B \Longleftrightarrow^{def} C.$ Где $A, B, C$ – некоторые высказывания, а $B$ – вводимое понятие данным определением.
Это нужно понимать так:
$B\Longleftrightarrow^{def} A \wedge C$ ?

Не надо возводить «определяющие» $=$ и $\Leftrightarrow$ в какой-то особый статус. «Пусть $A$, тогда $B\Leftrightarrow C$» так и запишется: $A\Rightarrow(B\Leftrightarrow C)$. Можно, конечно, попытаться вытащить $B$ и получить какую-то формулу вида $B\Leftrightarrow \varphi$ и потом нарисовать «def» над равносильностью, но…

Определение — это не какая-то особая формула. Это получение из одной теории другой, «расширенной» этим определением теории. Т. е. была теория, скажем, с сигнатурой $(\in,=)$, а после добавления ещё одной аксиомы стала с $(\in,=,\varnothing)$, а потом вообще $(\in,=,\varnothing,\subset)$.

melnikoff в сообщении #848610 писал(а):

Но тут возникает вопрос, правильно ли использован символ двоеточия, который читается тут как "такое, что"?

Не важно как он читается. Можно обойтись вообще без него. Многие люди пишут так: $\forall v\;(\varphi)$ и так: $\forall v\in A\;(\varphi)$. Другие добавляют точку или двоеточие и не всегда ставят скобки. (Третьи пишут неаккуратно, и записи соответствует несколько разных формул.) В любом варианте у точки, скобок или двоеточия нет какого-то особенного смысла.

-- Вс апр 13, 2014 02:14:55 --

(Оффтоп)

Интересно, что короче?

$$\begin{array}{c} b\in\mathbb Z\setminus\{0\} \\ b\in\mathbb Z\wedge b\ne0 \end{array}$$

Даже если и длиннее, всё равно лично мне удобочитаемее нижнее.

[Munin]

(Оффтоп)

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

всё равно лично мне удобочитаемее нижнее.

От привычки зависит.

[arseniiv]

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

Можно, конечно, попытаться вытащить $B$ и получить какую-то формулу вида $B\Leftrightarrow \varphi$ и потом нарисовать «def» над равносильностью, но…

Я вчера более-менее ерунду написал. Определение нового предикатного символа $r$ как раз делается добавлением вместе с ним аксиомы вида $\forall x_1\cdots\forall x_n (r(x_1,\ldots,x_n) \Leftrightarrow \varphi)$, где $\varphi$ — формула без $r$. Точнее можно прочитать здесь. Так что можно рассматривать здесь $\Leftrightarrow$ «определяющей». А вот $=$ и функциональные символы так уже не всегда связаны. Например, доказав в теории вещественных чисел, что $\forall x\exists! s(s>0 \wedge s^4 = x^2)$, мы можем ввести функциональный символ $q$ добавлением его вместе с аксиомой $\forall x(q(x)>0 \wedge q(x)^4 = x^2)$, и в исходной теории нет никакой эквивалентной ей формулы вида $\forall x(q(x) = t)$, где терм $t$ не содержит $q$.