Как доказательства логики вписываются в логическую структуру?

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

Доказательства — это наборы утверждений в системе, а утверждения о доказательствах не являются утверждениями в системе — это утверждения на естественном языке (например, английском). Поэтому высказывания на английском языке об высказываниях в системе не связаны правилами системы и не живут внутри системы. Однако точно так же, как можно сказать, является ли $2+2=4$ правильным или неправильным в контексте арифметики, не используя арифметику, можно определить, действительно ли доказательство в системе, не используя для этого систему. Это потому, что любой беспристрастный наблюдатель может проверить свод правил, чтобы убедиться, что правила соблюдались правильно.

Вот в чем загвоздка: разумно думать, что логика системы — это также логика, которую мы используем для анализа утверждений о системе, но это просто не так. Когда мы анализируем систему, мы просто проверяем свод правил, и выводы, которые мы делаем, объективно верны или ложны. Хотя другая система с другим сводом правил может привести к другому выводу.

Тем не менее, я сочувствую (чему я верю) вашему беспокойству, а именно. «Мы используем логику для анализа логики, так что, разве это не циклично? Как мы можем использовать логику, пока не узнаем, как она работает?» Ответ заключается в том, что естественная интуиционистская логика не обязательно опирается на формальную систему, поскольку ее истинность самоочевидна. Позвольте мне сказать так: почему вы верите в арифметику? Это потому, что вы изучили правила, и они кажутся внутренне непротиворечивыми, или потому, что их выводы совершенно очевидны? 2 яблока и 3 яблока — это 5 яблок, следовательно, $2+3=5$. Не попадайтесь в ловушку, ставя телегу впереди лошади. Система моделирует реальность, а не наоборот. Модель несовершенна, но мы используем систему, потому что модель соответствует нашим интуитивным представлениям.

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

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

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

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

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