Зачем изучать логику

Концепция концепций

Если вы пытаетесь что-либо кому-либо объяснить, то сделать это будет гораздо легче, если найти нечто другое, но похожее, что человек уже смог понять. Представьте, как вы будете объяснять концепцию современного дрона человеку из Каменного века. Это будет сложно сделать. Но объяснить это человеку, жившему 50 лет назад, и уже видевшему вертолёты и модели самолётов, будет гораздо легче.

И в итоге суть в том, что когда мы что-то объясняем, мы делаем это на языке, известном как нам, так и тому, кому мы это объясняем. И чем богаче язык, тем меньше новых элементов нам приходится вводить, чтобы передать то, что мы пытаемся объяснить.

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

Допустим, мы заметили такие вещи, как вода, кровь и масло. В какой-то момент мы понимаем, что существует обобщённая концепция «жидкости», и всех их можно описать как жидкость. И когда у нас появляется такая концепция, в её терминах можно начинать рассуждать, находя больше концепций – допустим, вязкость – основанных на ней.

Когда имеет смысл объединять вещи в концепцию? Сложный вопрос, на который нельзя ответить, не предусмотрев всё, что можно с этой концепцией сделать. На практике, в процессе эволюции языка и идей человека, наблюдается некий процесс последовательной аппроксимации.

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

Честно говоря, то, что происходит с FeatureSpacePlot – как и в процессе интеллектуального развития человека – в каком-то смысле пошаговый процесс. Чтобы распределить объекты по пространству особенностей, FeatureSpacePlot использует особенности, которые она научилась извлекать на основе предыдущих попыток разделения на категории.

Хорошо, если мы примем мир, какой он есть, какие наилучшие категории – или концепции – можно использовать для описания вещей? Этот вопрос постоянно развивается. И вообще, все прорывы – будь то наука, технология или что-то ещё – часто точно связываются с осознанием возможности полезным образом идентифицировать новую категорию или концепцию.

Но в процессе эволюции нашей цивилизации присутствует некая спираль. Во-первых, определяется некая определённая концепция – допустим, идея программы. После этого люди начинают её использовать и размышлять в её терминах. Довольно скоро на базе этой концепции оказывается построенным множество разных понятий. А затем определяется ещё один уровень абстракции, создаются новые концепции, стоящие на основе предыдущей.

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

Будущее понимания

Что же всё это означает для будущего понимания?

В прошлом, когда люди изучали природу, у них было небольшое количество причин для её понимания. Иногда они персонифицировали определённые её аспекты в виде духов или божеств. Но они принимали её такой, какая она есть, не думая о возможности понять все детали причин процессов.

С появлением современной науки – и особенно когда всё большая часть наших жизней проходит в искусственных окружениях, где доминируют технологии, разработанные нами – эти ожидания поменялись. И когда мы изучаем вычисления, проводимые ИИ, нам не нравится, что мы можем их не понять.

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

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

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

Что насчёт таких областей, как математика? В математике мы привыкли к тому, что мы строим набор наших знаний так, чтобы мы могли понимать каждый шаг. Но экспериментальная математика – как и такие возможности, как автоматическое доказательство теорем – делают очевидным существование таких областей, в которых нам будет недоступен такой метод.

Будем ли мы называть их «математикой»? Думаю, что должны. Но эта традиция отличается от той, к которой мы привыкли за последнее тысячелетие. Мы всё ещё можем создавать там абстракции, и конструировать новые уровни понимания.

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

Зачем нужны доказательства?

В каком-то смысле, доказательство нужно, чтобы знать истинность чего-либо. Конечно, особенно в наше время, доказательство отошло на второй план, уступив место чистым вычислениям. На практике гораздо чаще встречается желание сгенерировать что-либо вычислениями, чем желание «отойти назад» и сконструировать доказательство истинности чего-либо.

В чистой математике, тем не менее, часто приходится сталкиваться с понятиями, включающими в себя, хотя бы номинально, бесконечное количество случаев («истинно для всех простых чисел», и т.п.), для которых вычисления «в лоб» не подойдут. А когда встаёт вопрос о подтверждении («может ли эта программа завершиться с ошибкой?» или «можно ли потратить эту криптовалюту дважды?») чаще разумнее попытаться до казать это, чем просчитать все возможные случаи.

Но в реальной математической практике, доказательство – это нечто большее, чем установление истины. Когда Евклид писал свои «Начала», он просто указывал результаты, а доказательства «оставлял читателю». Но, так или иначе, особенно за последнее столетие, доказательство превратилось в нечто, что не просто происходит за кулисами, а является основным носителем, через которые необходимо транслировать понятия.

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

