51 завершение курса по матлогике
Vložit
- čas přidán 4. 07. 2024
- Обзор тем, затронутых в курсе:
- Логика = Язык + Исчисление + Семантика
- Оценка, семантическая корректность и полнота вывода
- Классы семантик (алгебры Гейтинга, топология, шкалы Крипке)
- Теории: корректность, синтаксическая полнота, тееоремы Гёделя
- Стандартные модели логик и арифметик
- Иерархии формул
- Перечислимость и разрешимость множеств
- Теория рекурсивных функций (теория вычислимости)
- Иерархии функций
- Определимость, представимость в теории
- Доказуемо тотальные рекурсивные функции
- Ординальные анализ, прогрессии Тьюринга (теория доказательств)
Если пропустили начало: вот ссылка на плейлист: • Основные понятия и тео...
💰 Если Вам нравится мой контент, то Вы можете поддержать канал:
через сервис Boosty: boosty.to/mathreisender
Черновой конспект лекций: disk.yandex.ru/i/2zw7wrW1q-Umvg (часть конспекта написана на английском языке) - Věda a technologie
👍
Прекрасный курс. Больше спасибо. Признаться, еще не весь его осилил, но пока все очень нравится, особенно стиль и доступность изложения. Хотел бы попросить вас прокомментировать нынешнее состояние теории доказательств и ординального анализа. Как мне известно последние работы в этом направлении были сделаны T. Arai в 2021 - 2024. В первой работе "An ordinal analysis of Π_1-Collection", как я понимаю, автор методами ординального анализа создает proof-theoretic ordinal (PTO) для ZFC без аксиомы булеана, со схемами, ограниченными для Π1-формул, а во второй работе "An ordinal analysis of Π_N-Collection" достигнут PTO для ZFC без аксиомы булеана, со схемами для любых формул, что эквивалентно Арифметике второго порядка. И если его работа не содержит каких-либо критических ошибок, то значит ли это, что мы достигли того уровня, когда была доказана непротиворечивость арифметики второго порядка? И если это так, то получается, что это крупнейшее достижение с момента доказательства непротиворечивости Арифметики Пеано (1ого порядка)? Как вы прогнозируете будущее развитие теории доказательств, доживем ли мы до того момента, когда будет доказана непротиворечивость всей ZFC, или, возьмем круче, даже ZF+AD? В каких тогда метатеориях придется работать логикам для этого? Ну и насколько это будет отдалено от людей, которые не посвятили всю свою жизнь мат.логике? Есть ли сейчас шанс у начинающего логика понять суть последней работы T. Arai?
Спасибо за высокую оценку моего труда. Указанную работу я еще не читал, но уже по вашему комментарию понятно, что это некотрые частные случаи подхода. Строго говоря, доказать непротиворечивость арифметики второго опрядка силами ее самой или более слабой теории нельзя - теорему Гёделя никто не отменял. А в ZFC доказать непротиворечивость арифметики любого порядка - задача почти тривиальная.
Поэтому современные поиски идут отчасти в поле слабых негеделевых систем.
То, что вы упоминаете, скорее, является поиском таких негеделевых систем, которые а) умеют доказывать свою непротиворечивость и б) являются достаточно выразительными для описания более сильных формализмов. В этом же направлении работает Федор Пахомов, он тоже имеет некотрые результаты о формальной теории множеств без аксиомы степени. Можете погуглить.
В классическом же смысле, разумеется, мы никогда не докажем непротиворечивость PA хоть 1го, хоть 2го порядка.
Вопрос в том, как в будущем изменится подход к определению непротиворчивости или, скажем, так, надежности формальных систем. Например, будем ли мы считать теорию достаточно надежной, если ее язык определен в более слабой системе, умеющей доказывать свою непротиворечивость? Или будет придумана еще какая-то категория теорий, способных давать классические результаты математики (или их аналоги в некотором приближении), но при этом не являющихся геделевыми? Пока здесь все покрыто мраком неизвестности.
Насчет способности понять - тут как посмотреть. Алгебраисты, думаю, способны понять, т.к. это рядом с ними происходит. Нематематики - вряд ли, потому что нужен хороший бэкграунд в смысле упражнений с формальным выводом.
Одно неизбежно: борьба формального с неформальным будет вечной)) Такова природа человека.
@@reisedurchdiemathe Я имел ввиду, что это большое достижение в области конструктивных доказательств. В одной из ваших лекций вы упоминали, что в свое время к теореме о неполноте Геделя с ее диагональным доказательством по языку самой арифметики отнеслись скептически, посчитав этот пример искусственным, не имеющим отношения к каким-либо реальным теоремам, но появление теоремы Гудстейна все изменило, и именно это дало толчок к развитию Генценовского подхода и трансфинитных итераций по Тьюрингу, о которых вы говорили в последних лекциях, и формирования самого понятия теоретико-доказательственный ординал. Наличие примера конструктивной теоремы, которая выходит за пределы доказательственных возможностей теории, ее демонстративное доказательство в рамках более сильной теории, и иллюстрация того самого ε_0 - PTO(PA) это то, что окончательно сменило парадигму в умах большинства математиков. В сущности, как я понимаю, такие иерархии, как FGH или иерархии Харди в совокупности с трансфинитными ординалами сами по себе генерируют подобные теоремы для соответствующих по силе теорий. Но тут есть важный момент - объяснить неподготовленному человеку масштаб рекурсий (размеры чисел) FGH от ε_0 или тех, что создаются в процессе вычисления теоремы Гудстейна - это посильная задача даже в рамках нестрогих научно-популярных математических роликов, нужно всего лишь познакомить с нормальной формой Кантора и понятием фундаментальной последовательности. Но вот рекурсии (размеры чисел), которые создаются вблизи FGH от PTO(Z2), который был получен Arai, настолько мощные и невообразимые, что даже сами математики врятли могут их до конца постичь. Мне кажется только правила записи нормальной формы его коллапсирующей функции должны занимать более 50 стр. И если объяснить скажем функцию Веблена, которая добивает до ATR0, или коллапсирующую функцию Бухольца добивающую до KPω еще можно в рамках лекций и курсов, то дальше начинается непроглядный рекурсивный лес. Предыдущими рекордсменами в этой области были в 80-е Buchholz и Jäger конструктивно создавшие PTO для теорий П^1_1-CA_0 и KPI соответственно, затем в 90-е Rathjen создавший PTO для теорий KPM и KP-П_3-reflection, в 2010-е Stegert проанализировавший теории KP-П_n-reflection (с натуральной и трансфинитной индукцией по n), и вот наконец 2020-е и Arai c PTO для П^1_2-CA_0 и в конечном счете Z2.
Кстати, известен такой замечательный факт: если к РА добавить аксиому Con(ZF), выраженную в языке PA, то данная теория PA+Con(ZF) доказывает совместность ZF (и ZFC+CH)
По поводу сложности и доступности для понимания, думаю, вы правы - современная математика (не только логика) идет по пути стремительного роста сложности доказательств (хотя сами результаты при этом могут оставаться доступными для понимания широких масс - взять хотя бы теорему Ферма и ее доказательство). поэтому результаты, думаю, можно объяснить многим, отчасти прибегая к аналогиям и упрощениям, а вот объяснить доказательство становится все труднее и труднее. да что там объяснить - понять даже самим специалистам в данной области! и тут либо нужны какие-то новые идеи для дальнейшего развития самого языка математики, либо какие-то машинные пруферы, доверие к которым будет выше, чем к человечским доказательствам. Николай Вавилов по этому поводу неоднократно высказывался, что современные математические доказательства - это вопрос доверия к их авторам. И это может быть проблемой математики 21 века.
По поводу PTO - если смотреть шире на всю идею (забыв про дремучий лес техники работы с этими понятиями), то я в своих лекциях отмечал (и Лев Беклемишев тоже это упоминал), что само понятие ординала теории, прямо скажем, оставляет желать лучшего, поскольку для той же РА можно определить, с одной стороны, недоказуемый порядок типа ω, с другой стороны - доказуемый порядок длинее, чем ε0. Но оба эти примера в некотором смысле патологические, неестественные. При этом никто не может толком определить, что такое естественный порядок, хотя всякий специалист в каждом конкретном случае легко отличит естественный от неестественного порядка.
Поэтому я думаю, что главный фокус исследований должен заключаться не в поиске очередного "крутого" ординала какой-то теории (это, безусловно, тоже важно, но это уровень кандидатской диссертации и больше напоминает состязания в поисках очередного простого числа). Фокус исследований должен быть направлен на поиск какой-то более внятной концепции того, как вообще мы понимаем математические доказательства и теории, должна ли быть фундированной категория теорий и если да, то как выстроить такую иерархию, каким должен быть язык метаматематики, надо ли его расширять, модифицировать, может быть это вообще должен быть какой-то особенный язык. А может быть мы просто упускаем из виду какие-то альтернативные ZF принципи "овеществления" логики?
Может быть с изменением подходов к исследованиям упростится и их понимание, и доступность для более широких масс (в том числе нематематиков). Хотя вся история математики, вроде бы, говорит об обратном.