Очерки логики

Предел логики и рост компьютеров

AI со времен Аристотеля (часть 2)

Почему на протяжении двадцати пяти веков после Аристотеля интуиции не уделялось столько внимания, как логике? Интуиция неуловима, ее трудно определить и измерить, а иногда и обманчиво. На самом деле интуиция бывает разной. Согласно Аристотелю, интуиция - это маяк, сияющий над тьмой; однако большую часть времени он выглядит как прожектор, указывающий не на те места в темноте. С другой стороны, логика, с помощью которой можно строго продемонстрировать математику, является точной и достоверной, пока вы не вернетесь к основным принципам.

Пуанкаре: использование логики для демонстрации и интуиции для изобретений

Анри Пуанкаре (1854–1921), французский математик и физик, признал, что наша интуиция может вводить в заблуждение, но в первую очередь ответственна за развитие математики. Логическое рассуждение, согласно Пуанкаре, предназначено для окончательной демонстрации результата интуитивного исследования. Он разделил великих математиков на две категории: аналитики, которые следуют логике и неспособны «видеть в пространстве», и геометры, которые следуют интуиции и «быстро устают от долгих вычислений и становятся в недоумении ». Согласно Пуанкаре,

Логика, которая сама по себе может дать уверенность, является инструментом демонстрации; интуиция - инструмент изобретения »(Пуанкаре, 1969).

Представьте, что на уроке элементарной геометрии есть студентка Эми, которая использует интуицию и логику для изучения геометрии. Интуиция используется для изучения диаграмм и поиска стратегий доказательства. Затем с помощью логики шаг за шагом выстраивается доказательство. Эми ставится следующая задача:

Эми сразу вспомнила, что у 180 градусов есть прозвище - плоский угол. Итак, она думает: проблема должна быть связана с прямой линией. Так как его нет, я просто проведу где-нибудь прямую линию. Меня учили рисовать вспомогательную линию при необходимости. Нет другого выбора, кроме как нарисовать одну, касающуюся одной из вершин. Поэтому я произвольно выберу C. Как следует сориентировать линию? Один из очевидных вариантов - сделать его параллельным линии AB. Я смотрю на диаграмму со вспомогательной линией и нахожу, что углы a и d, а также e и b выглядят одинаково, но я, конечно, не должен рассчитывать на диаграмму или точность моего рисунка. Тем не менее, я помню что-то из параллельного постулата, что они действительно равны! Вуаля! a + b + c = e + d + c = 180.

На данный момент все ее идеи по решению этой проблемы исходят из догадок и спонтанных суждений на основе того, чему ее учили в классе. Она больше интуитивно догадывается, чем логически рассуждает. Затем она переключится на свои навыки логического мышления, чтобы соединить точки и продемонстрировать доказательство своему учителю геометрии. Даже с помощью этого тривиального примера Эми демонстрирует, как типичный математик использует интуицию для изобретений и логику для демонстрации.

Рассел: Игры, в которых нет смысла

Вместо того, чтобы отказаться от работы Фреге и изменить направление, Рассел и его коллеги продолжили незавершенную работу Фреге. Однако чем упорнее математики пытались избежать парадоксов, с которыми боролся Фреге, тем тоньше и глубже возникали те из них.

Рассел дал иллюстративную версию своего парадокса, названного парадоксом парикмахера:

Парикмахер бреет всех и только тех, кто не бреется. Парикмахер бреется?

Если парикмахер бреет себя, он, парикмахер, не бреет его. Противоречие. С другой стороны, если парикмахер не побреется, он будет сбриваться парикмахером. Тоже противоречие.

В отличие от Фреге, Рассел отказался от идеи, что аксиомы должны быть самоочевидными, если можно показать, что они развивают математические знания без противоречий. Его процитировали: «Математику можно определить как предмет, в котором мы никогда не узнаем, о чем говорим, и правильно ли то, что мы говорим» . Любые предварительные знания, какими бы очевидными они ни казались, запрещены, и в математическом развитии не должно быть места человеческой интуиции. Неудивительно, что в Principia Mathematica Рассела понадобилось 362 страницы, чтобы вывести 1 + 1 = 2.

