Что такое "окольное доказательство" в "Предложениях как типы" П. Вадлера?

Question

В предложениях как типы написано:

В 1935 году, в возрасте 25 лет, Генцен15 ввел не одну, а две новые формулировки логики - естественное дедукция и последовательное исчисление - которые утвердились как две основные системы для формулировки логики и остаются таковыми по сей день. Он показал, как нормализовать доказательства, чтобы они не были "окольными", что дало новое доказательство непротиворечивости системы Гильберта. И, в довершение всего, чтобы соответствовать использованию символа ∃ для экзистенциального количественного определения, введенного Пеано, Генцен ввел символ ∀ для обозначения универсального количественного определения. Он записал импликацию как A ⊃ B (если A выполнено, тогда B выполнено), конъюнкцию как A & B (как A и B удерживают), так и дизъюнкцию как A ∨ B (хотя бы один из A или B имеет место).

Что является окольным доказательством? Не могли бы вы привести простой пример? Почему это проблема?

Answer 1

Давайте возьмем соединение, например: A ∧ B,

Если мы знаем A а также Bмы можем вывести A ∧ B:

 A   B
------- I
 A ∧ B

Это известно как правило введения.

Вдвойне, если мы знаем A ∧ B мы можем вывести A, или же B:

 A ∧ B          A ∧ B
------- E1     ------- E2
   A              B

Это правила исключения.

Тогда, если мы знаем A мы можем доказать A как первый вывод A ∧ A используя правило введения, а затем разрушить его в A (и другой A) используя правило исключения:

 A   A
------- I
 A ∧ A
-------- E1
   A     

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

Нет причин делать это туда и обратно: мы закончили, где мы начали!

Секвенциальное исчисление "запрещает" введение правил после исключения правил. Результат Гентзена говорит, что логика с этим свойством так же сильна, как логика, в которой разрешены правила исключения после правил введения. В настоящее время это важно, так как пространство доказательств намного меньше: сначала мы исключаем (составляем так мало формул, сколько можем / нуждаемся), затем вводим (для построения цели). Это практически полезно, например, для автоматического поиска корректуры или синтеза программы.

РЕДАКТИРОВАТЬ первую версию этого ответа было доказательство A ∧ B:

 A ∧ B         A ∧ B
------- E1    ------- E2
   A             B
  ----------------- I
         A ∧ B

И все же, кроме прямых доказательств:

A ∧ B

------- I A A B

кажется, это единственное другое "простое доказательство". В синтаксисе Haskell можно написать:

proof :: (a, b) -> (a, b)
proof (x, y) = (x, y)
-- or
proof x = x
proof = id

Которые являются (кроме свойств строгости, которых не интересует логика) одинаковыми и единственно разумными определениями. Например:

proof :: (a, b) -> (a, b)
proof x = fst (x, x)

Действителен также, больше не умен.