Но одной из основных целей моей деятельности за последние несколько десятилетий было изменить такое положение вещей, и разработать в Wolfram Language настоящий «язык вычислительного общения», в котором вычислительные идеи можно передавать так, что их смогут понять и компьютеры, и люди.

У такого языка есть много последствий. Одно из них – изменение роли доказательства. Допустим, мы смотрим на какой-то математический результат. В прошлом единственным правдоподобным способом довести его до понимания было выдать доказательство, читаемое людьми. Но теперь возможно и другое: можно выдать программу для Wolfram Language, подсчитывающую результат. И это во многих смыслах гораздо более богатый способ донести истинность результата. Каждая часть программы представляет собой нечто точное и недвусмысленное – каждый желающий может её запустить. Нет такой проблемы, как попытки понять какую-то часть текста, требующие заполнять некие пробелы. Всё указано в тексте совершенно чётко.

Что насчёт доказательств? Есть ли недвусмысленные и точные способы писать доказательства? Потенциально да, хотя это не особенно легко. И хотя основа Wolfram Language существует уже 30 лет, только сегодня появился разумный способ представлять с его помощью такие структурно прямолинейные доказательства, как одна из моих аксиом выше.

Можно представить себе создание доказательств в Wolfram Language так же, как люди создают программы – и мы работаем над тем, чтобы предоставить высокоуровневые версии такой функциональности, «помогающей с доказательствами». Однако доказательство моей системы аксиом никто не создавал – его нашёл компьютер. И это уже больше похоже на выходные данные программы, чем на саму программу. Однако, как и программу, доказательство в некотором смысле тоже можно «запустить» для проверки результата.

История

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

Однако к XV веку изобрели алгебру, а с ней появилось более ясное представление вещей. Но только в 1847 году Джордж Буль, наконец, сформулировал логику так же, как алгебру, с логическими операциями типа AND и OR, работающими по правилам, похожим на правила алгебры.

Через несколько лет люди уже записывали аксиоматические системы для логики. Типичным примером было:

Но нужны ли на самом деле для логики AND, OR и NOT? После первого десятилетия XX века несколько людей обнаружили, что достаточно будет единственной операции, которую мы теперь называем NAND, и, к примеру, p OR q можно вычислить, как (p NAND p) NAND (q NAND q). «Функциональная полнота» NAND могла навеки остаться диковиной, если бы не разработка полупроводниковой технологии – она реализует все миллиарды логических операций в современном микропроцессоре при помощи комбинации транзисторов, выполняющих лишь функцию NAND или связанную с ней NOR.

Ну хорошо, так как же выглядят аксиомы логики в терминах NAND? Вот первый известный их вариант, записанный Генри Шеффером в 1913 году (здесь точка обозначает NAND):

В 1910-м Principia Mathematica, трёхтомный труд по логике и философии математики Альфреда Норта Уайтхеда и Бертрана Рассела, популяризовал идею о том, что, возможно, всю математику можно вывести из логики. Учитывая это, довольно интересно было изучить вопрос того, насколько простыми могут быть аксиомы логики. Наиболее значимые работы в этой области проводили во Львове и Варшаве (тогда эти города были в составе Польши), в частности, Ян Лукасевич (в качестве побочного эффекта своей работы в 1920-м изобрёл «польскую» запись, не требующую скобок). В 1944 году в возрасте 66 лет Лукасевич бежал от наступающей советской армии и в 1947-м оказался в Ирландии.

Тем временем ирландец Кэрью Мередит, учившийся в Винчестере и Кембридже, и ставший преподавателем математики в Кембридже, из-за своего пацифизма был вынужден вернуться в Ирландию в 1939-м. В 1947-м Мередит попал на лекцию Лукасевича в Дублине, что вдохновило его заняться поисками простых аксиом, чем он и занимался, по большей части, всю оставшуюся жизнь.

Уже к 1949 Мередит обнаружил двухаксиомную систему:

Почти 20 лет работы спустя, в 1967 ему удалось упростить это до:

А можно ли упростить это и далее? Мередит годами возился с этим, выясняя, где ещё можно убрать лишние NAND. Но после 1967-го дальше он уже не продвинулся (и умер в 1976), хотя в 1969-м он нашёл трёхаксиомную систему:

Когда я начал изучать аксиомные системы логики, я ничего не знал о работе Мередита. Я увлёкся этой темой в рамках попыток понять, какое поведение может вырастать из простых правил. В 1980-х я сделал неожиданное открытие, что даже клеточные автоматы с простейшими из возможных правил – таких, как моё любимое правило 30 – могут приводить к невероятно сложному поведению.

