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

Question

В Propositions as Types, написано:

В 1935 годе в возрасте 25 лет, Gentzen15 не введена один, а два новых формулировки логики естественных дедукций и секвенции исчисления, что утвердились как два основными системы для формулировки логики и остаются такими и по сей день. Он показал, как нормализовать доказательства, чтобы обеспечить они не были «обходной путь», давая новое доказательство согласованности Система Гильберта. И, в довершение всего, для соответствия использованию символа ∃ для экзистенциальной квантификации, введенной Пеано, Gentzen представил символ ∀ для обозначения универсальной количественной оценки. Он написал импликацию как A ⊃ B (если A держится, а затем B), соединение как A & B (как A и B hold), так и дизъюнкция как 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  

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

Нет причин для этого в оба конца: мы закончили с того места, где мы начали!

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

EDIT первая версия этого ответа было доказательство A ∧ B:

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

Но кроме прямого доказательства:

A ∧ B 

------- Id 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) 

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