Аксиома порядка в логических символах

[Pennywise]

Решил разобраться с аксиоматикой геометрии Гильберта, так как это со школы меня гложет. Занимаюсь по книге Расина "Лекции по геометрии". Забавы ради решил аксиомы переписать в логических символах. Запись одной аксиомы получилась довольно длинной, поэтому прошу участников форума проверить насколько правильно я это понимаю.

Аксиома такая. $II_4. $ Среди трех попарно различных коллинеарных точек A, B, C существует одна и только одна, лежащая между двумя другими.

До этого были даны аксиомы связности и следующие аксиомы порядка:
1) Если точка B лежит между точками A и C, то A, B, C – различные коллинеарные точки.
2) Если точка B лежит между точками A и C, то B лежит между C и A.
3) Для любых различных точек A, B существует такая точка C, что B лежит между A и C.

У меня такие обозначения. $\Pi$ — множество всех точек плоскости (рассматриваются пока только аксиомы планиметрии), $\Delta \subseteq 2^\Pi$ — множество всех прямых, $M \subseteq \Pi^3$ — отношение "лежать между".

Итак, запись в логических символах получилась следующая:

$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! \lbrace (x, y, z), (z, y, x) \rbrace \subseteq M (x, y, z \in \lbrace A, B, C \rbrace) )$

Верно?

[Connector]

А ещё вроде бы можно так:

$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! y \in \left\lbrace A, B, C \right\rbrace ((x, y, z) \in M \cap \left\lbrace A, B, C \right\rbrace^{3}))$


Верно?

(Оффтоп)

Я не читал Расина, но в оригинале у Гильберта другие аксиомы.

[Connector]

ИМХО, строго говоря, неверно. Ваша запись соответствует более сильному утверждению, из которого, в частности, следует аксиома 2:

Цитата:

Если точка $B$ лежит между точками $A$ и $C$, то $B$ лежит между $C$ и $A$.

[Pennywise]

Connector в сообщении #1409287 писал(а):

ИМХО, строго говоря, неверно. Ваша запись соответствует более сильному утверждению, из которого, в частности, следует аксиома 2

Да, я как-то подзабыл про независимость аксиом друг от друга. Тем не менее, аксиома 2 из моей записи аксиомы 4 не следует. Из неё следует, что если мы возьмём три коллинеарные точки, то одна из них (скажем, С) будет лежать как между А и В, так и между В и А. Это тоже плохо, так как из словесной формулировки подобное заключение вывести нельзя, но формально эта запись не отменяет того случая, когда для каких-нибудь трёх неколлинеарных точек $X, Y, Z: (X, Y, Z) \in M$, а $(Z, Y, X) \notin M$.

Connector в сообщении #1409255 писал(а):

Я не читал Расина, но в оригинале у Гильберта другие аксиомы.

Идейно они близки. Цитата из книги: "В первой главе на основе системы аксиом, близкой к системе аксиом Д.Гильберта (см. [2]), строится достаточно представительный "кусок"планиметрии." Всё-таки книгу, написанную для современных мат. школьников, поприятнее читать, чем перевод 1920-х годов.

[Connector]

Pennywise в сообщении #1409325 писал(а):

но формально эта запись не отменяет того случая, когда для каких-нибудь трёх неколлинеарных точек $X, Y, Z: (X, Y, Z) \in M$, а $(Z, Y, X) \notin M$.

Согласен. Чтобы исключить такую возможность, необходимо дополнительно использовать аксиому 1. Неточно выразился, действительно, следовало сказать о зависимости аксиом. Словом, я имел в виду «из аксиомы 4 и других аксиом».

(Оффтоп)

Кстати, когда, находясь в рамках аксиоматической теории, мы говорим " из $A$ следует $B$ ", то обычно имеем в виду: "из $A$, аксиом и ранее полученных теорем следует $B$ "

(Для аккуратности)

Перевод, конечно, древний, но сделан никак не в 20-е годы, а скорее в 40-е или 30-е.

[beroal]

Pennywise в сообщении #1409247 писал(а):

$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! \lbrace (x, y, z), (z, y, x) \rbrace \subseteq M (x, y, z \in \lbrace A, B, C \rbrace) )$
Верно?

Мне непонятна следующая формула.
$\exists ! \lbrace (x, y, z), (z, y, x) \rbrace \subseteq M (x, y, z \in \lbrace A, B, C \rbrace)$
Существует уникальное что? Множество вида $\lbrace (x, y, z), (z, y, x) \rbrace$?

Connector в сообщении #1409255 писал(а):

А ещё вроде бы можно так:
$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! y \in \left\lbrace A, B, C \right\rbrace ((x, y, z) \in M \cap \left\lbrace A, B, C \right\rbrace^{3}))$

Вы не связали переменные $x, z$.

[Pennywise]

Переделал. Теперь должно быть правильно.

$\forall A_1, A_2, A_3 \in \Pi \ ([(\exists l \in \Delta (A_1, A_2, A_3 \in l)) \wedge (A_1 \neq A_2 \wedge A_2 \neq A_3 \wedge A_1 \neq A_3)] \to \exists ! \ i, j, k \in \lbrace 1, 2, 3 \rbrace [(i \neq j \wedge j \neq k \wedge i \neq k) \wedge ( (A_i, A_j, A_k) \in M \vee (A_k, A_j, A_i) \in M)])$

(Оффтоп)

Connector в сообщении #1409351 писал(а):