Проведя 1990-е в попытках понять общность этого явления, я в итоге захотел посмотреть, как его можно применить к математике. В математике мы, по сути, начинаем работать с аксиом (допустим, в арифметике, в геометрии, в логике), а потом на их основе пытаемся доказать целый набор сложных теорем.

Однако насколько простыми могут быть аксиомы? Именно это я хотел установить в 1999-м. В качестве первого примера я решил изучить логику (или, что то же самое, булеву алгебру). Опровергая все мои ожидания, мой опыт с клеточными автоматами, машинами Тьюринга и другими системами – включая даже дифференциальные уравнения в частных производных – говорит о том, что можно просто начать перечислять наиболее простые случаи из возможных, и в какой-то момент увидеть кое-что интересное.

Но можно ли таким способом «открыть логику»? Был лишь один способ сказать это. И в конце 1999 я устроил всё так, чтобы начать изучать пространство всех возможных систем аксиом, начиная с самых простых.

Было довольно легко проверить, что аксиомы, в которых было 3 или меньше NAND (или «оператора точка») не работали. К 5 утра в воскресенье, 29 января (ага, тогда я был совой), я обнаружил, что не сработают и аксиомы, содержащие 4 NAND. Когда я прекратил работу, примерно к 6 утра, у меня на руках было 14 кандидатов с пятью NAND. Но продолжив работу вечером в воскресенье и проведя дополнительные испытания, пришлось отбросить их все.

Незачем и говорить, что следующим шагом стала проверка аксиом с 6 NAND. Их оказалось 288 684. Но мой код работал эффективно, и прошло не так много времени перед тем, как на экране появилось следующее (да, из Mathematica Version 4):

Сначала я не понял, что у меня получилось. Я только знал, что у меня есть 25 неэквивалентных аксиом с 6 NAND, которым удалось продвинуться дальше, чем аксиомам с 5 NAND. Но были ли среди них аксиомы, порождающие логику? У меня был эмпирический метод, способный отбрасывать ненужные аксиомы. Но единственным способом точно узнать правильность конкретной аксиомы было доказать, что она успешно способна воспроизвести, допустим, аксиомы Шеффера для логики.

Потребовалось немного поиграться с программами, но по прошествии нескольких дней я обнаружил, что большая часть из полученных 25 аксиом не работает. В итоге выжили две:

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

Вскоре после этого я обнаружил системы из двух аксиом с 6 NAND в целом, которыке, как я доказал, способны воспроизводить логику:

А если принять коммутативность p · q = q · p, как само собой разумеющееся, тогда логику можно получить из аксиомы, содержащей всего 4 NAND.

Зачем и где применяют логическое программирование

Давайте вернемся к рассмотренным примерам и попробуем представить, как это можно использовать на практике.

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

Механика доказательства

Ладно, так как же доказать корректность моей системы аксиом? Первое, что приходит в голову – показать, что из неё можно вывести известную систему аксиом для логики – например, систему аксиом Шеффера:

Здесь присутствуют три аксиомы, и нам надо вывести каждую. Вот, что можно сделать для вывода первой, при помощи последней версии Wolfram Language:

Примечательно, что сейчас стало возможным сделать это. В «объекте доказательства» записано, что для доказательства было использовано 54 шага. Исходя из этого объекта мы можем сгенерить «notebook », описывающий каждый из шагов:

В общем здесь доказывается вся последовательность промежуточных лемм, что позволяет в итоге вывести конечный результат. Между леммами существует целая сеть взаимных зависимостей:

А вот сети, участвующие в выводе всех трёх аксиом в системе аксиом Шеффера – для последней используются невероятные 504 шага:

Да, очевидно, что эти сети довольно запутаны. Но перед тем, как обсудить, что означает эта сложность, поговорим о том, что происходит на каждом шаге этих доказательств.

Главная идея проста. Представим, что у нас есть аксиома, которая просто записывается, как p · q = q · p (математически это означает, что оператор коммутативен). Точнее, аксиома говорит, что для любых выражений p и q, p · q эквивалентно q · p.

Хорошо, допустим мы хотим вывести из этой аксиомы, что (a · b) · (c · d) = (d · c) · (b · a). Это можно сделать, используя аксиому для превращения d · c в c · d, b · a в a · b, и, наконец, (c · d) · (a · b) в (a · b) · (c · d).

FindEquationalProof делает по сути то же самое, хотя она выполняет эти шаги не совсем в том же порядке, и изменяет как левую часть уравнения, так и правую.

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