Гильберт: Игры, в которых не нужны игроки

Дэвид Гильберт (1862–1943), немецкий математик, расширил работу Фреге и Рассела и предложил знаменитую программу Гильберта, согласно которой любую отрасль математики можно переформулировать как формальную теорию, и спросил, есть ли положительные ответы на следующие 3 вопросов:

  1. Можно ли доказать непротиворечивость формальной теории, в которой из аксиом не могут быть выведены противоречия, внутри самой теории?
  2. Может ли формальная теория оказаться завершенной, в том смысле, что она включает в себя какое-либо истинное математическое утверждение в конкретной ветви, которую она предназначена для воплощения?
  3. Существует ли чисто механическая процедура, которую я называю универсальным механизмом доказательства, которая определяет, является ли какое-либо данное математическое утверждение истинным или ложным. Этот вопрос на немецком языке назывался проблемой решения или Entscheidungsproblem.

Гильберт ожидал, что ответы на все его вопросы будут положительными, что полностью устранило бы необходимость интуиции и сделало бы математику свободной от интуиции. Его оптимизм в отношении формальных теорий заключался в его позитивизме, убеждении в том, что все математические проблемы могут быть решены. Его знаменитая поговорка «Wir müssen wissen, wir werden wissen» (Мы должны знать, мы будем знать) была начертана на его могиле в Геттингене, Германия. Гильберта и его коллег называли «формалистами».

Гильберт считал, что, начав с набора непротиворечивых аксиом, формальная теория может быть полной, самопроверяемой и самооткрываемой. Поскольку формальная теория не предназначена для понимания или интерпретации людьми, а предназначена для использования машинами, ее называют формальной «системой». Ссылаясь на такую ​​систему, как на «формальную», подразумевается, что предыдущее лечение того же предмета было «неформальным», что отражало использование ими интуиции. Относительно своей формальной теории евклидовой геометрии Гильберт однажды заметил, что вместо точек, линий и плоскостей с таким же успехом можно говорить о столах, стульях и пивных кружках.

В то время как Рассел считал математику бессмысленными символическими играми, Гильберт хотел, чтобы в игры играли сами по себе. Если бы грандиозное видение Гильберта было верным, формальная система суммировала бы прошлое и определила бы будущее математики. По иронии судьбы, Хиберт мог ошибиться своей интуицией в этом отношении.

Гёдель: возвращение математиков

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

Кроме того, теория также включает утверждения о том, ли сама теория доказуема. Понимая это, Гёдель гениально сконструировал модифицированную версию парадокса лжеца, как показано ниже:

Это предложение называется приговором Гёделя. Если это правда, то это невозможно доказать в теории, согласно тому, что там говорится. Если он ложен, то то, что он говорит, должно быть ложным, что означает, что это доказуемо в теории, и, следовательно, оно должно быть правдой. Итак, у нас есть истинное математическое утверждение, которое нельзя ни доказать, ни опровергнуть в теории. Формальная система математической теории, даже такая элементарная, как теория чисел, является лишь приближением.

Тьюринг: рост программистов

Что вычислимо?

Даже если мы довольствуемся неполной формальной системой, существует ли универсальный механизм доказательства для решения проблемы принятия решения? Прежде чем углубиться в вопрос, мы должны ответить, что такое «чисто механическая процедура». Алан Тьюринг (1912–1954), английский математик, определил математическую модель «чисто механической процедуры», вдохновленную пациентом и подчиняющимся правилам человеком-компьютером (обычно женщиной), выполняющим свою работу с помощью карандаша и бумаги. Машина, определенная в модели, сканирует гипотетическую ленту, разделенную на квадраты. Следуя таблице правил и собственному внутреннему состоянию, он затем пишет символ на квадрате, а затем либо остается на месте, либо перемещается на один квадрат вправо или влево. Эта модель машины позже была названа машиной Тьюринга, которую он использовал для математических аргументов вместо создания реального компьютера. Обычно считается, что все во Вселенной вычислимо тогда и только тогда, когда оно может быть сведено к машине Тьюринга. Это называется гипотезой Черча-Тьюринга. Упомянутая выше таблица правил теперь называется «компьютерной программой».

