Принцип Винни-Пуха и всех-всех-всех в математической логике

[gevaraweb]

Известный мыслитель и медоед Винни-Пух как то сказал фразу:

Винни-Пух писал(а):

Хвост или есть, или его нет совсем.

Это глубокая, философская мысль, которая является истиной. В матлогике ей соответствует равенство:

$a \vee \bar{a} = 1$

Это равенство безымянно. Предлагаю впредь называть его принципом (или правилом, или равенством) Винни-Пуха в дань памяти и уважения к оному мыслителю. Впредь писать его в учебники. И легко теперь сказать студенту: воспользуйся правилом Винни Пуха.
Также предлагаю придумать и дать именованные названия к прочим равенствам матлогики.
Например:

$a \wedge \bar{a} = 0$

$a \vee {a} = a$

$a \wedge {a} = a$

$a \wedge 1 = a$

$a \vee 1 = 1$ sql-инъекция

$a \vee ( a \wedge {b} ) = a$
и пр.
Может названия у некоторых есть, но кто их помнит? Мы дадим лучше.

[Dmitriy40]

Вроде первое апреля уже прошло ...

[Munin]

gevaraweb в сообщении #1451517 писал(а):

Это равенство безымянно.

А название "правило исключённого третьего" вам ничего не говорит?

[gevaraweb]

Munin в сообщении #1451533 писал(а):

А название "правило исключённого третьего" вам ничего не говорит?

gevaraweb в сообщении #1451517 писал(а):

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

[Munin]

Название, отражающее смысл, всегда лучше названия по чьему-то имени.

[kotenok gav]

SQL-инъекция - это, скорее, $a\vee0=0$, если у нас цель получить 0, и $a\vee-a=1$, если у нас цель получить 1.

-- 05 апр 2020, 23:27 --

$a\wedge 0=0$, а вот 1 с И сделать не всегда возможно.

[arseniiv]

gevaraweb в сообщении #1451517 писал(а):

Это равенство безымянно.

LEM это. Все его знают под таким именем. Кроме тех, кто не знает. Что он даже не везде считается допустимым.

gevaraweb в сообщении #1451517 писал(а):

Впредь писать его в учебники.

Оно там есть, здрасьте.

gevaraweb в сообщении #1451517 писал(а):

sql-инъекция

Не надо. SQL-инъекция — это конкретная вещь, а у более общих классов ситуаций уже есть названия, и наконец это равенство не является единственно верным обобщением таких вещей. С тем же успехом можно взять двойственное $x\wedge0 = 0$, и они оба не в кассу, потому что скорее они, а точнее полугруппа с поглощающим элементом, описывают исключительную ситуацию или short-circuiting вычислений.

Откройте статью по булевой алгебре и почитайте как называются её аксиомы. Кроме того это не «равенства матлогики», матлогика вообще не есть булева алгебра и там говорили бы или о выводимости формул (и никаких тут знаков равенства) или об их значениях в различных интерпретациях, опять же лучше аккуратнее с равенствами (если только на уровне «$g(x)\to 3$ при $x\to 2$»).

-- Вс апр 05, 2020 18:16:24 --

Munin в сообщении #1451542 писал(а):

Название, отражающее смысл, всегда лучше названия по чьему-то имени.

+много

[Mihr]

gevaraweb, названия уже существуют, Вы опоздали.

$a \wedge \bar{a} = 0$ - закон противоречия

$a \vee {a} = a$ - закон идемпотентности (точнее: идемпотентность дизъюнкции)

$a \wedge {a} = a$ - закон идемпотентности (точнее: идемпотентность конъюнкции)

$a \wedge 1 = a$ - один из законов поглощения

$a \vee ( a \wedge {b} ) = a$ - кажется, закон Порецкого

[arseniiv]

Я слышал, что $x\wedge(x\vee y) = x = x\vee(x\wedge y)$ звали поглощением, а тождества с константами можно считать утверждениями о нейтральном (операция с ним даёт другой аргумент) и поглощающем элементах (операция с ним даёт его).

[Mihr]

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

Я слышал, что $x\wedge(x\vee y) = x = x\vee(x\wedge y)$ звали поглощением

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

[arseniiv]

В русской Википедии я вроде тоже сегодня увидел, но это как-то странно, отдаёт чем-то древним. Надо вспомнить, как называются в школьных учебниках $x + 0 = x$ и $x\cdot 1 = x$…