Можно было бы решить: почему бы не попробовать все возможные последовательности, и если среди них есть рабочая, то она должна в итоге найтись? Проблема в том, что можно быстро прийти к астрономическому количеству последовательностей. Основная часть искусства автоматического доказательства теорем состоит из поиска способов уменьшения количества последовательностей для проверки.

Это быстро скатывается в технические подробности, но основную идею легко обсудить, если знать азы алгебры. Допустим, мы пытаемся доказать алгебраический результат вроде

Существует гарантированный способ сделать это: просто применив правила алгебры для раскрытия каждой из сторон, можно сразу увидеть их сходство:

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

Не прямо сразу. В алгебре это работает, поскольку у неё есть особое свойство, гарантирующее, что всегда можно «продвигаться» по пути упрощения выражений. Но в 1970-х разные учёные несколько раз независимо друг от друга открыли (под названиями вроде алгоритм Кнута-Бендикса или базис Грёбнера), что даже если у системы аксиом нет необходимого внутреннего свойства, потенциально можно обнаружить «дополнения» этой системы, у которых оно есть.

Именно это происходит в типичных доказательствах, которые выдаёт FindEquationalProof (основанная на системе Валдмейстера, «master of trees»). Существуют т.н. «леммы критических пар», которые напрямую не продвигают доказательство, но делают возможным появление путей, способных на это. Усложняется всё из-за того, что, хотя окончательное выражение, которые мы хотим получить, довольно короткое, на пути к нему, возможно, приходится проходить через куда как более длинные промежуточные выражения. Поэтому, к примеру, у доказательства первой аксиомы Шеффера есть такие промежуточные шаги:

В данном случае крупнейший из шагов оказывается в 4 раза больше оригинальной аксиомы:

Такие выражения можно представлять в виде дерева. Вот его дерево, в сравнении с деревом первоначальной аксиомы:

И вот как размеры промежуточных шагов развиваются в ходе доказательств каждой из аксиомы Шеффера:

Создавая понятность

Пользы в том, чтобы объяснить, как результат был получен на самом деле, не было бы; это очень неподходящий для человека процесс. Ей нужно понять, какие операции, выученные людьми, можно использовать для получения результата. Часто она придумывает какой-нибудь полезный трюк. Да, у неё есть систематический способ для этого, который всегда работает. Но в нём слишком много «механических» этапов. А «трюк» (подстановка, частичное интегрирование, и т.п.) не сработает в общем случае, но в данном конкретном он выдаст более быстрый путь к ответу.

А что же насчёт получения понятных версий других вещей? Например, работы программ в общем случае. Или доказательства моей системы аксиом.

Нужно затрачивать усилия на то, чтобы программа на Wolfram Language была хорошим описанием процесса, как и на то, чтобы простой текст на английском языке был хорошим описанием процесса. Однако можно получить такой кусок кода на Wolfram Language, который очень чётко объясняет, как всё работает, сам по себе.

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

В таком случае я обнаружил, что вычислительные эссе, представленные в виде Wolfram Notebooks, являются прекрасным инструментом для пояснения происходящего. Важно, что Wolfram Language, это позволяет запускать даже самые мелкие части программ по отдельности (с соответствующими символическими выражениями в роли входных и выходных данных). После этого можно представить себе последовательность шагов программы как последовательность элементов диалога, формирующего основу вычислительной записной книжки.

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

Конечно, создание хороших визуализаций сродни искусству. Но в Wolfram Language мы проделали большую работу по автоматизации этого искусства – часто при помощи довольно сложного машинного обучения и других алгоритмов, выполняющих такие вещи, как раскладка сетей или графических элементов.

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

На каком-то уровне эта задача похожа на реверс-инжиниринг. Вам демонстрируют машинный код, схему чипа, что угодно. А вам надо сделать шаг назад и воссоздать высокоуровневое описание, от которого отталкивался человек, которое каким-то образом «скомпилировалось» в то, что вы видите.

В традиционном подходе к инженерному делу, когда люди создают продукт по шагам, всегда имея возможность предвидеть последствия того, что они создают, этот подход в принципе может сработать. Но если вместо этого просто бродить по вычислительной вселенной в поисках оптимальной программы (так, как я искал возможные системы аксиом, чтобы найти систему для логики), то нет гарантии, что за этой программой окажется какая-то «человеческая история» или объяснение.

Сходная проблема встречается в естественных науках. Вы видите, как в биологической системе развивается сложный набор всяких процессов. Можно ли подвергнуть их «реверс-инжинирингу» с целью найти «объяснение»? Иногда можно сказать, что к этому приведёт эволюция с естественным отбором. Или что это часто встречается в вычислительной вселенной, поэтому вероятность его возникновения высока. Но нет гарантий, что естественный мир обязательно устроен так, чтобы люди могли его объяснить.

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

