ядрёной математики вам в мозг
Казимиров на канале Савватеева про формальные системы и теоремы Гёделя - 4.5 часа одним видео:
https://www.youtube.com/watch?v=KhaYjR2sCEY
4:25:11
Вторая теорема Гёделя
Маткульт-привет! :: Алексей Савватеев и Ко, 7 тыщ просмотров, 19 сент. 2021 - 270 тыс. подписчиков
[Spoiler (click to open)]
Авторский курс Николая Казимирова
Конспект: https://disk.yandex.ru/i/NgHxc6ptlCVAUQ
Канал Николая: @reisedurchdiemathe https://www.youtube.com/channel/UCdmf8RSgKOOXYjOk9WlUUCg
0:00:00 - Предисловие
0:00:38 - Формальные системы: определение
0:35:18 - Аксиомы: логические и нелогические
0:54:02 - Нумералы
0:55:45 - Правила вывода и построение выводов
1:09:48 - Теорема о дедукции
1:12:10 - Независимость формул, непротиворечивость и полнота теории
1:19:53 - Модели формальных теорий, интерпретация термов и формул
1:39:00 - Истинные в модели формулы
1:44:35 - Теорема о корректности исчисления предикатов
1:55:10 - Теорема Гёделя о полноте
1:57:10 - Теорема Лёвенгейма-Сколема
2:07:40 - Выразимость предикатов и функций в сигнатуре
2:30:40 - Вычислимые функции
2:31:20 - Перечислимость и разрешимость множеств
2:35:47 - Теорема Клини о существовании перечислимого неразрешимого множества
2:38:35 - Иерархия формул
2:41:15 - Теорема о сигма1-определимости вычислимых функций в арифметике
2:49:42 - Теорема о дельта0-разрешимости арифметики
2:52:30 - Теорема о сигма1-полноте арифметики
3:07:48 - Первая теорема Гёделя о неполноте (синтаксический вариант)
3:24:12 - Гёделева нумерация формл в форме Куайна
3:38:40 - Теорема о неподвижной точке
3:53:30 - Аксиомы Гёделя-Лёба в модальной логике
3:58:25 - Теорема Лёба
4:10:42 - Вторая теорема Гёделя о неполноте
4:15:20 - Теорема Тарского о невыразимости истины
Наши ресурсы: https://vk.com/alexei_savvateev https://www.instagram.com/aleksey_savvateev https://www.facebook.com/savvatan https://savvateev.livejournal.com https://savvateev.xyz https://t.me/savvateev_xyz
1) На самом деле математика тут не особо ядрёная, [Spoiler (click to open)]хотя Савватеев говорит, что он в ней не разбирается, и доверил пояснять Казимирову. В изложении Казимирова она становится более-менее понятной, особенно после того, как до этого посмотришь его же и других авторов лекции и статьи хотя бы в Википедии по тому же самому и смежным темам. В частности по ординалам, трансфинитным числам Кантора, которыми расширяют натуральный ряд чисел и арифметику Пеано, с помощью чего доказывают теорему Гудстейна - нетривиальный пример того, что нельзя доказать или опровергнуть в формальной системе арифметики с аксиомами Пеано/Тарского. Тут "особо сложного" ничего нет - всё на логику, а неизвестные тебе названия и фамилии становятся известными и более не пугают.
2) Но я ролик так до конца не отсмотрел. Остановился на том, что мне показалось важным, чтоб написать пост. Это вопрос о том, что в современной математике считают "истиной" и во что это всё упирается. [Spoiler (click to open)]
1:40:00 - Если на "сигнатуре" Σ (формальная система - начало лекции определяет, что это такое) утверждение (назвал формулой?) ВЫВОДИМО --> то на "модели" М утверждение (назвал формулой?) ИСТИННО (и тут уже действует закон исключения третьего)
Σ |- A |-> M |= Aм
Если такая "формула" в "модели" истинна при любых значениях переменных - то она сама "истинна".
Если ни в одном - то "ложная"
Формула в сигнатуре "выполнимая" - есть хотя бы одна модель, в которой она "выполнимая".
Формула "ложная" - если её отрицание выполнимо хоть в какой-то модели.
1:42:00 - на некой сигнатуре Σ есть теория Т, для которой есть отношение "выводимость" (значок "штопор": |-).
Этому отношению соответствует отношение "истинность" в модели М, удачно привязанной нами к этой сигнатуре. (Обозначается значком "двойной штопор": |=).
1:49:00 - если есть модель М - привязанная к теории Т - значит теория уже непротиворечивая, т.к. у модели уже есть носитель - и вся её "истинность" сводится к "истинности" метатеории для ИП (исчисления предикатов), что равно "непротиворечивости" ZFC, которая (как я понял) принимается на веру (постулируется). Потому что доказать это можно, лишь в другой системе - с добавлением новых аксиом, а ту - в системе с добавлением ещё аксиом, и так далее - что бессмысленно (тут: будет вместо одной принятой на веру системы, другая так же принятая на веру).
Добавлять аксиомы можно и имеет смысл (тут: не к ZFC для доказательства ZFC из новой системы, а "вообще" - к любой системе для произвольных целей) только те, которые не выводятся и не опровергаются остальными аксиомами формальной системы - т.е. теми самыми утверждениями, наличие которых доказывает неполноту формальной системы. Так "абсолютную геометрию" ([Spoiler (click to open)]аксиомы их 4х первых постулата Евклида: постулаты - что, что принимают на веру, аксиомы - это просто условие для построения формальной системы) дополняет аксиома о параллельности, которую можно выбрать любую - из 5 постулата Евклида, от Лобачевского, и или как в римановой геометрии - принять её переменной и в таком пространстве считать всё через тензоры.
3) Дальше не смотрел, но по оглавлению видно, что там что-то про "невыразимость истины". [Spoiler (click to open)]Возможно, это примерно то, что о чём менее строго и про другое (про эмпирические науки) писал Поппер, откуда вывел свой тезис, что (эмпирические = про реальность) теории только тогда "научные", когда допускают их "фальсификацию" (опровержение эмпирикой), потому как истинность эмпирикой не доказывается из-за сущности научного метода - что это НЕТОЧНАЯ ВЕРОЯТНОСТНАЯ неполная индукция = ВЕРОЯТНОСТНОМУ предсказанию на НЕПОЛНОЙ статистике НЕТОЧНЫХ эмпирических данных. А тут, в этом курсе у Казимирова, видимо, показывается, что "истины" нет и в строгой математике, где "истинность" сводится к предполагаемой истинности наиболее общей теории множеств ZFC, без которой большая часть математики не будет работать. Математика в научном методе не проверяется эмпирикой, а берётся как уже доказанное в самой математике общезначимое знание и используется для счёта статистики эмпирических измерений и в теормоделях, которые как раз и проверяются эмпирикой. И эта 4,5ч лекция именно о том, как же на самом деле обстоит дело с обоснованностью математики.
3-1) Глянул вперёд - оказалось, что "невыразимость" истины означает "неарифметизируемость" её, невыразимость через арифметику Пеано.
3-2) Предыдущий пост:[Spoiler (click to open)]
===
https://man-with-dogs.livejournal.com/3299704.html
2023-06-29 03:29 - бомблю от философа
…
+) А вообще, я пытаюсь подробнее разобраться с теоремами Гильберта …
===
3-3) В нём ставил вопрос: "что такое "любые системы, которые её (арифметику Пеано) содержат" - это самое интересное." [Spoiler (click to open)]
Пока мой интуитивный ответ из того, что послушал у Казимирова - это всё про формальные системы с мерой и одной бесконечностью по этой мере. Геометрия (например, Евклидова) содержит бесконечности, но не содержит меры - потому там возможна полнота и непротиворечивость одновременно. А в арифметике Пеано есть 0, 1 и есть бесконечное продолжение натурального ряда без включения самой бесконечности (включается в расширение арифметики как ординалы - трансфинитные числа Кантора). Для множества целых чисел уже есть какие-то отличия (не запомнил в чём именно - что-то со сложностью определения отношения ">=" + возможность перевернуть и сдвинуть ряд чисел в любую сторону в попаданием его на самого себя)
4) Диалог Казимирова с Григорьевым, [Spoiler (click to open)]комми-ММТшником (это там, где "правительство напечатает денег"), сделавшем пару лекций про теорему Гёделя для самых маленьких - с чего можно начинать знакомиться с темой: [Spoiler (click to open)]
https://www.youtube.com/watch?v=45SqP02qKDk
40:23
Теорема Гёделя, часть 1. Нежное введение и основные понятия.
New Deal - Экономика и Дефициты, 9 тыщ просмотров, 25 сент. 2020 - 18,3 тыс. подписчиков
[Spoiler (click to open)]
# логика # математика
Ого, математика! Этот день мы... в общем, ждали очень сильно. Чтобы не бросаться в мрачные уголки разума на одних эмоциях, начнём с теоретического минимума новобранца. Что такое множества, числа, теоремы, парадоксы и виды бесконечности? Наливайте кефир и открывайте блокноты, приключение начинается!
Аксиомы ZFC: https://tinyurl.com/y2vezg3k
Аксиомы Пеано: https://tinyurl.com/y34uhjwv
Таймкоды
00:00 Мы вместе больше года!
1:04 Почему Гёдель?
5:17 Зачем нужны теоремы и как работают доказательства
7:14 Множества, элементы и операции
10:41 Парадоксы теории множеств
14:46 В чём польза аксиоматического подхода?
16:17 Определение натуральных чисел
22:23 Простые числа и кодирование
26:05 Как посчитать бесконечность?
38:37 Мы многое поняли!
https://www.youtube.com/watch?v=69osRNhHiu8
1:11:17
Теорема Гёделя. Почти строгое доказательство!
New Deal - Экономика и Дефициты, 5 тыщ просмотров, 7 окт. 2021 - 18,3 тыс. подписчиков
[Spoiler (click to open)]
Как же хочется поскорее разобрать основную идею доказательства... Но сначала нам предстоит понять что общего между высказываниями, числами и формальными системами, а также зачем одно переводить в другое! (пожалуйста, не спрашивайте когда будет следующая часть)
Книга Ньюмена и Нагеля: https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371
Книга Мендельсона: https://www.routledge.com/Introduction-to-Mathematical-Logic/Mendelson/p/book/9781482237726
ссылка про формальные системы: https://cs.lmu.edu/~ray/notes/formalsystems/
Таймкоды:
00:00 Мы начинаем!
2:28 Предисловие (изоморфизм и структуры)
7:13 Языки и формальные системы
11:13 Кодирование и типы высказываний
15:16 Противоречия, полнота и выводимость
19:21 Арифметика и теория множеств
26:47 Формальные системы с арифметикой
31:58 Логические пояснения
33:48 Высказывания и числа
43:25 Метаматематика и доказательства
53:58 План доказательства
57:01 Поясняем шаги!
1:09:13 Финальные выводы
Ко второму видео в комменты пришёл Казимиров и сделал свои замечания и пояснения. Что, мол, хорошее доходчивое объяснение, но есть косячки + пояснил некоторые моменты, как раз те, на которых я и остановился при просмотре лекции Казимирова для записи их в этот пост: [Spoiler (click to open)]
===
https://www.youtube.com/watch?v=69osRNhHiu8&lc=UgyoCvY2WPG1nLlQxWt4AaABAg
@reisedurchdiemathe, 1 год назад (это Казимиров)
Отличная подача материала! Но есть одно небольшое замечание: в 14:51 сказано, что теорема - это выводимая в рамках формальной системы истинная формула. Это не так. Во-первых, формальная система сама по себе ничего не умеет выводить. Для этого ей как минимум нужно исчисление предикатов и правило modus ponens. Во-вторых, если система аксиом противоречива, то в ней теоремой будет любая формула, в том числе тождественно ложная, поскольку из противоречия выводимо все что угодно.
На самом деле, понятие истинности жестко привязано к модели. Одна и та же формула может быть как истинной, так и ложной в зависимости от ее интерпретации в модели (например, пятый постула Евклида на плоскости и в модели Клейна).
Так что теорема - это просто формула, выводимая из заданного аксиоматического базиса. В связке с моделью верно следующее: если формула выводима, то она истинна в модели, интерпретирующей данную аксиоматику (теорема о корректности ИП).
- Подробнее можно посмотреть ролик на канале Савватеева в моем исполнении: https://www.youtube.com/watch?v=KhaYjR2sCEY
6 лайков, 5 ответов
@NewDeal1917, 1 год назад (это Григорьев)
большое спасибо за ваши комментарии!
я ни в коем случае не являюсь специалистом или даже продвинутым любителем в матлогике, так что не могу страховаться от некорректных утверждений.
надеюсь в следующем году сделать небольшой плейлист по теории доказательств с прицелом на то, чтобы рассказать как можно удобно доказывать всякие штуки на языке Lean, облегчая себе процесс освоения базовых понятий.
было бы очень круто по возможности с вами консультироваться и что-то уточнять.
@reisedurchdiemathe, 1 год назад
@NewDeal1917 можно пообщаться, почему бы и да. сайт и мыло я указывал в свойствах своего канала. но я тоже не оракул и на все вопросы ответить не смогу) оракулом в матлогике я бы назвал академика Беклемишева)
@user-zh8dd6co2y, 1 год назад (юзер Ярослав Московский)
Пожалуйста поправьте меня, если не вполне строго выражаюсь, но ведь исчисление предикатов это тоже формальная система? Немного занимался когда-то программированием на Прологе, что-то еще, оказывается, помню. Всплыло, когда просматривал видео.
@reisedurchdiemathe, 1 год назад
@user-zh8dd6co2y исчисление предикатов - это формальная система + аксиомы исчисления предикатов) просто формальная система - это по сути язык, т.е. набор базовых значков и правил построения выражений. без аксиом она не имеет истинностно-ложного смысла.
регулярные выражения - тоже формальная система.
а вот разговорный язык - нет, т.к. в нем нет детерминированных правил построения выражений (т.е. по произвольному набору букв машина не всегда может распознать, является ли этот набор правильно построенным словом языка)
===
https://www.youtube.com/watch?v=69osRNhHiu8&lc=Ugxw5BPbn6A6ZmJeVzh4AaABAg
@reisedurchdiemathe, 1 год назад
Да, и, кстати, 27:00 - в элементарной геометрии невозможно интерпретировать арифметику Пеано, т.к. единица и ноль не определимы в э.г. (иначе бы они сохранялись при автоморфизмах). Да и полнота геометрии на это также указывает.
2 лайков, 3 ответа
@NewDeal1917, 1 год назад
но ведь с аксиоматикой Гильберта это уже работает?
@reisedurchdiemathe, 1 год назад
@NewDeal1917 с Гильбертом все не очень здорово, т.к. он включил в свою систему аксиому из логики второго порядка (аксиома о полноте). Поэтому лучше брать аксиоматику Тарского.
Но и без этого понятно, что раз геометрия полна, т арифметику в ней невозможно интерпретировать, иначе получим противоречие с первой т.Гёделя о неполноте. То же самое относится к теории вещественно замкнутых полей характеристики 0 (по сути матанализ, только без подмножеств - окрестностей и прочего).
Вообще логика второго порядка - читай наличие переменных, пробегающих подмножества (или предикаты логики первого порядка), а это гораздо более сильные теории.
Немного истории на эту тему я рассказывал в первом ролике про теорему Гудстейна на канале Савватеева.
===
https://www.youtube.com/watch?v=KhaYjR2sCEY
4:25:11
Вторая теорема Гёделя
Маткульт-привет! :: Алексей Савватеев и Ко, 7 тыщ просмотров, 19 сент. 2021 - 270 тыс. подписчиков
[Spoiler (click to open)]
Авторский курс Николая Казимирова
Конспект: https://disk.yandex.ru/i/NgHxc6ptlCVAUQ
Канал Николая: @reisedurchdiemathe https://www.youtube.com/channel/UCdmf8RSgKOOXYjOk9WlUUCg
0:00:00 - Предисловие
0:00:38 - Формальные системы: определение
0:35:18 - Аксиомы: логические и нелогические
0:54:02 - Нумералы
0:55:45 - Правила вывода и построение выводов
1:09:48 - Теорема о дедукции
1:12:10 - Независимость формул, непротиворечивость и полнота теории
1:19:53 - Модели формальных теорий, интерпретация термов и формул
1:39:00 - Истинные в модели формулы
1:44:35 - Теорема о корректности исчисления предикатов
1:55:10 - Теорема Гёделя о полноте
1:57:10 - Теорема Лёвенгейма-Сколема
2:07:40 - Выразимость предикатов и функций в сигнатуре
2:30:40 - Вычислимые функции
2:31:20 - Перечислимость и разрешимость множеств
2:35:47 - Теорема Клини о существовании перечислимого неразрешимого множества
2:38:35 - Иерархия формул
2:41:15 - Теорема о сигма1-определимости вычислимых функций в арифметике
2:49:42 - Теорема о дельта0-разрешимости арифметики
2:52:30 - Теорема о сигма1-полноте арифметики
3:07:48 - Первая теорема Гёделя о неполноте (синтаксический вариант)
3:24:12 - Гёделева нумерация формл в форме Куайна
3:38:40 - Теорема о неподвижной точке
3:53:30 - Аксиомы Гёделя-Лёба в модальной логике
3:58:25 - Теорема Лёба
4:10:42 - Вторая теорема Гёделя о неполноте
4:15:20 - Теорема Тарского о невыразимости истины
Наши ресурсы: https://vk.com/alexei_savvateev https://www.instagram.com/aleksey_savvateev https://www.facebook.com/savvatan https://savvateev.livejournal.com https://savvateev.xyz https://t.me/savvateev_xyz
1) На самом деле математика тут не особо ядрёная, [Spoiler (click to open)]хотя Савватеев говорит, что он в ней не разбирается, и доверил пояснять Казимирову. В изложении Казимирова она становится более-менее понятной, особенно после того, как до этого посмотришь его же и других авторов лекции и статьи хотя бы в Википедии по тому же самому и смежным темам. В частности по ординалам, трансфинитным числам Кантора, которыми расширяют натуральный ряд чисел и арифметику Пеано, с помощью чего доказывают теорему Гудстейна - нетривиальный пример того, что нельзя доказать или опровергнуть в формальной системе арифметики с аксиомами Пеано/Тарского. Тут "особо сложного" ничего нет - всё на логику, а неизвестные тебе названия и фамилии становятся известными и более не пугают.
2) Но я ролик так до конца не отсмотрел. Остановился на том, что мне показалось важным, чтоб написать пост. Это вопрос о том, что в современной математике считают "истиной" и во что это всё упирается. [Spoiler (click to open)]
1:40:00 - Если на "сигнатуре" Σ (формальная система - начало лекции определяет, что это такое) утверждение (назвал формулой?) ВЫВОДИМО --> то на "модели" М утверждение (назвал формулой?) ИСТИННО (и тут уже действует закон исключения третьего)
Σ |- A |-> M |= Aм
Если такая "формула" в "модели" истинна при любых значениях переменных - то она сама "истинна".
Если ни в одном - то "ложная"
Формула в сигнатуре "выполнимая" - есть хотя бы одна модель, в которой она "выполнимая".
Формула "ложная" - если её отрицание выполнимо хоть в какой-то модели.
1:42:00 - на некой сигнатуре Σ есть теория Т, для которой есть отношение "выводимость" (значок "штопор": |-).
Этому отношению соответствует отношение "истинность" в модели М, удачно привязанной нами к этой сигнатуре. (Обозначается значком "двойной штопор": |=).
1:49:00 - если есть модель М - привязанная к теории Т - значит теория уже непротиворечивая, т.к. у модели уже есть носитель - и вся её "истинность" сводится к "истинности" метатеории для ИП (исчисления предикатов), что равно "непротиворечивости" ZFC, которая (как я понял) принимается на веру (постулируется). Потому что доказать это можно, лишь в другой системе - с добавлением новых аксиом, а ту - в системе с добавлением ещё аксиом, и так далее - что бессмысленно (тут: будет вместо одной принятой на веру системы, другая так же принятая на веру).
Добавлять аксиомы можно и имеет смысл (тут: не к ZFC для доказательства ZFC из новой системы, а "вообще" - к любой системе для произвольных целей) только те, которые не выводятся и не опровергаются остальными аксиомами формальной системы - т.е. теми самыми утверждениями, наличие которых доказывает неполноту формальной системы. Так "абсолютную геометрию" ([Spoiler (click to open)]аксиомы их 4х первых постулата Евклида: постулаты - что, что принимают на веру, аксиомы - это просто условие для построения формальной системы) дополняет аксиома о параллельности, которую можно выбрать любую - из 5 постулата Евклида, от Лобачевского, и или как в римановой геометрии - принять её переменной и в таком пространстве считать всё через тензоры.
3) Дальше не смотрел, но по оглавлению видно, что там что-то про "невыразимость истины". [Spoiler (click to open)]Возможно, это примерно то, что о чём менее строго и про другое (про эмпирические науки) писал Поппер, откуда вывел свой тезис, что (эмпирические = про реальность) теории только тогда "научные", когда допускают их "фальсификацию" (опровержение эмпирикой), потому как истинность эмпирикой не доказывается из-за сущности научного метода - что это НЕТОЧНАЯ ВЕРОЯТНОСТНАЯ неполная индукция = ВЕРОЯТНОСТНОМУ предсказанию на НЕПОЛНОЙ статистике НЕТОЧНЫХ эмпирических данных. А тут, в этом курсе у Казимирова, видимо, показывается, что "истины" нет и в строгой математике, где "истинность" сводится к предполагаемой истинности наиболее общей теории множеств ZFC, без которой большая часть математики не будет работать. Математика в научном методе не проверяется эмпирикой, а берётся как уже доказанное в самой математике общезначимое знание и используется для счёта статистики эмпирических измерений и в теормоделях, которые как раз и проверяются эмпирикой. И эта 4,5ч лекция именно о том, как же на самом деле обстоит дело с обоснованностью математики.
3-1) Глянул вперёд - оказалось, что "невыразимость" истины означает "неарифметизируемость" её, невыразимость через арифметику Пеано.
3-2) Предыдущий пост:[Spoiler (click to open)]
===
https://man-with-dogs.livejournal.com/3299704.html
2023-06-29 03:29 - бомблю от философа
…
+) А вообще, я пытаюсь подробнее разобраться с теоремами Гильберта …
===
3-3) В нём ставил вопрос: "что такое "любые системы, которые её (арифметику Пеано) содержат" - это самое интересное." [Spoiler (click to open)]
Пока мой интуитивный ответ из того, что послушал у Казимирова - это всё про формальные системы с мерой и одной бесконечностью по этой мере. Геометрия (например, Евклидова) содержит бесконечности, но не содержит меры - потому там возможна полнота и непротиворечивость одновременно. А в арифметике Пеано есть 0, 1 и есть бесконечное продолжение натурального ряда без включения самой бесконечности (включается в расширение арифметики как ординалы - трансфинитные числа Кантора). Для множества целых чисел уже есть какие-то отличия (не запомнил в чём именно - что-то со сложностью определения отношения ">=" + возможность перевернуть и сдвинуть ряд чисел в любую сторону в попаданием его на самого себя)
4) Диалог Казимирова с Григорьевым, [Spoiler (click to open)]комми-ММТшником (это там, где "правительство напечатает денег"), сделавшем пару лекций про теорему Гёделя для самых маленьких - с чего можно начинать знакомиться с темой: [Spoiler (click to open)]
https://www.youtube.com/watch?v=45SqP02qKDk
40:23
Теорема Гёделя, часть 1. Нежное введение и основные понятия.
New Deal - Экономика и Дефициты, 9 тыщ просмотров, 25 сент. 2020 - 18,3 тыс. подписчиков
[Spoiler (click to open)]
# логика # математика
Ого, математика! Этот день мы... в общем, ждали очень сильно. Чтобы не бросаться в мрачные уголки разума на одних эмоциях, начнём с теоретического минимума новобранца. Что такое множества, числа, теоремы, парадоксы и виды бесконечности? Наливайте кефир и открывайте блокноты, приключение начинается!
Аксиомы ZFC: https://tinyurl.com/y2vezg3k
Аксиомы Пеано: https://tinyurl.com/y34uhjwv
Таймкоды
00:00 Мы вместе больше года!
1:04 Почему Гёдель?
5:17 Зачем нужны теоремы и как работают доказательства
7:14 Множества, элементы и операции
10:41 Парадоксы теории множеств
14:46 В чём польза аксиоматического подхода?
16:17 Определение натуральных чисел
22:23 Простые числа и кодирование
26:05 Как посчитать бесконечность?
38:37 Мы многое поняли!
https://www.youtube.com/watch?v=69osRNhHiu8
1:11:17
Теорема Гёделя. Почти строгое доказательство!
New Deal - Экономика и Дефициты, 5 тыщ просмотров, 7 окт. 2021 - 18,3 тыс. подписчиков
[Spoiler (click to open)]
Как же хочется поскорее разобрать основную идею доказательства... Но сначала нам предстоит понять что общего между высказываниями, числами и формальными системами, а также зачем одно переводить в другое! (пожалуйста, не спрашивайте когда будет следующая часть)
Книга Ньюмена и Нагеля: https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371
Книга Мендельсона: https://www.routledge.com/Introduction-to-Mathematical-Logic/Mendelson/p/book/9781482237726
ссылка про формальные системы: https://cs.lmu.edu/~ray/notes/formalsystems/
Таймкоды:
00:00 Мы начинаем!
2:28 Предисловие (изоморфизм и структуры)
7:13 Языки и формальные системы
11:13 Кодирование и типы высказываний
15:16 Противоречия, полнота и выводимость
19:21 Арифметика и теория множеств
26:47 Формальные системы с арифметикой
31:58 Логические пояснения
33:48 Высказывания и числа
43:25 Метаматематика и доказательства
53:58 План доказательства
57:01 Поясняем шаги!
1:09:13 Финальные выводы
Ко второму видео в комменты пришёл Казимиров и сделал свои замечания и пояснения. Что, мол, хорошее доходчивое объяснение, но есть косячки + пояснил некоторые моменты, как раз те, на которых я и остановился при просмотре лекции Казимирова для записи их в этот пост: [Spoiler (click to open)]
===
https://www.youtube.com/watch?v=69osRNhHiu8&lc=UgyoCvY2WPG1nLlQxWt4AaABAg
@reisedurchdiemathe, 1 год назад (это Казимиров)
Отличная подача материала! Но есть одно небольшое замечание: в 14:51 сказано, что теорема - это выводимая в рамках формальной системы истинная формула. Это не так. Во-первых, формальная система сама по себе ничего не умеет выводить. Для этого ей как минимум нужно исчисление предикатов и правило modus ponens. Во-вторых, если система аксиом противоречива, то в ней теоремой будет любая формула, в том числе тождественно ложная, поскольку из противоречия выводимо все что угодно.
На самом деле, понятие истинности жестко привязано к модели. Одна и та же формула может быть как истинной, так и ложной в зависимости от ее интерпретации в модели (например, пятый постула Евклида на плоскости и в модели Клейна).
Так что теорема - это просто формула, выводимая из заданного аксиоматического базиса. В связке с моделью верно следующее: если формула выводима, то она истинна в модели, интерпретирующей данную аксиоматику (теорема о корректности ИП).
- Подробнее можно посмотреть ролик на канале Савватеева в моем исполнении: https://www.youtube.com/watch?v=KhaYjR2sCEY
6 лайков, 5 ответов
@NewDeal1917, 1 год назад (это Григорьев)
большое спасибо за ваши комментарии!
я ни в коем случае не являюсь специалистом или даже продвинутым любителем в матлогике, так что не могу страховаться от некорректных утверждений.
надеюсь в следующем году сделать небольшой плейлист по теории доказательств с прицелом на то, чтобы рассказать как можно удобно доказывать всякие штуки на языке Lean, облегчая себе процесс освоения базовых понятий.
было бы очень круто по возможности с вами консультироваться и что-то уточнять.
@reisedurchdiemathe, 1 год назад
@NewDeal1917 можно пообщаться, почему бы и да. сайт и мыло я указывал в свойствах своего канала. но я тоже не оракул и на все вопросы ответить не смогу) оракулом в матлогике я бы назвал академика Беклемишева)
@user-zh8dd6co2y, 1 год назад (юзер Ярослав Московский)
Пожалуйста поправьте меня, если не вполне строго выражаюсь, но ведь исчисление предикатов это тоже формальная система? Немного занимался когда-то программированием на Прологе, что-то еще, оказывается, помню. Всплыло, когда просматривал видео.
@reisedurchdiemathe, 1 год назад
@user-zh8dd6co2y исчисление предикатов - это формальная система + аксиомы исчисления предикатов) просто формальная система - это по сути язык, т.е. набор базовых значков и правил построения выражений. без аксиом она не имеет истинностно-ложного смысла.
регулярные выражения - тоже формальная система.
а вот разговорный язык - нет, т.к. в нем нет детерминированных правил построения выражений (т.е. по произвольному набору букв машина не всегда может распознать, является ли этот набор правильно построенным словом языка)
===
https://www.youtube.com/watch?v=69osRNhHiu8&lc=Ugxw5BPbn6A6ZmJeVzh4AaABAg
@reisedurchdiemathe, 1 год назад
Да, и, кстати, 27:00 - в элементарной геометрии невозможно интерпретировать арифметику Пеано, т.к. единица и ноль не определимы в э.г. (иначе бы они сохранялись при автоморфизмах). Да и полнота геометрии на это также указывает.
2 лайков, 3 ответа
@NewDeal1917, 1 год назад
но ведь с аксиоматикой Гильберта это уже работает?
@reisedurchdiemathe, 1 год назад
@NewDeal1917 с Гильбертом все не очень здорово, т.к. он включил в свою систему аксиому из логики второго порядка (аксиома о полноте). Поэтому лучше брать аксиоматику Тарского.
Но и без этого понятно, что раз геометрия полна, т арифметику в ней невозможно интерпретировать, иначе получим противоречие с первой т.Гёделя о неполноте. То же самое относится к теории вещественно замкнутых полей характеристики 0 (по сути матанализ, только без подмножеств - окрестностей и прочего).
Вообще логика второго порядка - читай наличие переменных, пробегающих подмножества (или предикаты логики первого порядка), а это гораздо более сильные теории.
Немного истории на эту тему я рассказывал в первом ролике про теорему Гудстейна на канале Савватеева.
===