Линейная Логика II: предыстория. Классическая логика

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

Готфрид Вильгельм Лейбниц

Если рассказывать предысторию линейной логики, то с какого периода начать? С Аристотеля? Или, быть может, с Лейбница? Или начать с Джона Буля и Готлоба Фреге? Бертрана Рассела и Альфреда Уайтхеда? Или с критики Брауэром программы Давида Гильберта? 

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

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

• "и": A ⋀ B — если верно A ⋀ B, то верны и A и B, и наоборот.
• "или": A ⋁ B — если верно A ⋁ B, то верно по крайней мере одно из высказываний A или B, и наоборот.
• "не":  ¬A — выполняется в том случае, когда A неверно.
• "следует": A → B — его можно определить как ¬A ⋁ B. В формальной логике считается, что из правды можно вывести любую правду, а из лжи — всё что угодно. Что оправдывает такое определение. Если выполняется A → B и B → A, то можно писать A ↔ B.

Этих связок хватает, чтобы строить самую простую логику — логику высказываний. Более сложной и интересной вещью является логика предикатов. Предикат — это логическая функция, высказывание о нефиксированном объекте.¹ Его можно понимать как недостроенное высказывание — если предоставить объект, оно превращается в обычное. (природу самого объекта мы пока вынесем за скобки). Другим способом превращения предиката в высказывание является применение кванторов всеобщности и существования:

• ∀x P(x) — для всех x выполняется свойство P
• ∃x P(x) — существует x для которого выполняется свойство P

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

∀x P(x) ≡ P(a) ⋀ P(b) ⋀ P(c) ⋀ ... 

∃x P(x) ≡ P(a) ⋁ P(b) ⋁ P(c) ⋁ ...

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

Что нам еще нужно, чтобы пользоваться классической логикой? Мы знаем как строить высказывания, но не знаем как строить доказательства этих высказываний. То есть, нам нужны правила, по которым из одних высказываний, можно получить другие высказывания — правила вывода. Кроме того, нам нужны аксиомы — правила построения верных высказываний.² Если мы указали аксиому, частный случай которой представляет наше высказывание, то мы его доказали, при том чисто синтаксически. Если мы пользуясь правилами вывода прошли от аксиом к нашему высказыванию, то мы его доказали, построив дерево вывода.

Весь список кораблей аксиом и правил вывода приводить не имеет большого смысла. Они естественным образом определяются знакомыми всем свойствами логических связок (от A ⋀ B можно перейти к A, от A можно перейти к A ⋁ B, и т.д.). Самым важным правилом вывода, наверное, следует считать modus ponens: из двух высказываний A и A → B можно вывести B. Вообще, линия между правилами вывода и аксиомами размыта — одно и то же свойство логической связки может быть в разных формализациях передано как аксиомой, так и правилом вывода, в принципе, при соответствующей формулировке аксиом из всех правил вывода можно оставить только modus ponens. Если же используются несколько правил вывода, то соответствующие аксиомы становятся теоремами.

Что для нас существенно, что среди аксиом классической логики есть закон исключенного третьего A ⋁ ¬A. Или равносильный ему закон двойного отрицания ¬¬A  → A. Они делают возможным построение доказательств от противного. Они также есть причиной замечательных тождеств де Моргана:

¬ ( A ⋁ B ) ↔ ¬A ⋀ ¬B

¬ ( A ⋀ B ) ↔ ¬A ⋁ ¬B

делающих классическую логику столь симметричной. Схожей природы правило отрицания для кванторов:

¬ ∃x P(x) ↔ ∀x ¬ P(x)

¬ ∀x P(x) ↔ ∃x ¬ P(x)

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

---

¹ Предикат конечно может зависеть от нескольких переменных, так что изложение здесь нестрогое
² Строго говоря, аксиома — это конкретное высказывание, полагаемое верным, правила построения верных высказываний называются схемами аксиом