Будущее познания

Изучая математику, науку или технологии, можно увидеть сходные базовые пути качественного развития, состоящие в построении набора всё увеличивающихся абстракций. Было бы неплохо количественно оценить этот процесс. Возможно, можно подсчитать, как определённые термины или описания, часто встречавшиеся в одно время, включаются в более высокие уровни абстракции, на которых в свою очередь появляются новые термины или описания, связанные с ними.

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

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

Но что же произойдёт, если этот процесс будет повторяться снова и снова, воспроизводя идеализированную интеллектуальную историю человека и создавая растущую всё выше башню абстракций?

Предположительно, тут можно провести аналогию с критическими явлениями в физике и методом ренормализационной группы. Если так, можно представить, что мы сможем определить траекторию в пространстве платформ для представления концепций. Что будет делать эта траектория?

Возможно, у неё будет фиксированное значение, когда в любой момент истории существует примерно одинаковое количество стоящих изучения концепций – новые концепции медленно открываются, а старые поглощаются.

Что это может означать для математики? Например, что любые «случайные математические факты», открытые эмпирически, в итоге будут рассмотрены при достижении определённого уровня абстракции. Нет очевидного понимания того, как этот процесс будет работать. Ведь на любом уровне абстракции всегда есть новые эмпирические факты, к которым надо «перепрыгнуть». Может произойти и так, что «поднятие уровня абстракции» будет двигаться медленнее, чем нужно для совершения этих «прыжков».

Применение логики

Логическое мышление применяется практически в каждой области человеческой деятельности (гуманитарные науки, экономика, риторика, творческая деятельность и т.п.). К примеру, в математических науках  или философии применяют строгую и формализованную логику.  В других же сферах логика служит источником полезных знаний необходимых для получения обоснованного вывода всей ситуации в целом.

Человек старается применять логические навыки на подсознательном уровне. Кто-то с этим справляется лучше, кто-то хуже. Но в любом случае используя нашу логику нам необходимо знать, что мы можем делать с ее помощью:

• Подбирать необходимый метод решения проблемы;
• Быстрее мыслить;
• Качественно излагать свои мысли;
• Избегать самообмана;
• Находить и корректировать ошибки других людей в их умозаключениях;
• Подбирать необходимые аргументы для убеждения собеседника в своей правоте.

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

Природа объяснимости

Что означает фраза «нечто можно объяснить»? По сути это значит, что люди могут это понять.

Что же требуется от людей для того, чтобы что-то понять? Нам нужно каким-то образом это осознать. Возьмём типичный клеточный автомат со сложным поведением. У компьютера нет никаких проблем с тем, чтобы пройти каждый шаг в его эволюции. С огромными усилиями и трудозатратами человек мог бы воспроизвести работу компьютера.

Но нельзя сказать, что в этом случае человек «понял» бы, что делает клеточный автомат. Для этого человек должен был бы с лёгкостью рассуждать о поведении клеточного автомата на высоком уровне. Или, иначе говоря, человек должен был бы суметь «рассказать историю» о поведении автомата, которую могли бы понять другие люди.

Есть ли универсальный способ для этого? Нет, из-за вычислительной несводимости. Однако может случиться так, что определённые особенности, важные для людей, можно объяснить на высоком уровне с определёнными ограничениями.

Как это работает? Для этого нужно создать некий язык высокого уровня, который может описывать интересующие нас особенности. Изучая типичный рисунок работы клеточного автомата, можно попытаться говорить не в терминах цветов огромного количества отдельных клеток, а в терминах структур более высоко уровня, которые можно обнаружить. Главное, что можно составить по крайней мере частичный каталог таких структур: хотя в них будет много деталей, не укладывающихся в классификацию, определённые структуры встречаются часто.

И если мы хотим начать «объяснять» поведение клеточного автомата, мы начнём с наименования структур, а потом расскажем о том, что происходит с точки зрения этих структур.

У случая с клеточным автоматом есть одна упрощающая особенность: поскольку он работает на основе простых детерминистских правил, у него есть одинаково повторяющиеся структуры. В природе, к примеру, мы обычно не сталкиваемся с подобным идентичным повторением. Там просто один, допустим, тигр, очень похож на другого, поэтому мы называем их обоих «тигр», хотя расположение их атомов не идентично.

Каков во всём этом общий смысл? Он состоит в использовании идеи символической репрезентации. Мы говорим, что можем назначить некий символ – часто это слово – которое можно использовать для символического описания целого класса вещей, без того, чтобы всякий раз детально перечислять все составляющие этих вещей.

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