[Munin]

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

LEM это. Все его знают под таким именем.

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

[arseniiv]

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

В некоторых аксиоматиках аксиомы хорошо делятся на правила введения и удаления связок, вот например возьмём такую: https://en.wikipedia.org/wiki/Intuitionistic_logic#Hilbert-style_calculus. Там:
• правило Modus ponens (MP) — это удаление $\to$; введение $\to$ не входит в виде правила, но ему соответствует метатеорема о дедукции;
• AND-1, AND-2 — удаление $\wedge$, AND-3 — введение $\wedge$;
• OR-1, OR-2 — введение $\vee$, OR-3 — удаление $\vee$;
• FALSE — удаление $\bot$, а правила введения $\bot$ не дают по смыслу этой константы;
• аналогично если бы была аксиома TRUE: $\top$ — она была бы введением $\top$, а удаления не предусматривается;
• правило ∀-GEN — введение $\forall$, аксиома PRED-1 — удаление;
• правило ∃-GEN — удаление $\forall$, аксиома PRED-2 — введение;
• NOT-1′ можно вполне считать введением $\neg$, NOT-2′ удалением, хотя они просто являют переписывание $\neg\varphi$ как $\varphi\to\bot$;
• NOT-1 — снова введение $\neg$, NOT-2 — удаление, «менее читерские»;
• IFF-1, IFF-2 — снова «читерское» удаление $\leftrightarrow$, и IFF-3 — введение.

Дальше там предлагают добавить какую-нибудь аксиомку, чтобы логика стала классической, с их названиями, которые я сюда переписывать не стану. Если теперь вернуться к THEN-1 и THEN-2, они не являются ни введением, ни удалением $\to$, но их можно называть аксиомами K и S соответственно, ибо они есть в точности типы комбинаторов K и S.

В натуральном выводе введение и удаление импликации выходят намного естественнее (метатеорема о дедукции уже не метатеорема, а правило наряду с остальными, и эквиваленты аксиом K, S, являющиеся в некотором смысле её присутствием в системе, уже не нужны).

Если интересны названия аксиом всё же булевых алгебр, отошлю к https://en.wikipedia.org/wiki/Boolean_algebra_(structure).

-- Пн апр 06, 2020 13:03:55 --

Вообще же булевы алгебры лучше определять не длинными списками аксиом, а короткой фразой типа «[ограниченная] дистрибутивная решётка с дополнением» (ограниченность требуется дополнением, так что можно её не проговаривать), где в свою очередь решётка — это частичный порядок, у которого есть sup и inf любой пары элементов (которые и станут операциями $\vee, \wedge$). Дистрибутивность и дополнение можно обдумать в терминах порядка и получить картину не хуже чем идя от одних аксиом. И лучше (всем, ставящим «булеву» алгебру во главу угла, и я кошусь немного и в сторону ТС) знать, что это не какая-то уникальная штуковина, а уникальная штуковина со связями, в частности рядом с ней ещё будет стоять например алгебра Гейтинга (Heyting), ну и что это не только одна конкретная двухэлементная структура $\mathbb B$ (ой не все в курсе этого!).

По поводу логических систем: вот тут есть разные аксиоматизации вместе с авторством. Они больше к тому, что вы можете кого-нибудь попугать например «аксиомой Мередита» (хотя что конкретно это будет означать, зависит от того, какая из его аксиоматизаций и какой логики используется), и там ещё куча других аксиоматизаций с единственной аксиомой.

-- Пн апр 06, 2020 13:28:53 --

А, чего забыл дописать: «дистрибутивная решётка с дополнением» лучше в том же ключе, как и лучше определять модуль как абелеву группу $V$ вместе с морфизмом колец $K\to\operatorname{End}V$. Да, немного придётся распаковать, зато с этими понятиями идёт сразу их применимость, а с плоским списком аксиом ничего само собой не идёт — надо будет вывести всё самому (ну или почитать такой вывод) и нигде особо не посмотришь, в отличие от лёгкости поиска по терминам. Выводить конечно тоже полезно и частью придётся везде, но.

[Munin]

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

[arseniiv]

Ну там по ссылкам же. Elimination, introduction. Pierce’s law (на этом месте я уже явно отметил, что смотреть надо там). Связки понятно как называются. Ну что там ещё. Да, я конечно планировал писать английские, а как-то незаметно съехал на русские.