Проблема остановки

Определив машину Тьюринга, Тьюринг приступил к доказательству отсутствия универсального механизма доказательства Гильберта. Вдохновленный схемой нумерации Гёделя, Тьюринг кодировал машины как числа, так что машины можно было изучать как числа, которые можно было использовать в качестве входных данных для других машин. Теперь Тьюринг мог задать проблему остановки: существует ли машина под названием останавливающий оракул, которая могла бы решить, остановится ли какая-либо машина на заданном входе или в цикле навсегда. Тьюринг гениально избежал необходимости объяснять детали такой абсурдно мощной машины, показав, что простое ее существование привело бы к противоречию.

Тьюринг предположил, что существует особая машина M, которая делает прямо противоположное тому, что делает останавливающийся оракул. Если останавливающийся оракул решает, что машина останавливается, принимая себя в качестве входных данных, M будет повторяться бесконечно. С другой стороны, если останавливающийся оракул решает, что машина зацикливается вечно, M в этом случае остановится. Таким образом, вы можете сказать, что M преднамеренно саботирует останавливающийся оракул. Теперь вопрос: останавливается ли специальная машина M, когда принимает себя в качестве входных данных?

  1. Если M останавливается на M, M будет повторяться вечно по определению M: противоречие.
  2. Если M зацикливается на M, M остановится. Еще одно противоречие

Этот парадокс референции проиллюстрирован ниже:

Следовательно, останавливающийся оракул не может существовать. Проблема остановки не может быть решена или технически неразрешима.

Теперь мы можем вернуться к проблеме принятия решений Гильберта. Если бы универсальный механизм доказательства существовал, мы могли бы сделать его останавливающимся оракулом, сформулировав любой запрос для останавливающегося оракула в виде математического утверждения. Однако не существует останавливающегося оракула, как и универсального механизма доказательства. С другой стороны, если бы останавливающийся оракул действительно существовал, мы могли бы реализовать универсальный механизм доказательства следующим простым способом: во-первых, написать программу, которая будет бесконечно искать все возможные доказательства математического утверждения и останавливаться, когда найдет их; Затем мы спрашиваем останавливающегося оракула, останавливается ли такая программа поиска. Следовательно, неразрешимость проблемы остановки подразумевает неразрешимость проблемы решения, и наоборот.

Вообразив, что останавливающийся оракул существует, мы легко решим многие сложные или открытые теоретико-числовые задачи. Например, мы могли бы доказать гипотезу Гольдбаха, которая гласит, что каждое четное число больше 2 является суммой двух простых чисел. Мы могли бы просто написать программу, которая перебирает все четные числа, начиная с 4, и проверяет, действительно ли каждое из них является суммой двух простых чисел. Затем мы докажем гипотезу, скармливая программу останавливающемуся оракулу и спрашивая, останавливается ли он. В действительности эта проблема остается нерешенной.

Другой способ описать несуществующий останавливающий оракул и универсальный механизм доказательства - сказать, что они не «вычислимы», согласно гипотезе Черча-Тьюринга. По словам Гёделя, его результаты

Не устанавливайте никаких границ для возможностей человеческого разума, а скорее для возможностей чистого формализма в математике.

Другими словами, то, что показали Гёдель и Тьюринг, было ограничением логических рассуждений без использования интуиции. Они фактически подтвердили точку зрения Пуанкаре о том, что, несмотря на ее строгость и определенность, логика - это всего лишь демонстрационный инструмент, и его нужно дополнять интуицией.