Допустим, мы сгенерировали гигантскую структуру, например, математическую:

Первый шаг – создать некое внутреннее представление высокого уровня. К примеру, мы можем обнаружить повторно употребляемые структуры. И мы можем назначить им имена. А потом показать «скелет» всей структуры с их помощью:

Да, эта, похожая на «словарное сжатие» схема, полезна для выхода на первый уровень объяснимости.

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

Какой ещё можно сделать шаг? Нам нужно придумать какое-то описание ещё более высокого уровня. Что это может быть?

Логическое доказательство и автоматизация абстракции

Вернёмся к логическим доказательствам. Как они связаны с типичной математикой? Пока что никак. Да, у доказательства есть номинально та же форма, что и у стандартного математического доказательства. Но оно не «дружелюбно к людям-математикам». Это только механические детали. Оно не связано с абстрактными концепциями высокого уровня, которые будут понятными человеку-математику.

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

Но как без этого сделать объяснимым доказательство?

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

Не уверен, как это сделать. Я рассматривал возможность назначить премию (что-то вроде моей премии 2007 года за машину Тьюринга) за «преобразование доказательства в объяснимый вид». Однако совершенно непонятно, как можно оценить «объяснимость». Можно было бы попросить записать часовое видео, в котором было бы дано успешное объяснение доказательства, подходящее для типичного математика – но это было бы весьма субъективно.

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

Здесь прослеживается аналогия с разработкой языков. Создавая Wolfram Language, я пытаюсь идентифицировать «куски вычислительной работы», которые часто нужны людям. Мы создаём из них встроенные в язык функции, с определёнными именами, которые люди могут использовать, чтобы на них ссылаться.

Похожий процесс идёт – хотя вовсе не так организованно – в эволюции естественных языков. «Куски смысла», оказывающиеся полезными, в итоге получают свои слова в языке. Иногда они начинаются с фраз, состоящих из нескольких существующих слов. Но наиболее влиятельные обычно оказываются настолько далеко от существующих слов, что они появляются в виде новых слов, дать определение которым потенциально довольно сложно.

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

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

Но что делает лемму «интересной по сути»? Надо сказать, что до того, как я поработал над своей книгой, я обвинял в выборе лемм (или терем) в любой области математики, которую описывают и именуют в учебниках, большой произвол и исторические случайности.

Но, детально разобрав теоремы из базовой логики, я удивился, найдя нечто совсем другое. Допустим, что мы выстроили все правильные теоремы логики по порядку их размера
(к примеру, p = p будет первой, p AND p = p – чуть позже, и т.д.). В этом списке довольно много избыточности. Большая часть теорем оказывается тривиальным расширением теорем, которые уже появлялись в списке.

Но иногда появляется теорема, выдающая новую информацию, которую нельзя доказать на основе теорем, уже появлявшихся в списке. Примечательный факт: таких теорем 14, и они, по сути, точно соответствуют теоремам, которым обычно дают названия в учебниках по логике (здесь AND – это ∧, OR это ∨, а NOT это ¬.)

Иначе говоря, в данном случае именованными, или «интересными» теоремами оказываются именно те, что делают заявления о новой информации минимального размера. Да, по такому определению через какое-то время новой информации уже не останется, поскольку мы получим все аксиомы, необходимые для того, чтобы доказать всё, что можно – хотя можно пойти и дальше, начав ограничивать сложность допустимых доказательств.

Что насчёт теорем NAND, например, тех, что встречаются в доказательстве? Опять-таки, можно выстроить все истинные теоремы по порядку, и найти, какие из них нельзя доказать на основе предыдущих теорем из списка:

У NAND нет такой исторической традиции, как у AND, OR и NOT. И, судя по всему, не существует человеческого языка, в котором бы NAND обозначалось одним словом. Но в списке теорем NAND первую из отмеченных легко опознать как коммутативность NAND. После этого нужно лишь немного переводов, чтобы дать им имена: a = (a · a) · (a · a) похожа на двойное отрицание, a = (a · a) · (a · b) похожа на закон поглощения, (a · a) · b = (a · b) · b похожа на «ослабление», и так далее.

Хорошо, если мы собираемся выучить несколько «ключевых теорем» логики NAND, какие это должны быть теоремы? Возможно, это должны быть «популярные леммы» в доказательствах.

Конечно, у любой теоремы может существовать много возможных доказательств. Но, допустим, мы будем использовать только доказательства, которые выдаёт FindEquationalProof. Тогда оказывается, что в доказательстве первой тысячи теорем NAND самой популярной леммой будет a · a = a · ((a · a) · a), за которой следуют леммы типа (a · ((a · a) · a)) · (a · (a · ((a · a) · a))) = a.

