объявление: популярный рассказ про матлогику

[kobak]

Завтра в три часа дня я буду рассказывать в гимназии математическому клубу «Эратосфен» о том, что такое математическая логика. Постараюсь излагать так, чтобы было понятно совсем неподготовленным. Если кому-то интересно — приходите. Часика полтора порассказываю, а потом чай будем пить.

В примерной программе: парадокс Рассела, «Principia Mathematica», программа Гильберта, арифметика Пеано, первая теорема Гёделя, вторая теорема Гёделя, связь этих результатов с программированием и проблема останова (с доказательством, пожалуй), результаты типа Харрингтона-Кирби-Париса (конкретно: теорема Гудстайна и задача про Геракла и гидру), континуум-гипотеза в теории множеств, платонизм — и в качестве разговоров уже за чаем: искусственный интеллект и аргументы Пенроуза. Как-то так.

Тема вообще жутко интересная, если кто совсем не в курсе.

Comments

[kobak.livejournal.com]

Ну, неважно, как это назвать. Более или менее понятно, что я успею -- сформулировать все упомянутые результаты в несколько упрощённом виде, объяснить что откуда берётся и какая была логика развития. Вопрос в другом: судя по Вашим репликам, Вы считаете, что это не очень осмысленная задача. А мне кажется, что такое популярное введение в тему для старшеклассников ("чтобы глаза загорелись") и для более страших нематематиков (в качестве расширения кругозора) -- может быть очень полезно и интересно.

[sowa.livejournal.com]

А я думаю, что задача как раз очень осмысленная. Но вряд ли все успеете.

Мне когда-то очень повезло - у нас в классе был маленький "кружок", в котором обсуждались философские аспекты всех этих вещей.

[kobak.livejournal.com]

Я совсем не успел рассказать только про компьютерную сторону дела (остальное успел). Это жаль, потому что я хотел доказать теорему Тьюринга о неалгоритмизуемости halting problem -- и вывести из неё потом теорему Гёделя в её простом варианте. Мне кажется, что такое рассуждение проще всего объяснить (а идея док-ва по большому счёту одна и та же): теорема Тюьринга как-то нагляднее, особенно для тех кто хоть чуть-чуть программировал когда-то.

А так пришлось просто руками помахать, говоря о гёделевской формуле.

(Кстати, к вопросу о философии всего этого дела: мне очень нравится аналогия между теоремой Гёделя и теоремой о невозможности трисекции угла с помощью циркуля и линейки. Последняя никого не поражает: легко сделать вывод о том, что циркуль и линейка -- не слишком совершенные инструменты с ограниченными возможностями. Аксиоматические теории, получается, тоже. К сожалению, я уже не помню, прочитал ли я про циркуль с линейкой где-то у Вас в дискуссиях, или сам придумал.)

[kapahel.livejournal.com]

Меня невозможность тисекции очень даже поажает. Во всяком случае, очень долго так было, потом just got used to.

[sowa.livejournal.com]

Вы и так много рассказали.

Кстати, о том, как объяснять теорему Гёделя. Мне кажется, что часть ее содержания теряется, если она сформулирована в терминах машин Тьюринга. С другой строны, есть замечательное доказательство для некоторой модельной теории, арифметики Шмульяна (Смаллиана). Оно есть в старой книжке Манина "Доказуемое и недоказуемое" (она существует в электронном виде, наверное, есть в Колхозе, у меня есть файл - 2Мег), и, что, может быть, даже больше подходит, в популярной статье Манина в журнале "Природа" (я думаю, это 80-е, как найти - не знаю). Там еще есть, как обычно у Манина, всякие "философские" замечания, которые должны быть особенно интересны.

Идею о том, что формальные теории имеют ограниченные возможности я действительно недавно обсуждал (посты про теорему Лёвенгейма-Сколема), но сравнение с построениями циркулями и линейкой мне в голову не приходило. Это ваше. Очень хорошее сравнение, мне нравится.

[kobak.livejournal.com]

Я посмотрю эту главу в "Доказуемом и недоказуемом", но вряд ли основную конструкцию доказательства можно сделать существенно проще: нужно вводить операцию подстановки в незамкнутую формулу её собственного номера, записывать формулу для такой операции, потом рассматривать некую открытую формулу, включающую в себя в частности и эту операцию, а потом целиком к этой формуле эту же операцию применять -- и тогда получится искомое гёделево утверждение. Это довольно запутанно.

В случае halting problem ровно та же идея воплощается в явном предъявлении нескольких функций, которые передают друг в друга какие-то параметры, -- и всё становится сразу очень понятно. Ну, а связь между этими теоремами легко установить. Я думал об этом исключительно в дидактических целях. Мне кажется, что потеряется при таком "обходном манёвре" не очень много.

А про циркуль и линейку я тогда напишу отдельно.

[ex-dmitri83798.livejournal.com]

"Я посмотрю эту главу в "Доказуемом и недоказуемом", но вряд ли основную конструкцию доказательства можно сделать существенно проще: нужно вводить операцию подстановки в незамкнутую формулу её собственного номера, записывать формулу для такой операции, потом рассматривать некую открытую формулу, включающую в себя в частности и эту операцию, а потом целиком к этой формуле эту же операцию применять -- и тогда получится искомое гёделево утверждение. Это довольно запутанно."

простое на мой взгляд доказательство есть в учебнике Шенфилда (Schoenfield). что в нём ещё хорошо, так это то, что оно концептуально интересно.

там сначала доказывается теорема Чёрча, что любое (непротиворечивое) расширение арифметики неразрешимо. потом доказывается утверждение, что любая рекурсивно аксиоматизируемая полная теория разрешима (архиполезное само по себе утверждение). из этого напрямую делается вывод, что любое рекурсивно аксиоматизированное расширение арифметики неполно (теорема Гёделя).

[kobak.livejournal.com]

Да, я знаю такой вариант рассуждений. Мне он не очень нравится, потому что он в каком-то смысле неконструктивный: гёделево утверждение здесь не предъявляется, в отличие от настоящего доказательства. Но интересно, да.

[ex-dmitri83798.livejournal.com]

да, неконсруктивный. но можно рассказать такое доказтельство, потому что оно проще и занимает меньше времени :) (если не вдаваться в технические детали), а потом сказать, что есть конструктивное доказательство, но формула, которую в нём конструируют, искусственная и является формулировкой парадокса лжеца.

[ex-dmitri83798.livejournal.com]

вот ещё нашёл красивое и простое рассуждение

http://en.wikipedia.org/wiki/Halting_problem#Relationship_with_G.F6del.27s_Incompleteness_Theorem

только они там на самом деле не теорему Гёделя доказывают, а неразрешимость логики первого порядка. но метод важен -- так можно доказать неразрешимость любой логики (что и делают). грубо говоря, если на языке какой-то логики можно написать "эта машина Тьюринга останавливается", то логика неразрешима.

[kobak.livejournal.com]

Да, именно так я и хотел детям рассказывать. От неразрешимости до неполноты один шаг.