"Истина" - следите за руками. Виды логик.
Член-корр РАН Беклемишев (+ ещё доцент Кузнецов) читает лекции про теоремы о неполноте Гёделя. Лекции разбили на смысловые куски. И вот кусок, в котором вводится "истинность" утверждений - с 0:41:
https://www.youtube.com/watch?v=9JUnze3n_iU
0:41 / 10:01
3 Истинность и доказуемость, гёделева нумерация, парадокс лжеца
Vanechki: математика, биология и многое другое, 1 тыща просмотров, 7 мар. 2019 - 13,3 тыс. подписчиков
0) Плейлист с нарезкой лекций Беклемишева и Кузнецова: [Spoiler (click to open)]
===
https://www.youtube.com/playlist?list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj
Теорема Гёделя о неполноте. Беклемишев и Кузнецов
Vanechki: математика, биология и многое другое
20 видео 6 тыщ просмотров, Обновлен 29 мар. 2023
Полезно прочитать брошюру В.А. Успенского «Теорема Гёделя о неполноте»
http://math.ru/lib/plm/57 и статью «Теоремы Гёделя о неполноте и границы их применимости» http://www.mi-ras.ru/~bekl/Papers/goedel-uspehi.pdf
Лев Дмитриевич БЕКЛЕМИШЕВ - член-корреспондент РАН, главный научный сотрудник Математического института имени В.А. Стеклова, профессор кафедры математической логики и теории алгоритмов мехмата МГУ.
Лекция Малого мехмата МГУ 2.3.2019:
http://mmmf.msu.ru/lect/lect20.html
1) 33:15 - 1 Формальные аксиоматические теории
https://www.youtube.com/watch?v=Ixl2oZtxYe4&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=1
2) 6:19 - 2 Арифметика Пеано
https://www.youtube.com/watch?v=Nc0rfvQQpG4&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=2
3) 10:02 - 3 Истинность и доказуемость, гёделева нумерация, парадокс лжеца
https://www.youtube.com/watch?v=9JUnze3n_iU&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=3
4) 7:56 - 4 Идея Гёделя
https://www.youtube.com/watch?v=_Geyw06FSWc&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=4
5) 19:49 - 5 Первая теорема Гёделя о неполноте
https://www.youtube.com/watch?v=CwypqBF5iTg&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=5
6) 9:24 - 6 Парадокс Греллинга-Нельсона: рефлексивно ли слово НЕРЕФЛЕКСИВНЫЙ?
https://www.youtube.com/watch?v=5wSzzMKFY1U&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=6
7) 10:08 - 7 Напоминание (план доказательства первой теоремы Гёделя о неполноте)
https://www.youtube.com/watch?v=3XppJEYLYZQ&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=7
8) 15:14 - 8 Ограниченные кванторы. Сигма- и дельта-формулы, перечислимые и разрешимые множества
https://www.youtube.com/watch?v=Uw5WJKXX2Fc&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=8
9) 9:34 - 9 Нумерация пар натуральных чисел
https://www.youtube.com/watch?v=1ZrkSGqyY0I&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=9
10) 13:18 - 10 Конечные подмножества натурального ряда и двоичная система счисления
https://www.youtube.com/watch?v=2KgCyirmn-M&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=10
11) 18:00 - 11 Кодирование последовательностей, формул, выводов
https://www.youtube.com/watch?v=cKHGbC3kZEY&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=11
12) 52:32 - 12 Степени числа 2 и китайская теорема об остатках. Количество элементов множества и биекция
https://www.youtube.com/watch?v=VKYy3coL51E&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=12
13) 9:36 - 13 Парадокс лжеца и теорема Тарского о неарифметичности множества истинных высказываний
https://www.youtube.com/watch?v=6MzAZLeiSSU&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=13
14) 15:06 - 14 Теоремы Гёделя о неполноте
https://www.youtube.com/watch?v=Bl7cZfmL2e8&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=14
15) 11:40 - 15 Парадокс Карри и теорема Лёба
https://www.youtube.com/watch?v=B9jcLgn03yo&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=15
16) 19:34 - 16 Теорема о неподвижной точке
https://www.youtube.com/watch?v=7ci_pnh7Vyg&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=16
17) 7:43 - 17 Парадокс Берри и сложность описания
https://www.youtube.com/watch?v=Wgb7o6ijyCo&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=17
18) 13:42 - 18 Невычислимость сложности. Парадокс Берри и доказательство Чейтина первой теоремы Гёделя о неполно
https://www.youtube.com/watch?v=BjiD-fmJTIs&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=18
19) 5:48 - 19 Всюду определённые вычислимые функции
https://www.youtube.com/watch?v=YxvHWanKGKU&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=19
20) 50:19 - Доказуемость и недоказуемость
https://www.youtube.com/watch?v=kVI7WrqDIVE&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=20
===
1) Что сделал лектор? Он взял множество всех утверждений (как я понял - некой формальной системы, данной через аксиомы) - нарисовал условный круг с этими утверждениями. И разбил этот круг на 2 части - в одной "истинные" утверждения, в другой - "ложные". Т.е. других вариантов нет.
Я именно на этом моменте останавливаюсь - [Spoiler (click to open)]т.к. именно тут у меня был затык с тем, что шло дальше.
Ведь 1ая теорема Гёделя о неполноте формальной системы с определяемой на нём арифметикой (например, собственно арифметика Пеано) доказывает, что существует утверждение (формула), которое средствами такой формальной системы нельзя ни доказать, ни опровергнуть (доказать его отрицание).
И куда поместить такие утверждения в множество, которое уже разбито на 2 части - на "истинные" и "ложные" утверждения?
Как я понял (может не отслеживал внимательно), утверждают, что недоказуемое утверждение обязательно "истинно". Про то, что есть ещё и отрицание утверждения - которое тоже может быть "истинным" и попасть в "истинные" может именно отрицание - об этом не приходит в голову ни лекторам, ни слушателям. А почему бы не посчитать "истинным" отрицание такого утверждения? Изначально в мозги впечатался образ круга разделённого пополам как множества всех утверждений разделённого на "истинные" и "ложные" - и очень трудно перебороть желание заранее поместить недоказуемые утверждение именно в "истинные". Однако изнутри формальной системы мы на этот счёт ничего не может сказать - оно там недоказуемо, потому "истинным" может быть как само утверждение, а "ложным" его отрицание, так и наоборот: утверждение - "ложно", а его отрицание - "истинно".
Очень может быть, что, если добавить какие-то ещё аксиомы и сделать из старой формальной системы новую формальную систему, то в ней исходное утверждение будет доказуемым. (Так в расширении арифметики транфинитными числами доказывают непротиворечивость исходной арифметики.) Но делает ли это "истинной" такое утверждение в старой ФС?
Для таких недоказуемых утверждений приводят аналогию - 5 постулат Евклида/аксиому о параллельных прямых. Она не доказуема в элементарной геометрии, определённой без этой аксиомы. Потому про параллельные прямые можно ввести разные аксиомы - Евклида, Лобачевского. И будут получаться разные внутренне непротиворечивые геометрии.
Так и с недоказуемыми утверждениями - про них говорят, что их можно объявить новыми аксиомами. Или их отрицание. При этом не будет противоречия ни в том, ни в другом случае. Т.е. новая система останется такой же непротиворечивой, как и была до добавления этой аксиомы в любом варианте.
2) И так. Исходную картинку с множеством всех утверждений в данной формальной системе можно модифицировать. Оставить куски "истинных" и "ложных" утверждений, и выделить из них часть утверждений недоказуемых - про истинность и ложность которых ничего изнутри формальной системы нельзя доказать.
Однако дальше возможны варианты, которые можно ВЫБИРАТЬ - [Spoiler (click to open)]в зависимости от целей, вкусов, убеждений. И именно на этом месте, на мой взгляд, лучше разобраться в ассортименте выбора, чем пытаться сразу выбрать "самое правильное". "Самого правильного" не бывает, а бывает выбор из вариантов, с которыми просто стоит быть знакомыми, даже если выбирать будешь всё время что-то одно. Хотя бы для того, чтоб понимать место развилки - когда рассуждения упираются в варианты выбора логики. Пока же я сам с этими вариантами не очень знаком - общего представления не имею и сказать, что делать и как - не скажу.
2-1) В каких-то лекциях говорилось, что есть интуиционисты (и их вариант - конструктивисты - у них, как я понял, логика конечных алгоритмов). И они не принимают аксиому "закон исключения третьего". Вместо него ими используется только введение двойного отрицания без снятия двойного отрицания.
===
https://ru.wikipedia.org/wiki/Закон_исключённого_третьего
Закон исключённого третьего [Spoiler (click to open)](лат. tertium non datur, то есть «третьего не дано») - закон классической логики, который формулируется следующим образом: два противоречащих суждения не могут быть оба ложными, одно из них будет истинно: а есть либо b, либо не b. Истинно либо утверждение некоторого факта, либо его отрицание. Третьего не дано.[1]
[Spoiler (click to open)]В отличие от закона противоречия, который действует по отношению ко всем несовместимым друг с другом суждениям, закон исключенного третьего действует только в отношении противоречащих (контрадикторных) суждений.
С «интуиционистской» (и, в частности, «конструктивистской») точки зрения установление истинности высказывания вида «А или не А» означает:
либо установление истинности A;
либо установление истинности его отрицания ┐A.
Поскольку, вообще говоря, не существует общего метода, позволяющего для любого высказывания за конечное число шагов установить его истинность или истинность его отрицания, закон исключённого третьего не должен применяться в рамках интуиционистского и конструктивного направлений в математике как аксиома.
Формулировка [Spoiler (click to open)]
В математической логике закон исключённого третьего выражается тождественно истинной формулой[2]:
A∨┐A, где: ∨ - знак дизъюнкции; ┐ - знак отрицания.
Другие формулировки [Spoiler (click to open)]
Подобный смысл имеют другие логические законы, многие из которых сложились исторически.
В частности, закон двойного отрицания ┐(┐A)→ A и закон Пирса ((P→Q)→P)→P эквивалентны закону исключённого третьего в интуиционистской логике. Это означает, что расширение системы аксиом интуиционистской логики любым из этих трёх законов в любом случае приводит к классической логике. И всё же, в общем случае, существуют логики, в которых все три закона неэквивалентны[3].
[3] Zena M. Ariola and Hugo Herbelin. Minimal classical logic and control operators. In Thirtieth International Colloquium on Automata, Languages and Programming , ICALP’03, Eindhoven, The Netherlands, June 30 - July 4, 2003, volume 2719 of Lecture Notes in Computer Science, pages 871-885. Springer-Verlag, 2003.[1] Архивная копия от 18 июля 2008 на Wayback Machine
Примеры [Spoiler (click to open)]
…Гораздо более тонкий пример применения закона исключённого третьего, который хорошо демонстрирует, почему он не является приемлемым с точки зрения интуиционизма, состоит в следующем. Предположим, что мы хотим доказать теорему, что существуют иррациональные числа a и b такие, что a^b рационально.
Известно, что √2 иррациональное число (доказательство). Рассмотрим число:√2^√2.
Очевидно (исключая третий вариант), что это число либо рационально, либо иррационально. Если данное число рационально, то теорема доказана. Искомые числа: a=√2 b=√2
√2^√2 является иррациональным, тогда пусть a=√2^√2 и b=√2. Следовательно,
=a^b=(√2^(√2))^√2=√2^(√2∙√2)=(√2)^2=2,
то есть a^b - рациональное число.
По закону исключённого третьего иных вариантов быть не может. Поэтому теорема в общем случае доказана. Причём доказательство предельно просто и элементарно. С другой стороны, если принять интуиционистскую точку зрения и отказаться от закона исключённого третьего, теорема хотя и может быть доказана, но доказательство её становится исключительно сложным.
===
2-2) При этом отдельно есть "закон противоречия", который интуиционисты считают выполняющимся:
===
https://ru.wikipedia.org/wiki/Закон_противоречия
Закон противоречия [Spoiler (click to open)](закон непротиворечия) - закон логики, который гласит, что два несовместимых (противоречащих или противоположных) суждения не могут быть одновременно истинными - по крайней мере одно из них ложно[1].
Математическая запись в виде формулы, всегда имеющей ложное значение[2]:
P∧┐P, где: ∧ - знак конъюнкции (И); ┐ - знак отрицания.
Закон противоречия является фундаментальным логическим законом, на котором построена вся современная математика. Его отрицание является тавтологией классической логики, а также большинства неклассических логик, в том числе интуиционистской логики. Всё же существуют нетривиальные логические системы, в которых он не соблюдается, например, логика Клини.
===
Т.е.
A∧┐A = всегда ложь, в классической логике и для интуиционистов
A∨┐A - всегда истина, в классической логике, но не для интуиционистов, для них возможны другие варианты.
2-3) Различия классической и интуиционистской логики в законах двойного отрицания - для интуиционистов работает только закон введения двойного отрицания, а остальные не работают. [Spoiler (click to open)]А конструктивисты к тому, что они интуиционисты ещё добавляют конечность шагов алгоритма вывода, что проясняет смысл того, почему отрицание отрицания не получится снять: когда есть бесконечный перебор невозможно сделать его конечным. Это следует из преобразования отрицания с кванторами (в логике 1 порядка).
┐A(x)↔∃x,┐A(x) - отрицание какого-то А(х) - это существование хотя бы одного х, при котором А(х) будет ложным
┐∃x,B(x)↔∀x,┐B(x) - отрицание существования хотя бы одного х, при котором выполняется В(х) - это невыполнение В(х) для любого х.
В конструктивной логике не признаётся возможным бесконечный перебор - алгоритм вывода должен быть только конечным, а что будет в других случаях, как я понимаю - "неизвестно".
А в интуиционистской логике работает A→┐(┐A), а в обратную сторону - нет: ┐(┐A)→A, потому как полагается, что кроме А и не А может быть что-то ещё - не работает закон исключения третьего.
===
https://ru.wikipedia.org/wiki/Закон_двойного_отрицания
[Spoiler (click to open)]положенный в основу классической логики принцип, согласно которому «если неверно, что неверно А, то А верно». Есть 3 формулировки закона двойного отрицания. В формализованном языке логики высказываний они выражаются формулами:
A→┐(┐A) - закон введения двойного отрицания;
┐(┐A)→A - закон снятия двойного отрицания;
A↔┐(┐A) - полный закон двойного отрицания.
В интуиционистской логике выводится лишь закон введения двойного отрицания, закон снятия же не выводится.
[Spoiler (click to open)]В традиционной содержательной математике закон двойного отрицания служит логическим основанием для проведения так называемых доказательств от противного по следующей схеме: из предположения, что суждение А данной математической теории неверно, выводится противоречие в этой теории, затем на основании непротиворечивости теории делается вывод, что неверно «не А», и тогда по закону снятия двойного отрицания заключают, что верно А. В рамках конструктивных рассмотрений, когда действует требование алгоритмической реализуемости обоснования математических суждений, закон снятия двойного отрицания оказывается, вообще говоря, неприемлемым.
Типичным тому примером служит всякое доказательство от противного суждения А, имеющего вид «при всяком х существует у такой, что верно В(х, у)», когда последний шаг, состоящий в применении закона снятия двойного отрицания, оказывается невозможным из-за того, что конструктивное понимание суждения требует для его обоснования построения алгоритма, который по каждому х давал бы конструкцию у такого, что верно В(х, у). Между тем рассуждение с применением закона снятия двойного отрицания не приводит к построению какого бы то ни было алгоритма; более того, искомого в этом случае алгоритма может вообще не существовать (см. также принцип конструктивного подбора).
Другие формулировки [Spoiler (click to open)]
Закон снятия двойного отрицания тесно связан с законом исключённого третьего, а также с так называемым законом Пирса. В определённом смысле все три закона эквивалентны. Так, в интуиционистском исчислении высказываний, где эти законы не являются тавтологиями, каждый из этих двух законов выводим из другого, а добавление любого из них в аксиоматику сразу приводит к классической логике. При этом однако, существуют логики, в которых все три закона неэквивалентны[1].
Для интуиционистской логики есть более слабая форма для закона снятия - закон снятия тройного отрицания:
┐(┐(┐A))→(┐A).
===
2-4) Дальше стоит ознакомиться с различием подходов классической логики и интуиционистов+конструктивистов в отношении доказательства от противного (и сведения к абсурду):
===
https://ru.wikipedia.org/wiki/Доказательство_от_противного
[Spoiler (click to open)]вид доказательства, при котором «доказывание» некоторого суждения (тезиса доказательства) осуществляется через опровержение отрицания этого суждения - антитезиса[2]. Этот способ доказательства основывается на истинности закона двойного отрицания в классической логике.
Схема доказательства [Spoiler (click to open)]
…
Доказательство утверждения А проводится следующим образом. Сначала принимают предположение, что утверждение А неверно, а затем доказывают, что при таком предположении было бы верно некоторое утверждение В, которое заведомо неверно.
Из определения импликации следует, что, если В ложно, то формула ┐А→В истинна тогда и только тогда, когда ┐A ложно, следовательно утверждение А истинно.
Полученное противоречие показывает, что исходное предположение было неверным, и поэтому верно утверждение ┐┐A, которое по закону двойного отрицания равносильно утверждению А.
Это рассуждение можно заменить следующим рассуждением, состоящим из двух частей: первая часть представляет собой доказательство утверждения ┐┐A приведением к нелепости (reductio ad absurdum), а вторая - переход к утверждению А снятием двойного отрицания. Поскольку, хотя и неявно, используется классическое правило снятия двойного отрицания, метод доказательства от противного является классическим и служит источником неэффективных доказательств теорем существования. О сущности различий между этими правилами написано далее в данной статье.
В интуиционистской логике доказательство от противного не принимается, так же как не действует закон исключённого третьего[1].
[1] [Spoiler (click to open)]Косвенное доказательство//Философия: Энциклопедический словарь. - М.: Гардарики. Под редакцией А. А. Ивина. 2004.
Замечание. Данная схема похожа на другую - на схему доказательства приведением к нелепости. В связи с этим их часто путают. Однако несмотря на некоторое сходство, они имеют разную форму. Причём различаются они не только по форме, но и по существу, и различие это носит принципиальный характер.
Сопоставление методов доказательства от противного и приведением к нелепости [Spoiler (click to open)]
…[Я: схемы смотреть в Википедии,
в док-ве от противного из вывода противоречия из отрицания А двойным отрицанием выводится А,
а в доведении до нелепости/абсурда - из самого А выводится противоречие и нет двойного отрицания]…
К сожалению, обычно в практике преподавания, а также в печатных изданиях - учебных, методических и научных - авторы не различают эти две схемы, два способа доказательства, чаще всего называя и тот и другой доказательством от противного.
Остановимся на причинах того, почему всё же следует различать эти схемы.
Во-первых, очевидно, что эти схемы отличаются чисто графически, а значит, рассуждения по этим схемам различаются по форме. Различия такого же характера, т. е. по крайней мере по форме, имеются между предложениями А и ┐┐A (или между предложениями А→В и ┐А∨В). Даже если, находясь на классических позициях, мы считаем, что эти утверждения равносильны, то всё равно факт различия по форме является очевидным.
Однако такое различие может кому-то показаться недостаточным, неубедительным для того, чтобы затевать весь этот разговор. Естественно, возникают вопросы: не равносильны ли эти схемы; в чём выражается различие между ними в практике математических доказательств; это различие лишь по форме или также по существу?
…
Доказывая методом от противного, мы используем более сильные логические средства, чем когда доказываем приведением к нелепости. Это вызвано тем, что доказательство от противного существенно опирается на правило снятия двойного отрицания, а доказательство приведением к нелепости нет. Именно благодаря этому обстоятельству различие между схемами contradictio in contrarium и reductio ad absurdum - это различие не только по форме, но и по существу. Более того, это различие тесно связано с некоторыми проблемами оснований математики.
Дело в том, что такие логические законы, как закон исключённого третьего А∨┐A, закон снятия двойного отрицания ┐(┐A)→A, схема доказательства от противного ((┐A→В)∧(┐A→┐В))→А, приводят к неэффективным конструкциям и доказательствам в математике. В первую очередь это относится к доказательствам так называемых теорем существования, т. е. теорем вида: «Существует x такой, что Р(х)»: ∃х,Р(х), где Р(х) - некоторое свойство Р, которое выполняется для x, причём x пробегает некоторое множество известных объектов (чисел, формул, множеств формул, и т. п.).
Эффективным доказательством теоремы вида ∃х,Р(х) называется построение объекта x (или способа, позволяющего построить этот объект) и доказательство того, что этот объект действительно обладает требуемым свойством Р. Доказательство теоремы существования, не удовлетворяющее этим условиям, считают неэффективным.
Типичным неэффективным доказательством теоремы существования является доказательство методом от противного. Действительно, пусть требуется доказать утверждение вида ∃х,Р(х) - «существует объект x, обладающий свойством Р». Допустим, что ┐∃х,Р(х). Путём рассуждений получаем некоторое противоречие: В и ┐В. Отсюда, в силу схемы reductio ad absurdum, делаем вывод, что допущение неверно, т. е. ┐┐∃х,Р(х). Далее, снимая двойное отрицание, получим ∃х,Р(х) и считаем доказательство завершённым. Однако такое доказательство не завершается построением хотя бы одного объекта с требуемым свойством, оно нисколько не приближает нас к построению примера такого x, что Р(х), т. е. является неэффективным доказательством.
Примерами доказательств такого вида служат доказательства теорем: теоремы об ограниченности непрерывной на отрезке функции (т. е. о существовании верней и нижней границ непрерывной на отрезке функции); теоремы о существовании наибольшего и наименьшего значений у непрерывной на отрезке функции. Традиционное доказательство этих теорем методом от противного не содержит конструкции, позволяющей построить объект, о существовании которого идёт речь в теореме.
Неэффективные доказательства теорем существования признаются не всеми математиками. Для математиков, стоящих на традиционных классических позициях, характерным является признание без всяких ограничений закона исключённого третьего А∨┐A и закона снятия двойного отрицания ┐(┐A)→A. Они пренебрегают различиями между утверждениями ∃х,Р(х) и ┐┐∃х,Р(х). Математики, не придерживающиеся классических взглядов (интуиционисты и конструктивисты), отрицают универсальность этих законов. Различия между утверждениями ∃х,Р(х) и ┐┐∃х,Р(х) такие математики признают весьма существенными, считая утверждение ┐┐∃х,Р(х), вообще говоря, более слабым, чем ∃х,Р(х). Доказательство от противного, с их точки зрения, также является неприемлемым, поскольку оно опирается на принцип снятия двойного отрицания.
Таким образом, различие между схемами contradictio in contrarium и reductio ad absurdum носит методологический характер, затрагивая проблему разного понимания утверждений о существовании в математике, а также связанные с этим другие проблемы оснований математики.
Идея построения основных разделов математики на эффективной основе, без использования закона снятия двойного отрицания и закона исключенного третьего восходит к интуиционистской концепции Л. Э. Я. Брауэра. Интуиционистское направление в математике бурно развивалось на протяжении всего XX в. Существенное развитие неклассические идеи получили в работах представителей школы конструктивного направления в математике во главе с А. А. Марковым - выдающимся советским математиком (1903-1979).
===
2-5) Интуиционисты:
===
https://ru.wikipedia.org/wiki/Интуиционистская_логика
Интуициони́стская ло́гика - [Spoiler (click to open)]формальная система, отражающая некоторые способы рассуждений, приемлемые с точки зрения интуиционизма. Предложена А. Гейтингом в 1930.
Основное отличие от привычного исчисления высказываний заключается в том, что отсутствует закон исключённого третьего.
Схемы аксиом 1-10 и правило «модус поненс» задают интуиционистское исчисление высказываний. Все 12 схем аксиом и все 3 правила вывода задают интуиционистское исчисление предикатов. Интуиционистское исчисление предикатов отличается от классического тем, что в последнем вместо схемы аксиом 10 используется схема аксиом ┐(┐A)→A.[1]. [Spoiler (click to open)][1] В. Е. Плиско Интуиционистская логика. - Математический энциклопедический словарь. - М., Советская энциклопедия, 1988. - Тираж 150 000 экз. - c. 243
Логические символы
∧ (знак конъюнкции), ∨ (знак дизъюнкции), → (знак импликации) и ┐ (знак отрицания).
Схемы аксиом [Spoiler (click to open)]
Далее через A, B и C обозначаются произвольные пропозициональные формулы.
1) (A→(B→A))
2) ((A→B)→((B→C)→(A→C)))
3) (A→(B→(A∧B)))
4) ((A∧B)→A)
5) ((A∧B)→B)
6) (A→(A∨B))
7) (B→(A∨B))
8) ((A→C)→((B→C)→((A∨B)→C)))
9) ((A→B)→((A→(┐B))→(┐A)))
10) ((┐A)→(A→B))
11) ∀xA(x)→A(y)
12) A(y)→∃xA(x)
Правила вывода [Spoiler (click to open)]
1) Modus ponens:
A,(A→B)
B
2)
C→A(x)
C→∀xA(x)
если x не является свободной переменной в C.
3)
A(x)→C
∃xA(x)→C
если x не является свободной переменной в C.
===
https://ru.wikipedia.org/wiki/Интуиционизм
Интуициони́зм - [Spoiler (click to open)]совокупность философских и математических взглядов, рассматривающих математические суждения с позиций «интуитивной убедительности». Различаются две трактовки интуиционизма: интуитивная убедительность, которая не связана с вопросом существования объектов, и наглядная умственная убедительность.
В интуиционистской математике отвергается подход классической теории множеств (в частности, не принимаются аксиома выбора и аксиома регулярности) и ряд рассуждений классической логики. Абстракция потенциальной осуществимости, которая используется в интуиционистской математике, лучше соотносится с действительностью, чем абстракция актуальной бесконечности.
Исторический очерк
Критика теории множеств привела к возникновению трёх течений: интуиционизма Лёйтзена Эгберта Яна Брауэра, формализма Давида Гильберта и логицизма Готлоба Фреге, Бертрана Рассела, Альфреда Норта Уайтхеда. …
Интуиционистская логика
В интуиционистской математике суждение считается истинным, только если его можно доказать некоторым «мысленным экспериментом». То есть истинность утверждения «Существует объект x, для которого верно суждение A(x)» доказывается построением такого объекта, а истинность утверждения «A или B» доказывается либо доказательством истинности утверждения A, либо доказательством истинности утверждения B. Отсюда, в частности, следует, что утверждение «A или не A» может быть не истинным, а закон исключённого третьего неприемлем. Истинным математическим суждением является ряд выполненных построений эффективного характера с использованием интуиционистской логики. Эффективность не обязательно связана с наличием алгоритма и может зависеть от физических и исторических факторов, фактического решения проблем[1]. …
Интуиционизм и другие математические подходы
…Значительное влияние друг на друга оказали концепции формализма и интуиционизма.
…В широкой трактовке конструктивное направление математики можно рассматривать как часть интуиционистской математики[1].
===
2-6) Конструктивисты.
===
https://ru.wikipedia.org/wiki/Конструктивная_логика
[Spoiler (click to open)]одно из направлений современной математической логики, которая исходит из принципов конструктивной математики и результатов критической переработки рациональных положений интуиционистской логики.
Конструктивисты, так же как и интуиционисты не принимают понятие абстракции актуальной бесконечности, то есть бесконечности, завершённой, видя в ней слишком сильную идеализацию, и проводят свои исследования в рамках абстракции потенциальной осуществимости, признающей незавершённую, становящуюся бесконечность, которую, следовательно нельзя рассматривать как что-то готовое и законченное.
Бесконечное множество, говорят они, бесконечно лишь в том смысле, что его можно неограниченно продолжать конструировать. …
Исследование в конструктивной логике ограничивается исследованием конструктивных объектов, существование которых лишь тогда считается доказанным, когда указывается способ потенциально осуществимого построения (конструирования) этих объектов. Конструктивная логика считает неправильным перенос принципов, применяемых в области конечных множеств, на область бесконечных множеств.
В конструктивной логике в операциях с бесконечными множествами не применяется закон исключённого третьего. Конструктивисты это объясняют тем, что в операциях, включающих в себя бесконечные множества, которые находятся в процессе становления, невозможно определить, какова будет последующая альтернатива. Правда, также как и интуиционисты, они не отрицают применимость закона исключённого третьего по отношению к конечным областям.
Но принимая некоторые положения интуиционистской логики, конструктивная логика несводима к интуиционистской логике. …
===
Выше не включил в цитату советскую борьбу с "субъективистами" и "верой в реальность божества", как политически мотивированную муть. Меня тут не интересует взгляды сов.власти. Из ссылок к статье только 1 на статью из энциклопедии после 1991 года - лежащей на сайте ИФ РАН - там статья адекватнее:
===
https://iphlib.ru/library/collection/newphilenc/document/HASH0171caea6f531bf148fa0371
КОНСТРУКТИВНАЯ ЛОГИКА - [Spoiler (click to open)]совокупность логических принципов, признаваемых представителями конструктивизма (в математике) и включающих абстракцию потенциальной, но не актуальной бесконечности, что определенным образом изменяет понимание логических связок и кванторов (по сравнению с их пониманием в классической логике), сочетая это понимание с конструктивными процессами (процессами, описываемыми алгоритмами). Так, дизъюнкция высказываний «А или B» считается обоснованной, если потенциально осуществим конструктивный процесс, позволяющий выбрать верный член этой дизъюнкции; аналогично оценивается обоснованность многочленных дизъюнкций. Близко к пониманию дизъюнкции истолкование квантора существования: утверждение «существует такой х, для которого справедливо условие А» считается обоснованным, если потенциально осуществим конструктивный процесс подбора конструктивного объекта х, подтверждающего условие А. Обоснование конъюнкции «А и В» состоит в обосновании обоих (т.е. всех) конъюнктивных членов, а утверждение «Для всякого x справедливо условие А» считается обоснованным, если мы в состоянии для всякого объекта рассматриваемого вида доказать, что он удовлетворяет предъявленному требованию. Обоснование импликации «если А, то В» состоит в предъявлении конструктивного процесса, позволяющего по обоснованию утверждения А построить обоснование утверждения В. Отрицание утверждения А обосновывается предъявлением конструкции, приводящей к противоречию всякую попытку обоснования A.
Конструктивное истолкование логических связок и кванторов допускает и различные другие уточнения. В частности, созданы различные аксиоматические системы конструктивной логики. Поскольку конструктивная позиция идейно близка интуиционистской, аксиоматические системы, первоначально предназначавшиеся для реконструкции интуиционистски приемлемых рассуждений (см. Интуиционистская логика), называются (или подразумеваются) конструктивными. … Отличие этих логик от классической проявляется в том, что хотя конструктивно приемлемыми являются, напр., законы p→¬¬p, ¬¬¬p→¬p, (p→q)→(¬q→¬p), в этих системах отсутствуют практически все остальные варианты форм рассуждений «от противного» - закон снятия двойного отрицания ¬¬p→p, закон контрапозиции (¬р→¬q) →(q → p), закон Клавия (¬p→p) → p, закон Пирса ((p→q) → p) → p и др. Кроме того, в конструктивной логике связки независимы, т.е. не выражаются друг через друга, нет классической взаимовыразимости кванторов всеобщности и существования. В результате оказываются, в частности, необоснованными рассуждения, приводящие к доказательству т.н. чистых теорем существования, типичным примером которых является доказательство Г.Кантора существования трансцендентных (т.е. действительных, но не алгебраических) чисел…
===
3) на 4:00 - краткая схема доказательства 1й теоремы Гёделя о неполноте. [Spoiler (click to open)]
G - специальное утверждение в нашей формальной системе, такое что:
G ↔ "G не доказуемо". Это определение для G - т.е. G - это утверждение "G не доказуемо". оно "истинное" по определению.
Пусть недоказуемость G = ложности G, тогда:
G ↔ "G ложно". Это парадокс лжеца. А значит предположение, что недоказуемость G = ложности G - ложное. Т.е. так доказывается недоказуемость G, при условии его истинности. Осталось только подобрать такое G - что и сделал Гёдель, пронумеровав все утверждения в арифметике Пеано и сделав утверждение о номере утверждения.
А про утверждение G ↔ "G ложно" на 5:00 лектор говорит, что такое утверждение не может быть ни "истинным", ни "ложным". Но при этом ничего не меняет в картинке множества всех утверждений формальной системы - не добавляет 3ю область "не истинных и не ложных" утверждений.
И вот это то самое место, где у меня вопросы. Если разделили множество возможных утверждении только на 2 части: "истинные" и "ложные", и вдруг выяснили, что есть ещё и утверждения "не истинные и не ложные одновременно", то не означает ли это, что исходное разбиение множества только на "истинные" и на "ложные" утверждения само ложно, т.к. не включает утверждения без истинности и ложности? Как раз от каких-то таких рассуждений я интуитивно приходил к отрицанию "закона исключения третьего". Тем более, что в компьютерной логике на базах данных (SQL), есть это третье - Unknown/Empty/Error. Но до интиуционистской логики не доходил, т.к. не доходил до аксиоматического построения логики. Т.е. сейчас дошёл до того места, на котором останавливался раньше. И теперь знаю, как разбираться дальше - через аксиомы. И теперь знаю, что в этом уже разобрались - можно просто ознакомиться с готовыми результатами.
https://www.youtube.com/watch?v=9JUnze3n_iU
0:41 / 10:01
3 Истинность и доказуемость, гёделева нумерация, парадокс лжеца
Vanechki: математика, биология и многое другое, 1 тыща просмотров, 7 мар. 2019 - 13,3 тыс. подписчиков
0) Плейлист с нарезкой лекций Беклемишева и Кузнецова: [Spoiler (click to open)]
===
https://www.youtube.com/playlist?list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj
Теорема Гёделя о неполноте. Беклемишев и Кузнецов
Vanechki: математика, биология и многое другое
20 видео 6 тыщ просмотров, Обновлен 29 мар. 2023
Полезно прочитать брошюру В.А. Успенского «Теорема Гёделя о неполноте»
http://math.ru/lib/plm/57 и статью «Теоремы Гёделя о неполноте и границы их применимости» http://www.mi-ras.ru/~bekl/Papers/goedel-uspehi.pdf
Лев Дмитриевич БЕКЛЕМИШЕВ - член-корреспондент РАН, главный научный сотрудник Математического института имени В.А. Стеклова, профессор кафедры математической логики и теории алгоритмов мехмата МГУ.
Лекция Малого мехмата МГУ 2.3.2019:
http://mmmf.msu.ru/lect/lect20.html
1) 33:15 - 1 Формальные аксиоматические теории
https://www.youtube.com/watch?v=Ixl2oZtxYe4&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=1
2) 6:19 - 2 Арифметика Пеано
https://www.youtube.com/watch?v=Nc0rfvQQpG4&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=2
3) 10:02 - 3 Истинность и доказуемость, гёделева нумерация, парадокс лжеца
https://www.youtube.com/watch?v=9JUnze3n_iU&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=3
4) 7:56 - 4 Идея Гёделя
https://www.youtube.com/watch?v=_Geyw06FSWc&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=4
5) 19:49 - 5 Первая теорема Гёделя о неполноте
https://www.youtube.com/watch?v=CwypqBF5iTg&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=5
6) 9:24 - 6 Парадокс Греллинга-Нельсона: рефлексивно ли слово НЕРЕФЛЕКСИВНЫЙ?
https://www.youtube.com/watch?v=5wSzzMKFY1U&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=6
7) 10:08 - 7 Напоминание (план доказательства первой теоремы Гёделя о неполноте)
https://www.youtube.com/watch?v=3XppJEYLYZQ&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=7
8) 15:14 - 8 Ограниченные кванторы. Сигма- и дельта-формулы, перечислимые и разрешимые множества
https://www.youtube.com/watch?v=Uw5WJKXX2Fc&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=8
9) 9:34 - 9 Нумерация пар натуральных чисел
https://www.youtube.com/watch?v=1ZrkSGqyY0I&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=9
10) 13:18 - 10 Конечные подмножества натурального ряда и двоичная система счисления
https://www.youtube.com/watch?v=2KgCyirmn-M&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=10
11) 18:00 - 11 Кодирование последовательностей, формул, выводов
https://www.youtube.com/watch?v=cKHGbC3kZEY&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=11
12) 52:32 - 12 Степени числа 2 и китайская теорема об остатках. Количество элементов множества и биекция
https://www.youtube.com/watch?v=VKYy3coL51E&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=12
13) 9:36 - 13 Парадокс лжеца и теорема Тарского о неарифметичности множества истинных высказываний
https://www.youtube.com/watch?v=6MzAZLeiSSU&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=13
14) 15:06 - 14 Теоремы Гёделя о неполноте
https://www.youtube.com/watch?v=Bl7cZfmL2e8&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=14
15) 11:40 - 15 Парадокс Карри и теорема Лёба
https://www.youtube.com/watch?v=B9jcLgn03yo&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=15
16) 19:34 - 16 Теорема о неподвижной точке
https://www.youtube.com/watch?v=7ci_pnh7Vyg&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=16
17) 7:43 - 17 Парадокс Берри и сложность описания
https://www.youtube.com/watch?v=Wgb7o6ijyCo&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=17
18) 13:42 - 18 Невычислимость сложности. Парадокс Берри и доказательство Чейтина первой теоремы Гёделя о неполно
https://www.youtube.com/watch?v=BjiD-fmJTIs&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=18
19) 5:48 - 19 Всюду определённые вычислимые функции
https://www.youtube.com/watch?v=YxvHWanKGKU&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=19
20) 50:19 - Доказуемость и недоказуемость
https://www.youtube.com/watch?v=kVI7WrqDIVE&list=PL1JJ1jVZ9z5Cn0T1Tfz32oWOv2WzuC4gj&index=20
===
1) Что сделал лектор? Он взял множество всех утверждений (как я понял - некой формальной системы, данной через аксиомы) - нарисовал условный круг с этими утверждениями. И разбил этот круг на 2 части - в одной "истинные" утверждения, в другой - "ложные". Т.е. других вариантов нет.
Я именно на этом моменте останавливаюсь - [Spoiler (click to open)]т.к. именно тут у меня был затык с тем, что шло дальше.
Ведь 1ая теорема Гёделя о неполноте формальной системы с определяемой на нём арифметикой (например, собственно арифметика Пеано) доказывает, что существует утверждение (формула), которое средствами такой формальной системы нельзя ни доказать, ни опровергнуть (доказать его отрицание).
И куда поместить такие утверждения в множество, которое уже разбито на 2 части - на "истинные" и "ложные" утверждения?
Как я понял (может не отслеживал внимательно), утверждают, что недоказуемое утверждение обязательно "истинно". Про то, что есть ещё и отрицание утверждения - которое тоже может быть "истинным" и попасть в "истинные" может именно отрицание - об этом не приходит в голову ни лекторам, ни слушателям. А почему бы не посчитать "истинным" отрицание такого утверждения? Изначально в мозги впечатался образ круга разделённого пополам как множества всех утверждений разделённого на "истинные" и "ложные" - и очень трудно перебороть желание заранее поместить недоказуемые утверждение именно в "истинные". Однако изнутри формальной системы мы на этот счёт ничего не может сказать - оно там недоказуемо, потому "истинным" может быть как само утверждение, а "ложным" его отрицание, так и наоборот: утверждение - "ложно", а его отрицание - "истинно".
Очень может быть, что, если добавить какие-то ещё аксиомы и сделать из старой формальной системы новую формальную систему, то в ней исходное утверждение будет доказуемым. (Так в расширении арифметики транфинитными числами доказывают непротиворечивость исходной арифметики.) Но делает ли это "истинной" такое утверждение в старой ФС?
Для таких недоказуемых утверждений приводят аналогию - 5 постулат Евклида/аксиому о параллельных прямых. Она не доказуема в элементарной геометрии, определённой без этой аксиомы. Потому про параллельные прямые можно ввести разные аксиомы - Евклида, Лобачевского. И будут получаться разные внутренне непротиворечивые геометрии.
Так и с недоказуемыми утверждениями - про них говорят, что их можно объявить новыми аксиомами. Или их отрицание. При этом не будет противоречия ни в том, ни в другом случае. Т.е. новая система останется такой же непротиворечивой, как и была до добавления этой аксиомы в любом варианте.
2) И так. Исходную картинку с множеством всех утверждений в данной формальной системе можно модифицировать. Оставить куски "истинных" и "ложных" утверждений, и выделить из них часть утверждений недоказуемых - про истинность и ложность которых ничего изнутри формальной системы нельзя доказать.
Однако дальше возможны варианты, которые можно ВЫБИРАТЬ - [Spoiler (click to open)]в зависимости от целей, вкусов, убеждений. И именно на этом месте, на мой взгляд, лучше разобраться в ассортименте выбора, чем пытаться сразу выбрать "самое правильное". "Самого правильного" не бывает, а бывает выбор из вариантов, с которыми просто стоит быть знакомыми, даже если выбирать будешь всё время что-то одно. Хотя бы для того, чтоб понимать место развилки - когда рассуждения упираются в варианты выбора логики. Пока же я сам с этими вариантами не очень знаком - общего представления не имею и сказать, что делать и как - не скажу.
2-1) В каких-то лекциях говорилось, что есть интуиционисты (и их вариант - конструктивисты - у них, как я понял, логика конечных алгоритмов). И они не принимают аксиому "закон исключения третьего". Вместо него ими используется только введение двойного отрицания без снятия двойного отрицания.
===
https://ru.wikipedia.org/wiki/Закон_исключённого_третьего
Закон исключённого третьего [Spoiler (click to open)](лат. tertium non datur, то есть «третьего не дано») - закон классической логики, который формулируется следующим образом: два противоречащих суждения не могут быть оба ложными, одно из них будет истинно: а есть либо b, либо не b. Истинно либо утверждение некоторого факта, либо его отрицание. Третьего не дано.[1]
[Spoiler (click to open)]В отличие от закона противоречия, который действует по отношению ко всем несовместимым друг с другом суждениям, закон исключенного третьего действует только в отношении противоречащих (контрадикторных) суждений.
С «интуиционистской» (и, в частности, «конструктивистской») точки зрения установление истинности высказывания вида «А или не А» означает:
либо установление истинности A;
либо установление истинности его отрицания ┐A.
Поскольку, вообще говоря, не существует общего метода, позволяющего для любого высказывания за конечное число шагов установить его истинность или истинность его отрицания, закон исключённого третьего не должен применяться в рамках интуиционистского и конструктивного направлений в математике как аксиома.
Формулировка [Spoiler (click to open)]
В математической логике закон исключённого третьего выражается тождественно истинной формулой[2]:
A∨┐A, где: ∨ - знак дизъюнкции; ┐ - знак отрицания.
Другие формулировки [Spoiler (click to open)]
Подобный смысл имеют другие логические законы, многие из которых сложились исторически.
В частности, закон двойного отрицания ┐(┐A)→ A и закон Пирса ((P→Q)→P)→P эквивалентны закону исключённого третьего в интуиционистской логике. Это означает, что расширение системы аксиом интуиционистской логики любым из этих трёх законов в любом случае приводит к классической логике. И всё же, в общем случае, существуют логики, в которых все три закона неэквивалентны[3].
[3] Zena M. Ariola and Hugo Herbelin. Minimal classical logic and control operators. In Thirtieth International Colloquium on Automata, Languages and Programming , ICALP’03, Eindhoven, The Netherlands, June 30 - July 4, 2003, volume 2719 of Lecture Notes in Computer Science, pages 871-885. Springer-Verlag, 2003.[1] Архивная копия от 18 июля 2008 на Wayback Machine
Примеры [Spoiler (click to open)]
…Гораздо более тонкий пример применения закона исключённого третьего, который хорошо демонстрирует, почему он не является приемлемым с точки зрения интуиционизма, состоит в следующем. Предположим, что мы хотим доказать теорему, что существуют иррациональные числа a и b такие, что a^b рационально.
Известно, что √2 иррациональное число (доказательство). Рассмотрим число:√2^√2.
Очевидно (исключая третий вариант), что это число либо рационально, либо иррационально. Если данное число рационально, то теорема доказана. Искомые числа: a=√2 b=√2
√2^√2 является иррациональным, тогда пусть a=√2^√2 и b=√2. Следовательно,
=a^b=(√2^(√2))^√2=√2^(√2∙√2)=(√2)^2=2,
то есть a^b - рациональное число.
По закону исключённого третьего иных вариантов быть не может. Поэтому теорема в общем случае доказана. Причём доказательство предельно просто и элементарно. С другой стороны, если принять интуиционистскую точку зрения и отказаться от закона исключённого третьего, теорема хотя и может быть доказана, но доказательство её становится исключительно сложным.
===
2-2) При этом отдельно есть "закон противоречия", который интуиционисты считают выполняющимся:
===
https://ru.wikipedia.org/wiki/Закон_противоречия
Закон противоречия [Spoiler (click to open)](закон непротиворечия) - закон логики, который гласит, что два несовместимых (противоречащих или противоположных) суждения не могут быть одновременно истинными - по крайней мере одно из них ложно[1].
Математическая запись в виде формулы, всегда имеющей ложное значение[2]:
P∧┐P, где: ∧ - знак конъюнкции (И); ┐ - знак отрицания.
Закон противоречия является фундаментальным логическим законом, на котором построена вся современная математика. Его отрицание является тавтологией классической логики, а также большинства неклассических логик, в том числе интуиционистской логики. Всё же существуют нетривиальные логические системы, в которых он не соблюдается, например, логика Клини.
===
Т.е.
A∧┐A = всегда ложь, в классической логике и для интуиционистов
A∨┐A - всегда истина, в классической логике, но не для интуиционистов, для них возможны другие варианты.
2-3) Различия классической и интуиционистской логики в законах двойного отрицания - для интуиционистов работает только закон введения двойного отрицания, а остальные не работают. [Spoiler (click to open)]А конструктивисты к тому, что они интуиционисты ещё добавляют конечность шагов алгоритма вывода, что проясняет смысл того, почему отрицание отрицания не получится снять: когда есть бесконечный перебор невозможно сделать его конечным. Это следует из преобразования отрицания с кванторами (в логике 1 порядка).
┐A(x)↔∃x,┐A(x) - отрицание какого-то А(х) - это существование хотя бы одного х, при котором А(х) будет ложным
┐∃x,B(x)↔∀x,┐B(x) - отрицание существования хотя бы одного х, при котором выполняется В(х) - это невыполнение В(х) для любого х.
В конструктивной логике не признаётся возможным бесконечный перебор - алгоритм вывода должен быть только конечным, а что будет в других случаях, как я понимаю - "неизвестно".
А в интуиционистской логике работает A→┐(┐A), а в обратную сторону - нет: ┐(┐A)→A, потому как полагается, что кроме А и не А может быть что-то ещё - не работает закон исключения третьего.
===
https://ru.wikipedia.org/wiki/Закон_двойного_отрицания
[Spoiler (click to open)]положенный в основу классической логики принцип, согласно которому «если неверно, что неверно А, то А верно». Есть 3 формулировки закона двойного отрицания. В формализованном языке логики высказываний они выражаются формулами:
A→┐(┐A) - закон введения двойного отрицания;
┐(┐A)→A - закон снятия двойного отрицания;
A↔┐(┐A) - полный закон двойного отрицания.
В интуиционистской логике выводится лишь закон введения двойного отрицания, закон снятия же не выводится.
[Spoiler (click to open)]В традиционной содержательной математике закон двойного отрицания служит логическим основанием для проведения так называемых доказательств от противного по следующей схеме: из предположения, что суждение А данной математической теории неверно, выводится противоречие в этой теории, затем на основании непротиворечивости теории делается вывод, что неверно «не А», и тогда по закону снятия двойного отрицания заключают, что верно А. В рамках конструктивных рассмотрений, когда действует требование алгоритмической реализуемости обоснования математических суждений, закон снятия двойного отрицания оказывается, вообще говоря, неприемлемым.
Типичным тому примером служит всякое доказательство от противного суждения А, имеющего вид «при всяком х существует у такой, что верно В(х, у)», когда последний шаг, состоящий в применении закона снятия двойного отрицания, оказывается невозможным из-за того, что конструктивное понимание суждения требует для его обоснования построения алгоритма, который по каждому х давал бы конструкцию у такого, что верно В(х, у). Между тем рассуждение с применением закона снятия двойного отрицания не приводит к построению какого бы то ни было алгоритма; более того, искомого в этом случае алгоритма может вообще не существовать (см. также принцип конструктивного подбора).
Другие формулировки [Spoiler (click to open)]
Закон снятия двойного отрицания тесно связан с законом исключённого третьего, а также с так называемым законом Пирса. В определённом смысле все три закона эквивалентны. Так, в интуиционистском исчислении высказываний, где эти законы не являются тавтологиями, каждый из этих двух законов выводим из другого, а добавление любого из них в аксиоматику сразу приводит к классической логике. При этом однако, существуют логики, в которых все три закона неэквивалентны[1].
Для интуиционистской логики есть более слабая форма для закона снятия - закон снятия тройного отрицания:
┐(┐(┐A))→(┐A).
===
2-4) Дальше стоит ознакомиться с различием подходов классической логики и интуиционистов+конструктивистов в отношении доказательства от противного (и сведения к абсурду):
===
https://ru.wikipedia.org/wiki/Доказательство_от_противного
[Spoiler (click to open)]вид доказательства, при котором «доказывание» некоторого суждения (тезиса доказательства) осуществляется через опровержение отрицания этого суждения - антитезиса[2]. Этот способ доказательства основывается на истинности закона двойного отрицания в классической логике.
Схема доказательства [Spoiler (click to open)]
…
Доказательство утверждения А проводится следующим образом. Сначала принимают предположение, что утверждение А неверно, а затем доказывают, что при таком предположении было бы верно некоторое утверждение В, которое заведомо неверно.
Из определения импликации следует, что, если В ложно, то формула ┐А→В истинна тогда и только тогда, когда ┐A ложно, следовательно утверждение А истинно.
Полученное противоречие показывает, что исходное предположение было неверным, и поэтому верно утверждение ┐┐A, которое по закону двойного отрицания равносильно утверждению А.
Это рассуждение можно заменить следующим рассуждением, состоящим из двух частей: первая часть представляет собой доказательство утверждения ┐┐A приведением к нелепости (reductio ad absurdum), а вторая - переход к утверждению А снятием двойного отрицания. Поскольку, хотя и неявно, используется классическое правило снятия двойного отрицания, метод доказательства от противного является классическим и служит источником неэффективных доказательств теорем существования. О сущности различий между этими правилами написано далее в данной статье.
В интуиционистской логике доказательство от противного не принимается, так же как не действует закон исключённого третьего[1].
[1] [Spoiler (click to open)]Косвенное доказательство//Философия: Энциклопедический словарь. - М.: Гардарики. Под редакцией А. А. Ивина. 2004.
Замечание. Данная схема похожа на другую - на схему доказательства приведением к нелепости. В связи с этим их часто путают. Однако несмотря на некоторое сходство, они имеют разную форму. Причём различаются они не только по форме, но и по существу, и различие это носит принципиальный характер.
Сопоставление методов доказательства от противного и приведением к нелепости [Spoiler (click to open)]
…[Я: схемы смотреть в Википедии,
в док-ве от противного из вывода противоречия из отрицания А двойным отрицанием выводится А,
а в доведении до нелепости/абсурда - из самого А выводится противоречие и нет двойного отрицания]…
К сожалению, обычно в практике преподавания, а также в печатных изданиях - учебных, методических и научных - авторы не различают эти две схемы, два способа доказательства, чаще всего называя и тот и другой доказательством от противного.
Остановимся на причинах того, почему всё же следует различать эти схемы.
Во-первых, очевидно, что эти схемы отличаются чисто графически, а значит, рассуждения по этим схемам различаются по форме. Различия такого же характера, т. е. по крайней мере по форме, имеются между предложениями А и ┐┐A (или между предложениями А→В и ┐А∨В). Даже если, находясь на классических позициях, мы считаем, что эти утверждения равносильны, то всё равно факт различия по форме является очевидным.
Однако такое различие может кому-то показаться недостаточным, неубедительным для того, чтобы затевать весь этот разговор. Естественно, возникают вопросы: не равносильны ли эти схемы; в чём выражается различие между ними в практике математических доказательств; это различие лишь по форме или также по существу?
…
Доказывая методом от противного, мы используем более сильные логические средства, чем когда доказываем приведением к нелепости. Это вызвано тем, что доказательство от противного существенно опирается на правило снятия двойного отрицания, а доказательство приведением к нелепости нет. Именно благодаря этому обстоятельству различие между схемами contradictio in contrarium и reductio ad absurdum - это различие не только по форме, но и по существу. Более того, это различие тесно связано с некоторыми проблемами оснований математики.
Дело в том, что такие логические законы, как закон исключённого третьего А∨┐A, закон снятия двойного отрицания ┐(┐A)→A, схема доказательства от противного ((┐A→В)∧(┐A→┐В))→А, приводят к неэффективным конструкциям и доказательствам в математике. В первую очередь это относится к доказательствам так называемых теорем существования, т. е. теорем вида: «Существует x такой, что Р(х)»: ∃х,Р(х), где Р(х) - некоторое свойство Р, которое выполняется для x, причём x пробегает некоторое множество известных объектов (чисел, формул, множеств формул, и т. п.).
Эффективным доказательством теоремы вида ∃х,Р(х) называется построение объекта x (или способа, позволяющего построить этот объект) и доказательство того, что этот объект действительно обладает требуемым свойством Р. Доказательство теоремы существования, не удовлетворяющее этим условиям, считают неэффективным.
Типичным неэффективным доказательством теоремы существования является доказательство методом от противного. Действительно, пусть требуется доказать утверждение вида ∃х,Р(х) - «существует объект x, обладающий свойством Р». Допустим, что ┐∃х,Р(х). Путём рассуждений получаем некоторое противоречие: В и ┐В. Отсюда, в силу схемы reductio ad absurdum, делаем вывод, что допущение неверно, т. е. ┐┐∃х,Р(х). Далее, снимая двойное отрицание, получим ∃х,Р(х) и считаем доказательство завершённым. Однако такое доказательство не завершается построением хотя бы одного объекта с требуемым свойством, оно нисколько не приближает нас к построению примера такого x, что Р(х), т. е. является неэффективным доказательством.
Примерами доказательств такого вида служат доказательства теорем: теоремы об ограниченности непрерывной на отрезке функции (т. е. о существовании верней и нижней границ непрерывной на отрезке функции); теоремы о существовании наибольшего и наименьшего значений у непрерывной на отрезке функции. Традиционное доказательство этих теорем методом от противного не содержит конструкции, позволяющей построить объект, о существовании которого идёт речь в теореме.
Неэффективные доказательства теорем существования признаются не всеми математиками. Для математиков, стоящих на традиционных классических позициях, характерным является признание без всяких ограничений закона исключённого третьего А∨┐A и закона снятия двойного отрицания ┐(┐A)→A. Они пренебрегают различиями между утверждениями ∃х,Р(х) и ┐┐∃х,Р(х). Математики, не придерживающиеся классических взглядов (интуиционисты и конструктивисты), отрицают универсальность этих законов. Различия между утверждениями ∃х,Р(х) и ┐┐∃х,Р(х) такие математики признают весьма существенными, считая утверждение ┐┐∃х,Р(х), вообще говоря, более слабым, чем ∃х,Р(х). Доказательство от противного, с их точки зрения, также является неприемлемым, поскольку оно опирается на принцип снятия двойного отрицания.
Таким образом, различие между схемами contradictio in contrarium и reductio ad absurdum носит методологический характер, затрагивая проблему разного понимания утверждений о существовании в математике, а также связанные с этим другие проблемы оснований математики.
Идея построения основных разделов математики на эффективной основе, без использования закона снятия двойного отрицания и закона исключенного третьего восходит к интуиционистской концепции Л. Э. Я. Брауэра. Интуиционистское направление в математике бурно развивалось на протяжении всего XX в. Существенное развитие неклассические идеи получили в работах представителей школы конструктивного направления в математике во главе с А. А. Марковым - выдающимся советским математиком (1903-1979).
===
2-5) Интуиционисты:
===
https://ru.wikipedia.org/wiki/Интуиционистская_логика
Интуициони́стская ло́гика - [Spoiler (click to open)]формальная система, отражающая некоторые способы рассуждений, приемлемые с точки зрения интуиционизма. Предложена А. Гейтингом в 1930.
Основное отличие от привычного исчисления высказываний заключается в том, что отсутствует закон исключённого третьего.
Схемы аксиом 1-10 и правило «модус поненс» задают интуиционистское исчисление высказываний. Все 12 схем аксиом и все 3 правила вывода задают интуиционистское исчисление предикатов. Интуиционистское исчисление предикатов отличается от классического тем, что в последнем вместо схемы аксиом 10 используется схема аксиом ┐(┐A)→A.[1]. [Spoiler (click to open)][1] В. Е. Плиско Интуиционистская логика. - Математический энциклопедический словарь. - М., Советская энциклопедия, 1988. - Тираж 150 000 экз. - c. 243
Логические символы
∧ (знак конъюнкции), ∨ (знак дизъюнкции), → (знак импликации) и ┐ (знак отрицания).
Схемы аксиом [Spoiler (click to open)]
Далее через A, B и C обозначаются произвольные пропозициональные формулы.
1) (A→(B→A))
2) ((A→B)→((B→C)→(A→C)))
3) (A→(B→(A∧B)))
4) ((A∧B)→A)
5) ((A∧B)→B)
6) (A→(A∨B))
7) (B→(A∨B))
8) ((A→C)→((B→C)→((A∨B)→C)))
9) ((A→B)→((A→(┐B))→(┐A)))
10) ((┐A)→(A→B))
11) ∀xA(x)→A(y)
12) A(y)→∃xA(x)
Правила вывода [Spoiler (click to open)]
1) Modus ponens:
A,(A→B)
B
2)
C→A(x)
C→∀xA(x)
если x не является свободной переменной в C.
3)
A(x)→C
∃xA(x)→C
если x не является свободной переменной в C.
===
https://ru.wikipedia.org/wiki/Интуиционизм
Интуициони́зм - [Spoiler (click to open)]совокупность философских и математических взглядов, рассматривающих математические суждения с позиций «интуитивной убедительности». Различаются две трактовки интуиционизма: интуитивная убедительность, которая не связана с вопросом существования объектов, и наглядная умственная убедительность.
В интуиционистской математике отвергается подход классической теории множеств (в частности, не принимаются аксиома выбора и аксиома регулярности) и ряд рассуждений классической логики. Абстракция потенциальной осуществимости, которая используется в интуиционистской математике, лучше соотносится с действительностью, чем абстракция актуальной бесконечности.
Исторический очерк
Критика теории множеств привела к возникновению трёх течений: интуиционизма Лёйтзена Эгберта Яна Брауэра, формализма Давида Гильберта и логицизма Готлоба Фреге, Бертрана Рассела, Альфреда Норта Уайтхеда. …
Интуиционистская логика
В интуиционистской математике суждение считается истинным, только если его можно доказать некоторым «мысленным экспериментом». То есть истинность утверждения «Существует объект x, для которого верно суждение A(x)» доказывается построением такого объекта, а истинность утверждения «A или B» доказывается либо доказательством истинности утверждения A, либо доказательством истинности утверждения B. Отсюда, в частности, следует, что утверждение «A или не A» может быть не истинным, а закон исключённого третьего неприемлем. Истинным математическим суждением является ряд выполненных построений эффективного характера с использованием интуиционистской логики. Эффективность не обязательно связана с наличием алгоритма и может зависеть от физических и исторических факторов, фактического решения проблем[1]. …
Интуиционизм и другие математические подходы
…Значительное влияние друг на друга оказали концепции формализма и интуиционизма.
…В широкой трактовке конструктивное направление математики можно рассматривать как часть интуиционистской математики[1].
===
2-6) Конструктивисты.
===
https://ru.wikipedia.org/wiki/Конструктивная_логика
[Spoiler (click to open)]одно из направлений современной математической логики, которая исходит из принципов конструктивной математики и результатов критической переработки рациональных положений интуиционистской логики.
Конструктивисты, так же как и интуиционисты не принимают понятие абстракции актуальной бесконечности, то есть бесконечности, завершённой, видя в ней слишком сильную идеализацию, и проводят свои исследования в рамках абстракции потенциальной осуществимости, признающей незавершённую, становящуюся бесконечность, которую, следовательно нельзя рассматривать как что-то готовое и законченное.
Бесконечное множество, говорят они, бесконечно лишь в том смысле, что его можно неограниченно продолжать конструировать. …
Исследование в конструктивной логике ограничивается исследованием конструктивных объектов, существование которых лишь тогда считается доказанным, когда указывается способ потенциально осуществимого построения (конструирования) этих объектов. Конструктивная логика считает неправильным перенос принципов, применяемых в области конечных множеств, на область бесконечных множеств.
В конструктивной логике в операциях с бесконечными множествами не применяется закон исключённого третьего. Конструктивисты это объясняют тем, что в операциях, включающих в себя бесконечные множества, которые находятся в процессе становления, невозможно определить, какова будет последующая альтернатива. Правда, также как и интуиционисты, они не отрицают применимость закона исключённого третьего по отношению к конечным областям.
Но принимая некоторые положения интуиционистской логики, конструктивная логика несводима к интуиционистской логике. …
===
Выше не включил в цитату советскую борьбу с "субъективистами" и "верой в реальность божества", как политически мотивированную муть. Меня тут не интересует взгляды сов.власти. Из ссылок к статье только 1 на статью из энциклопедии после 1991 года - лежащей на сайте ИФ РАН - там статья адекватнее:
===
https://iphlib.ru/library/collection/newphilenc/document/HASH0171caea6f531bf148fa0371
КОНСТРУКТИВНАЯ ЛОГИКА - [Spoiler (click to open)]совокупность логических принципов, признаваемых представителями конструктивизма (в математике) и включающих абстракцию потенциальной, но не актуальной бесконечности, что определенным образом изменяет понимание логических связок и кванторов (по сравнению с их пониманием в классической логике), сочетая это понимание с конструктивными процессами (процессами, описываемыми алгоритмами). Так, дизъюнкция высказываний «А или B» считается обоснованной, если потенциально осуществим конструктивный процесс, позволяющий выбрать верный член этой дизъюнкции; аналогично оценивается обоснованность многочленных дизъюнкций. Близко к пониманию дизъюнкции истолкование квантора существования: утверждение «существует такой х, для которого справедливо условие А» считается обоснованным, если потенциально осуществим конструктивный процесс подбора конструктивного объекта х, подтверждающего условие А. Обоснование конъюнкции «А и В» состоит в обосновании обоих (т.е. всех) конъюнктивных членов, а утверждение «Для всякого x справедливо условие А» считается обоснованным, если мы в состоянии для всякого объекта рассматриваемого вида доказать, что он удовлетворяет предъявленному требованию. Обоснование импликации «если А, то В» состоит в предъявлении конструктивного процесса, позволяющего по обоснованию утверждения А построить обоснование утверждения В. Отрицание утверждения А обосновывается предъявлением конструкции, приводящей к противоречию всякую попытку обоснования A.
Конструктивное истолкование логических связок и кванторов допускает и различные другие уточнения. В частности, созданы различные аксиоматические системы конструктивной логики. Поскольку конструктивная позиция идейно близка интуиционистской, аксиоматические системы, первоначально предназначавшиеся для реконструкции интуиционистски приемлемых рассуждений (см. Интуиционистская логика), называются (или подразумеваются) конструктивными. … Отличие этих логик от классической проявляется в том, что хотя конструктивно приемлемыми являются, напр., законы p→¬¬p, ¬¬¬p→¬p, (p→q)→(¬q→¬p), в этих системах отсутствуют практически все остальные варианты форм рассуждений «от противного» - закон снятия двойного отрицания ¬¬p→p, закон контрапозиции (¬р→¬q) →(q → p), закон Клавия (¬p→p) → p, закон Пирса ((p→q) → p) → p и др. Кроме того, в конструктивной логике связки независимы, т.е. не выражаются друг через друга, нет классической взаимовыразимости кванторов всеобщности и существования. В результате оказываются, в частности, необоснованными рассуждения, приводящие к доказательству т.н. чистых теорем существования, типичным примером которых является доказательство Г.Кантора существования трансцендентных (т.е. действительных, но не алгебраических) чисел…
===
3) на 4:00 - краткая схема доказательства 1й теоремы Гёделя о неполноте. [Spoiler (click to open)]
G - специальное утверждение в нашей формальной системе, такое что:
G ↔ "G не доказуемо". Это определение для G - т.е. G - это утверждение "G не доказуемо". оно "истинное" по определению.
Пусть недоказуемость G = ложности G, тогда:
G ↔ "G ложно". Это парадокс лжеца. А значит предположение, что недоказуемость G = ложности G - ложное. Т.е. так доказывается недоказуемость G, при условии его истинности. Осталось только подобрать такое G - что и сделал Гёдель, пронумеровав все утверждения в арифметике Пеано и сделав утверждение о номере утверждения.
А про утверждение G ↔ "G ложно" на 5:00 лектор говорит, что такое утверждение не может быть ни "истинным", ни "ложным". Но при этом ничего не меняет в картинке множества всех утверждений формальной системы - не добавляет 3ю область "не истинных и не ложных" утверждений.
И вот это то самое место, где у меня вопросы. Если разделили множество возможных утверждении только на 2 части: "истинные" и "ложные", и вдруг выяснили, что есть ещё и утверждения "не истинные и не ложные одновременно", то не означает ли это, что исходное разбиение множества только на "истинные" и на "ложные" утверждения само ложно, т.к. не включает утверждения без истинности и ложности? Как раз от каких-то таких рассуждений я интуитивно приходил к отрицанию "закона исключения третьего". Тем более, что в компьютерной логике на базах данных (SQL), есть это третье - Unknown/Empty/Error. Но до интиуционистской логики не доходил, т.к. не доходил до аксиоматического построения логики. Т.е. сейчас дошёл до того места, на котором останавливался раньше. И теперь знаю, как разбираться дальше - через аксиомы. И теперь знаю, что в этом уже разобрались - можно просто ознакомиться с готовыми результатами.