Перевод, конечно, древний, но сделан никак не в 20-е годы, а скорее в 40-е или 30-е.

Книгоиздательство "Сеятель" Е. В. Высоцкого, Петроград, 1923

beroal в сообщении #1409354 писал(а):

Существует уникальное что? Множество вида $\lbrace (x, y, z), (z, y, x) \rbrace$?

Да, но я уже понял, что это некорректный "перевод".

[Connector]

beroal в сообщении #1409354 писал(а):

Вы не связали переменные $x, z$.

Да, ошибся. Попробую так:
$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! y \in \left\lbrace A, B, C \right\rbrace \exists x, z \in \left\lbrace A, B, C \right\rbrace ((x, y, z) \in M ))$

(Оффтоп)

Pennywise в сообщении #1409356 писал(а):

Книгоиздательство "Сеятель" Е. В. Высоцкого, Петроград, 1923

...Перевод под редакцией А. В. Васильева. Ясно. Я-то подумал почему-то, что речь об издании 1948 года, пер. с немецкого издания 1930 г.

[beroal]

Pennywise в сообщении #1409356 писал(а):

Да, но я уже понял, что это некорректный "перевод".

В принципе, её можно было бы интерпретировать как $\exists x\in\Pi (\exists y\in\Pi (\exists z\in\Pi (\lbrace (x, y, z), (z, y, x) \rbrace \subseteq M \land \lbrace x, y, z\rbrace \subseteq \lbrace A, B, C \rbrace)))$, но там ещё уникальность… Наверное, не стоит мудрить.

Pennywise в сообщении #1409356 писал(а):

Переделал. Теперь должно быть правильно.

$\forall A_1, A_2, A_3 \in \Pi \ ([(\exists l \in \Delta (A_1, A_2, A_3 \in l)) \wedge (A_1 \neq A_2 \wedge A_2 \neq A_3 \wedge A_1 \neq A_3)] \to \exists ! \ i, j, k \in \lbrace 1, 2, 3 \rbrace [(i \neq j \wedge j \neq k \wedge i \neq k) \wedge ( (A_i, A_j, A_k) \in M \vee (A_k, A_j, A_i) \in M)])$

По-моему, тут та же проблема. Существует уникальный $i, j, k$. Который из них уникален? Кроме того, вначале у вас $A_1$ — это цельное имя, а потом $\{A_i\}_{i\in \{1, 2, 3\}}$ оказывается семейством.

Connector в сообщении #1409362 писал(а):

Попробую так:
$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! y \in \left\lbrace A, B, C \right\rbrace \exists x, z \in \left\lbrace A, B, C \right\rbrace ((x, y, z) \in M ))$

Вот я бы так написал. Если дословно, то ещё надо добавить $x\not =y\land y\not =z$ («две другие точки»), но это следует из $(x, y, z)\in M$ и другой аксиомы, если не ошибаюсь.

[Pennywise]

beroal в сообщении #1409363 писал(а):

Существует уникальный $i, j, k$. Который из них уникален?

Все три. Я думал, что это общепринятое сокращение, чтобы три раза почти что одно и то же не городить.

beroal в сообщении #1409363 писал(а):

Кроме того, вначале у вас $A_1$ — это цельное имя, а потом $\{A_i\}_{i\in \{1, 2, 3\}}$ оказывается семейством.

Я пока смутно понимаю проблему, но думаю, что её можно исправить.

beroal в сообщении #1409363 писал(а):

но это следует из $(x, y, z)\in M$ и другой аксиомы

По идее ничего из других аксиом (во всяком случае аксиом этой же группы) в формулировке аксиомы следовать не должно.

-- 09.08.2019, 00:13 --

Впрочем, есть ещё стопроцентный бронебойный вариант, который был у меня в самом начале, но он уж совсем страшный.

$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to [([(B, A, C) \in M \ \vee \ (C, A, B) \in M] \ \wedge \ (A, B, C) \notin M \ \wedge \ (C, B, A) \notin M \wedge (A, C, B) \notin M \wedge (B, C, A) \notin M) \vee ... ]) $

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

[beroal]

Pennywise в сообщении #1409367 писал(а):

beroal в сообщении #1409363

wrote:
но это следует из $(x, y, z)\in M$ и другой аксиомы

По идее ничего из других аксиом (во всяком случае аксиом этой же группы) в формулировке аксиомы следовать не должно.

Я имел в виду, что в присутствии аксиомы $II_1$

$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! y \in \left\lbrace A, B, C \right\rbrace \exists x, z \in \left\lbrace A, B, C \right\rbrace ((x, y, z) \in M ))$
эквивалентно
$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! y \in \left\lbrace A, B, C \right\rbrace \exists x, z \in \left\lbrace A, B, C \right\rbrace ((x, y, z) \in M \land x\not =y\land y\not =z))$.

[Pennywise]

beroal, да, действительно. Понял, спасибо вам и Connector за помощь.

beroal в сообщении #1409371 писал(а):

$\forall A, B, C \in \Pi \ ([(\exists l \in \Delta (A, B, C \in l)) \wedge (A \neq B \wedge B \neq C \wedge A \neq C)] \to \exists ! y \in \left\lbrace A, B, C \right\rbrace \exists x, z \in \left\lbrace A, B, C \right\rbrace ((x, y, z) \in M \land x\not =y\land y\not =z))$

Я бы ещё добавил в конце $ \wedge \ x \neq z $ .