Что это за леммы? Они полезны для методов, используемых FindEquationalProof. Но для людей они, кажется, не очень подходят.

А что насчёт лемм, которые оказываются короткими? a · b = b · a определённо не самая популярная, но самая короткая. (a · a) · (a · a) = a популярнее, но длиннее. А ещё есть такие леммы, как (a · a) · (b · a) = a.

Насколько эти леммы будут полезны? Вот один из способов проверить это. Посмотрим на первую тысячу теорем NAND и оценим, насколько добавление лемм укорачивает доказательства этих теорем (по крайней мере тех, что нашла FindEquationalProof):

a · b = b · a очень успешна, и часто урезает доказательство почти на 100 шагов. (a · a) · (a · a) = a гораздо менее успешна; она иногда даже «сбивает с толку» FindEquationalProof, заставляя сделать больше шагов, чем нужно (отрицательные величины на графиках). (a · a) · (b · a) = a неплохо справляется с сокращением, но не так хорошо, как a · b = b · a. Хотя, если скомбинировать её с a · b = b · a, в результате сокращения случаются чаще.

Анализ можно продолжать, допустим, включив сравнение того, насколько конкретная лемма укорачивает длины доказательств по отношению к изначальной их длине. Но проблема в том, что если добавить несколько «полезных лемм» вроде a · b = b · a и (a · a) · (b · a) = a, остаётся ещё много длинных доказательств – то есть, много того, что необходимо «понять».

Зачем нужно знакомство с логикой?

В
наш прагматичный век, сталкиваясь с
чем-то для себя новым, люди первым делом
спрашивают:

«А
зачем мне это нужно?» Увы, простая
любознательность постепенно исчезает,
да и вечная погоня за карьерой, успехом,
просто за куском хлеба почти не оставляет
времени и сил на занятия, не приносящие
немедленной пользы. Поэтому – зачем?
Зачем мне читать эту книжку? Быть может,
следующие соображения покажутся вам
заслуживающими внимания.

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

Логика
воспитывает умение обосновывать свои
идеи и решения и убеждать других людей.
Если вы способны обосновать свою мысль,
решение того или иного вопроса, то ваша
речь будет не только ясной, но и
убедительной. Каким бы родом деятельности
вы ни занимались, часто это – необходимое
условие ее успеха.

Еще
более важно то, что знакомство с логикой
постепенно формирует привычку
анализировать свои и чужие рассуждения.
Логика вооружает нас и средствами,
позволяющими обнаружить, точно обозначить
и устранить ошибку рассуждения. Она
помогает нам справиться с демагогией
и софистикой, избавляет нас от того
земляного простодушия, которое легко
толкает нас в объятия сладкоречивых
жуликов. Обращаются, например, к вам с
таким рассуждением: «Я – человек, а вы
– не я, следовательно, вы – не человек».
И даже если вы чувствуете, что здесь
что-то не так, сможете ли вы достойно
возразить? Вряд ли. В лучшем случае
буркнете что-то вроде «Сам дурак!» и
отойдете с чувством интеллектуального
унижения. Знакомство с логикой даст вам
возможность определить, что это за
рассуждение, каким требованиям оно
должно удовлетворять и какое из этих
требований здесь нарушено. Указав на
все это, вы пристыдите демагога или
невежду, и уже он отойдет от вас, посыпав
голову пеплом.

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

И
все-таки самое важное – логика вырабатывает
привычку думать. Современная жизнь
вынуждает человека много знать, поэтому
системы школьного и высшего образования
построены таким образом, чтобы вложить
в голову учащегося как можно больше
информации. Но они, как правило, не учат
думать, не стремятся развить эту
драгоценную способность человека.
Поэтому многие не любят и не умеют
думать. Вместо того чтобы задуматься и
найти свое решение тех или иных проблем,
мы охотно полагаемся на мнение
какого-нибудь телевизионного вещателя,
друзей или знакомых. Конечно, думать
трудно, напряженное размышление забирает
столько сил, сколько тратит шахтер или
молотобоец. Но ведь думать необходимо,
если вы не хотите прожить всю свою жизнь
куклой, которую дергают за веревочки
ловкие манипуляторы. А когда думание
становится привычкой, оно начинает
доставлять наслаждение. Так атлет,
хрустя позвоночником, обливаясь потом,
со стонами развивает свои мышцы. Зато
потом, какой восторг доставляет ему
игра этих мышц, когда каждая клетка тела
поет о радости телесного бытия!

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