В отсутствие «метаматематического» решения для доказательства «всех» математических проблем область «автоматического доказательства теорем» с менее амбициозными, но более прагматическими возможностями, чем программа Гильберта, была активной и процветающей. Формальные теории Гильберта оказались приближениями к математическим знаниям. Подобно тому, как физическая реальность Вселенной по-прежнему остается загадкой, призывающей физиков разгадывать ее, границы математических знаний остаются для математиков неуловимыми. Теперь математики и их интуиция вернулись в игру.

Рождение компьютера и рост программистов

В доказательстве проблемы остановки должен быть способ для M гипотетической машины запустить сам останавливающийся оракул, чтобы его саботировать. Для этого Тьюринг создал универсальную машину, которая может считывать кодировку любой машины Тьюринга и действовать от ее имени. Со стороны вы не сможете сказать, универсальная машина или конкретная машина выполняет эту работу. Современные компьютеры основаны на универсальной машине, которую часто называют «достаточно мощной», чтобы делать все, что только можно вообразить. Но откуда у него сила? На самом деле это пустая оболочка, предназначенная для запуска других машин Тьюринга, которые, должно быть, были написаны кем-то не с помощью логических рассуждений, а с творческим подходом, пониманием, суждениями и многими другими аспектами наших умственных усилий, которые в совокупности можно назвать интуицией. С этой точки зрения Тьюринг не только изобрел компьютер, но и создал роль программистов, которые несут ответственность за использование «выразительной силы» универсальной машины для ее программирования. Вместо всемогущей логической машины, которая запирается в башне из слоновой кости, у нас есть универсальный компьютер, который затрагивает практически все аспекты нашей повседневной жизни!

[Часть 1: Логика, интуиция и парадокс]

[Часть 3: Интуиция, сложность и последний парадокс]

Библиография

  • Ааронсон, С. (2016). P =? NP. В разделе Открытые задачи по математике. Springer.
  • Аристотель «О риторике»: теория гражданского дискурса (Дж. А. Кенди, пер.). (1991). Издательство Оксфордского университета.
  • Бансал, К., Лоос, С., Рабе, М., Сегеди, К., и Уилкокс, С. (2019). HOList: среда для машинного обучения доказательства теорем высокого порядка. Материалы 36-й конференции по машинному обучению.
  • Бансал, К., Сегеди, К., Рабе, М. Н., Лоос, С. М., и Томан, В. (2020). Учимся рассуждать в больших теориях без подражания. Https://arxiv.org/pdf/1905.10501.pdf
  • Борель, Э. (1962). Вероятности и жизнь. Dover Publications, Inc.
  • Копленд, Дж. Б., Пози, К. Дж., и Шагрир, О. (2013 г.). Вычислимость: Тьюринг, Гёдель, Черч и не только (изд. Kindle). MIT Press.
  • Хеул, М. Дж. Х., Куллманн, О., и Марек, В. В. (2016). Решение и проверка логической проблемы троек Пифагора с помощью Cube-and-Conquer. В конспектах лекций по информатике (стр. 228–245). Издательство Springer International. 10.1007 / 978–3–319–40970–2_15
  • Пуанкаре, Х. (1969). ИНТУИЦИЯ и ЛОГИКА в математике. Учитель математики, 62 (3), 205–212.
  • Полу С., Суцкевер И. (2020). Генеративное языковое моделирование для автоматизированного доказательства теорем. arxiv.org. Https://arxiv.org/abs/2009.03393
  • Поля Г. (1954). Индукция и аналогия в математике.
  • Поля Г. (1954). Математика и правдоподобные рассуждения. Издательство Мартино.
  • Поля Г. (1973). Как это решить (Второе изд.). Издательство Принстонского университета.
  • Сельсам, Д., Ламм, М., Бунц, Б., Лян, П., Дилл, Д.Л., & де Моура, Л. (2019). Изучение решателя SAT от Single -Bit Supervision. Https://arxiv.org/abs/1802.03685