Соседние файлы в папке logika

Прогресс математики

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

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

Существует ли неизбежность такого пути развития абстракций? Подозреваю, что до некоторой степени, да. Возможно, так же обстоит дело и с другими типами формирования концепций. Достигнув некоего уровня, вы получаете возможность изучать различные вещи, а со временем группы этих вещей становятся примерами более общих и абстрактных конструкций – которые в свою очередь определяют новый уровень, отталкиваясь от которого, можно изучать что-то новое.

Есть ли способы вырваться из этого цикла? Одна из возможностей может быть связана с математическими экспериментами. Можно систематически доказывать вещи, связанные с определёнными математическими системами. Но можно и эмпирически просто замечать математические факты – как Рамануджан заметил однажды, что

очень близко к целому числу. Вопрос: являются ли такие вещи «случайными математическими фактами» или они как-то встраиваются в «ткань математики»?

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

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

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

Однако согласно моему принципу вычислительной эквивалентности и моему опыту в вычислительной вселенной, я почти уверен, что это не так – и что на самом деле неразрешимость очень близка даже в типичной математики. Я не удивлюсь, если ощутимая часть нерешённых на сегодня задач математики (гипотеза Римана, P = NP, и т.д.) окажутся неразрешимыми.

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

Конечно, экспериментальная математика или «случайные вопросы» могут сразу же привести нас в область, полную неразрешимости. Но, по крайней мере пока, основная дисциплина математики развивалась не так.

А что с этими «случайными фактами математики»? Да то же, что и с другими областями интеллектуальных исследований. «Случайные факты» не включаются в путь интеллектуального развития, пока какая-нибудь структура – обычно это некие абстрактные концепции – не будет построена вокруг них.

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

Ещё один пример – вложенные последовательности (фракталы). Есть отдельные примеры того, как они встречались в мозаике XIII века, но никто не обращал на них внимания, пока в 1980-х вокруг фракталов не возникла целая платформа.

Одна и та же история повторяется снова и снова: пока абстрактные концепции не определяться, сложно рассуждать о новых понятиях, даже когда сталкиваешься с явлением, демонстрирующим их.

Подозреваю, что так и в математике: есть определённое неизбежное наслоение одних абстрактных концепций поверх других, определяющее траекторию математики. Уникален ли этот путь? Несомненно, нет. В огромном пространстве возможных математических фактов существуют определённые направления, которые выбираются для дальнейших построений. Но можно было выбрать и другие.

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

Возможно, в какой-то степени это является следствием принципа вычислительной эквивалентности, и явления вычислительной универсальности: хотя базовые правила (или «язык»), использующиеся в разных областях математики, разнятся, в итоге появляется способ перевода между ними – и на следующем уровне абстракции выбранный путь уже не будет настолько критически важным.

Какие виды логического мышления бывают?

Мышление — процесс обработки полученной информации, которая поступает из внешнего мира. При получении любой информации человек способен представить ее в виде некого образа, представить предмет, когда его нет рядом.

Выделяют следующие основные виды логического мышления:

• Наглядно-действенное – в результате решения какой-либо задачи человек способен преобразить ее в своих мыслях, основываясь на ранее приобретенном опыте и знаниях. Поначалу человек наблюдает за ситуацией, затем путем проб и ошибок пытается решить проблему, после этого происходит формирование теоретической деятельности. Этот вид мышления предполагает равное применение теории и практики.
• Наглядно-образное – мышление происходит за счет представления. Оно наиболее характерно для детей дошкольного возраста. Для того чтобы решить какую-то задачу, дети часто пользуются образами, которые могут находиться в памяти или создаваться воображением. Также таким типом мышления обладают люди, которые связаны с таким родом деятельности, в котором необходимо принимать решения исходя из наблюдения за предметами или их изображениями (рисунок, схема).
• Абстрактно-логическое – данному виду мышления не важны отдельные детали, его интересует процесс размышления в целом. Чтобы не возникало проблем с решением важных задач в будущем, важно развивать абстрактно-логическое мышление еще с раннего детства. Этот вид мышления проявляется в трех основных формах: понятии, суждении, умозаключении.

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

Суждение может быть как простым, так и сложным. Это может быть утверждением какого-то предмета или отрицанием его взаимосвязи с другими предметами. Примером простого суждения служат простые фразы: «Маша любит кашу», «Мама любит Аню», «Кошка мяукает» и т.д. Именно так рассуждают малыши, когда начинают познавать окружающий мир.

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

Каждый человек может самостоятельно развивать логический тип мышления, решая специальные задачи, ребусы, кроссворды, головоломки.