Теорема дедукции - Deduction theorem

В математической логике , вычет теорема является метатеорема , что обосновывает делать условные доказательства - доказать импликацию → B , предположим , что A в качестве гипотезы , а затем перейти к Dérivé B - в системах , которые не имеют явного правила логического вывода для этого. Теоремы дедукции существуют как для логики высказываний, так и для логики первого порядка . Теорема дедукции - важный инструмент в системах дедукции гильбертова, поскольку она позволяет писать более понятные и, как правило, гораздо более короткие доказательства, чем это было бы возможно без нее. В некоторых других формальных системах доказательства такое же удобство обеспечивается правилом явного вывода; например, естественная дедукция называет это введением импликации .

Более подробно, теорема вывода логики высказываний утверждает, что если формула выводима из набора предположений, то импликация выводима из ; в символах подразумевает . В частном случае, когда - пустое множество , утверждение теоремы дедукции может быть более компактно записано как: подразумевает . Теорема вывода для логики предикатов аналогична, но имеет некоторые дополнительные ограничения (которые, например, были бы выполнены, если это закрытая формула ). В общем, теорема дедукции должна учитывать все логические детали рассматриваемой теории, поэтому каждой логической системе технически нужна собственная теорема дедукции, хотя различия обычно незначительны. ${\ displaystyle B}$ ${\ displaystyle \ Delta \ cup \ {A \}}$ ${\ displaystyle от A \ до B}$ ${\ displaystyle \ Delta}$ ${\ displaystyle \ Delta \ cup \ {A \} \ vdash B}$ ${\ displaystyle \ Delta \ vdash от A \ до B}$ ${\ displaystyle \ Delta}$ ${\ displaystyle A \ vdash B}$ ${\ displaystyle \ vdash от A \ до B}$ ${\ displaystyle A}$

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

Примеры дедукции

«Докажите» аксиому 1:
- P 1. гипотеза
- Q 2. гипотеза
  - П 3. повторение 1
- Q → P 4. сбавка от 2 до 3
P → ( Q → P ) 5. удержание от 1 до 4 QED
«Докажите» аксиому 2:
- P → ( Q → R ) 1. гипотеза
  - P → Q 2. гипотеза
    
    П 3. Гипотеза
    
    Q 4. modus ponens 3,2
    
    Q → R 5. modus ponens 3,1
    
    R 6. modus ponens 4,5
  - P → R 7. сбавка от 3 до 6
- ( P → Q ) → ( P → R ) 8. сбавка от 2 до 7
( P → ( Q → R )) → (( P → Q ) → ( P → R )) 9. удержание от 1 до 8 QED
Используя аксиому 1, чтобы показать (( P → ( Q → P )) → R ) → R :
- ( P → ( Q → P )) → R 1. гипотеза
- P → ( Q → P ) 2. аксиома 1
- R 3. modus ponens 2,1
(( P → ( Q → P )) → R ) → R 4. удержание от 1 до 3 QED

Виртуальные правила вывода

Из примеров вы можете видеть, что мы добавили три виртуальных (или дополнительных и временных) правила вывода к нашей обычной аксиоматической логике. Это «гипотеза», «повторение» и «дедукция». Обычные правила вывода (т.е. «modus ponens» и различные аксиомы) остаются доступными.

1. Гипотеза - это шаг, на котором к уже имеющимся предположениям добавляются дополнительные. Итак, если ваш предыдущий шаг S был выведен как:

{\ displaystyle E_ {1}, E_ {2}, ..., E_ {n-1}, E_ {n} \ vdash S,}

затем добавляется еще одна посылка H и получается:

{\ displaystyle E_ {1}, E_ {2}, ..., E_ {n-1}, E_ {n}, H \ vdash H.}

Это символизируется переходом с n-го уровня отступа на n + 1-й уровень и высказыванием

S предыдущий шаг
- H гипотеза

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

3. Дедукция - это шаг, на котором удаляется самая последняя гипотеза (еще доступная) и добавляется к предыдущему шагу. Это показано удалением одного уровня следующим образом:

H гипотеза
......... (другие шаги)
C (вывод из H )

H → C вычет

Переход от доказательства с использованием мета-теоремы дедукции к аксиоматическому доказательству

В аксиоматических версиях логики высказываний обычно есть среди схем аксиом (где P , Q и R заменены любыми пропозициями):

Аксиома 1: P → ( Q → P )
Аксиома 2: ( P → ( Q → R )) → (( P → Q ) → ( P → R ))
Modus ponens: из P и P → Q вывести Q

Эти схемы аксиом выбраны так, чтобы можно было легко вывести из них теорему дедукции. Может показаться, что мы задаемся вопросом. Однако их можно оправдать, проверив, что они являются тавтологиями, используя таблицы истинности, и что modus ponens сохраняет истину.

Из этих схем аксиом можно быстро вывести схему теорем P → P (рефлексивность импликации), которая используется ниже:

( P → (( Q → P ) → P )) → (( P → ( Q → P )) → ( P → P )) из схемы аксиом 2 с P , ( Q → P ), P
P → (( Q → P ) → P ) из схемы аксиом 1 с P , ( Q → P )
( P → ( Q → P )) → ( P → P ) из modus ponens, примененного к шагу 2 и шагу 1
P → ( Q → P ) из схемы аксиом 1 с P , Q
P → P из modus ponens, примененного к шагу 4 и шагу 3

Предположим , что мы имеем , что Γ и H доказать C , и мы хотим показать , что Γ оказывается H → C . Для каждого шага S в дедукции , которая является предпосылкой в Г (шаг) или повторение аксиомы, мы можем применить модус поненс к аксиоме 1, S → ( H → S ), чтобы получить H → S . Если шаг H сам (шаг гипотезы), мы применяем схему теоремы , чтобы получить H → H . Если шаг является результатом применения modus ponens к A и A → S , мы сначала убеждаемся, что они были преобразованы в H → A и H → ( A → S ), а затем берем аксиому 2, ( H → ( → S )) → (( H → ) → ( H → S )), и применить модус поненс получить ( H → ) → ( H → S ) , а затем снова , чтобы получить H → S . В конце доказательства мы будем иметь H → C , как требуется, за исключением того, что теперь это зависит только от Г, а не на H . Таким образом, шаг вычет исчезнет, консолидируются в предыдущем шаге , который был вывод , полученный из H .

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

Во время преобразования может быть полезно применить все применения modus ponens к аксиоме 1 в начале вывода (сразу после шага H → H ).

При преобразовании модус поненс, если находится вне сферы H , то это будет необходимо применить аксиому 1, → ( Н → ) и модус поненс , чтобы получить H → A . Аналогично, если A → S выходит за рамки H , примените аксиому 1, ( A → S ) → ( H → ( A → S )) и modus ponens, чтобы получить H → ( A → S ). Нет необходимости делать оба из них, если только шаг modus ponens не является заключением, потому что, если оба выходят за рамки, тогда modus ponens должен был быть перемещен вверх перед H и, таким образом, также выходил за рамки.

При соответствии Карри – Ховарда описанный выше процесс преобразования для мета-теоремы вывода аналогичен процессу преобразования из терминов лямбда-исчисления в термины комбинаторной логики , где аксиома 1 соответствует комбинатору K, а аксиома 2 соответствует комбинатору S . Обратите внимание , что я Combinator соответствует теореме схеме P → P .

Полезные теоремы

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

{\ Displaystyle от А \ до А}

помогает преобразовать шаги гипотезы.

{\ Displaystyle (В \ к С) \ к ((от А \ к В) \ к (от А \ к С))}

помогает преобразовать modus ponens, когда основная посылка не зависит от гипотезы, заменяет аксиому 2, избегая использования аксиомы 1.

{\ Displaystyle (А \ К (В \ К С)) \ К (В \ К (А \ К С))}

помогает преобразовать modus ponens, когда второстепенная посылка не зависит от гипотезы, заменяет аксиому 2, избегая использования аксиомы 1.

Эти две теоремы вместе можно использовать вместо аксиомы 2, хотя преобразованное доказательство будет более сложным:

{\ Displaystyle (от А \ к В) \ к ((В \ к С) \ к (от А \ к С))}

{\ Displaystyle (А \ К (А \ К С)) \ К (А \ К С)}

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

{\ Displaystyle ((от А \ к В) \ к А) \ к А}

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

Доказательство теоремы дедукции

Мы доказываем теорему дедукции в дедуктивной системе исчисления высказываний в стиле Гильберта.

Позвольте быть набор формул и формул, такой что . Мы хотим это доказать . ${\ displaystyle \ Delta}$ ${\ displaystyle A}$ ${\ displaystyle B}$ ${\ displaystyle \ Delta \ cup \ {A \} \ vdash B}$ ${\ displaystyle \ Delta \ vdash от A \ до B}$

Поскольку есть доказательство от . Докажем теорему индукцией по доказательству длины n ; Таким образом , предположение индукции , что для любого , и таким образом, что существует доказательство от длины до п , имеет место. ${\ displaystyle \ Delta \ cup \ {A \} \ vdash B}$ ${\ displaystyle B}$ ${\ displaystyle \ Delta \ cup \ {A \}}$ ${\ displaystyle \ Delta}$ ${\ displaystyle A}$ ${\ displaystyle B}$ ${\ displaystyle B}$ ${\ displaystyle \ Delta \ cup \ {A \}}$ ${\ displaystyle \ Delta \ vdash от A \ до B}$

Если n = 1, то входит в набор формул . Таким образом, либо , в этом случае, это просто то, что выводится заменой из p → p, что выводится из аксиом, следовательно, также ; или находится в , и в этом случае ; из аксиомы p → (q → p) с заменой следует, что, а значит, по модусу ponens, что . ${\ displaystyle B}$ ${\ displaystyle \ Delta \ cup \ {A \}}$ ${\ displaystyle B = A}$ ${\ displaystyle от A \ до B}$ ${\ Displaystyle от А \ до А}$ ${\ displaystyle \ Delta \ vdash от A \ до B}$ ${\ displaystyle B}$ ${\ displaystyle \ Delta}$ ${\ displaystyle \ Delta \ vdash B}$ ${\ Displaystyle \ Delta \ vdash B \ to (A \ to B)}$ ${\ displaystyle \ Delta \ vdash от A \ до B}$

Теперь предположим предположение индукции для доказательств длины до n , и пусть будет формула, выводимая из с доказательством длины n +1. Тогда есть три возможности: ${\ displaystyle B}$ ${\ displaystyle \ Delta \ cup \ {A \}}$

${\ displaystyle B}$ входит в набор формул ; в этом случае поступаем так же, как при n = 0. ${\ displaystyle \ Delta \ cup \ {A \}}$
${\ displaystyle B}$ получается подстановкой в формуле φ. Тогда φ доказывается с помощью не более чем n шагов, следовательно, по предположению индукции , где мы можем писать A и φ с разными переменными. Но тогда мы можем прийти из в одной и той же подстановки , который используется для получения из ф; таким образом . ${\ displaystyle \ Delta \ cup \ {A \}}$ ${\ displaystyle \ Delta \ vdash A \ to \ varphi}$ ${\ displaystyle A \ to \ varphi}$ ${\ displaystyle от A \ до B}$ ${\ displaystyle B}$ ${\ displaystyle \ Delta \ vdash от A \ до B}$
${\ displaystyle B}$ достигается с помощью modus ponens. Тогда существует такая формула C , которая доказывает и , и тогда для доказательства используется modus ponens . Доказательства и состоят не более чем из n шагов, и по предположению индукции мы имеем и . По аксиоме (p → (q → r)) → ((p → q) → (p → r)) с заменой следует, что , а с помощью двойного использования modus ponens имеем . ${\ displaystyle \ Delta \ cup \ {A \}}$ ${\ displaystyle C}$ ${\ displaystyle C \ to B}$ ${\ displaystyle B}$ ${\ displaystyle C}$ ${\ displaystyle C \ to B}$ ${\ displaystyle \ Delta \ vdash от A \ до C}$ ${\ Displaystyle \ Delta \ vdash A \ to (C \ to B)}$ ${\ Displaystyle \ Дельта \ vdash (А \ К (С \ К В)) \ К ((А \ К С) \ К (А \ К Б))}$ ${\ displaystyle \ Delta \ vdash от A \ до B}$

Таким образом, во всех случаях теорема верна и для n +1, и по индукции теорема вывода доказана.

Теорема дедукции в логике предикатов

Теорема дедукции также верна в логике первого порядка в следующей форме:

Если T - теория, а F , G - формулы с замкнутым F , и , то . ${\ Displaystyle Т \ чашка \ {F \} \ vdash G}$ ${\ displaystyle T \ vdash F \ rightarrow G}$

Здесь символ означает «является синтаксическим следствием». Ниже мы укажем, чем доказательство этой теоремы дедукции отличается от доказательства теоремы дедукции в исчислении высказываний. ${\ displaystyle \ vdash}$

В наиболее распространенных версиях понятия формального доказательства, помимо схем аксиом исчисления высказываний (или понимания того, что все тавтологии исчисления высказываний следует рассматривать как самостоятельные схемы аксиом ), есть кванторные аксиомы , и в дополнение к modus ponens , еще одно правило вывода , известное как правило обобщения : «Из K вывести ∀ vK ».

Чтобы преобразовать доказательство G из T ∪ { F } в одно из F → G из T , нужно выполнить шаги доказательства G, которые являются аксиомами или являются результатом применения modus ponens таким же образом, как и для доказательств в логика высказываний. Шаги, которые являются результатом применения правила обобщения, рассматриваются с помощью следующей аксиомы квантора (действительной, если переменная v не свободна в формуле H ):

(∀ v ( H → K )) → ( H → ∀ vK ).

Так как в нашем случае F предполагается закрыть, мы можем взять H быть F . Эта аксиома позволяет вывести F → ∀ Vk из F → K и обобщения, что именно то , что требуется , когда правило обобщения применяется к некоторому K в доказательстве G .

В логике первого порядка ограничение на то, что F является замкнутой формулой, может быть ослаблено при условии, что свободные переменные в F не изменились при выводе G из . В случае, если свободная переменная v в F изменялась при дедукции, мы пишем (верхний индекс в турникете, указывающий, что v было изменено), и соответствующая форма теоремы дедукции имеет вид . ${\ Displaystyle Т \ чашка \ {F \}}$ ${\ Displaystyle Т \ чашка \ {F \} \ vdash ^ {v} G}$ ${\ Displaystyle Т \ vdash (\ forall vF) \ rightarrow G}$

Пример конвертации

Чтобы проиллюстрировать, как можно преобразовать естественный вывод в аксиоматическую форму доказательства, мы применим его к тавтологии Q → (( Q → R ) → R ). На практике обычно достаточно знать, что мы можем это сделать. Обычно мы используем естественно-дедуктивную форму вместо более длинного аксиоматического доказательства.

Сначала мы пишем доказательство, используя метод естественного вывода:

Q 1. гипотеза
- Q → R 2. гипотеза
- R 3. modus ponens 1,2
( Q → R ) → R 4. сбавка от 2 до 3

Q → (( Q → R ) → R ) 5. удержание от 1 до 4 QED

Во-вторых, мы преобразуем внутренний вывод в аксиоматическое доказательство:

( Q → R ) → ( Q → R ) 1. схема теорем ( A → A )
(( Q → R ) → ( Q → R )) → ((( Q → R ) → Q ) → (( Q → R ) → R )) 2. аксиома 2
(( Q → R ) → Q ) → (( Q → R ) → R ) 3. modus ponens 1,2
Q → (( Q → R ) → Q ) 4. аксиома 1
- Q 5. гипотеза
- ( Q → R ) → Q 6. modus ponens 5,4
- ( Q → R ) → R 7. modus ponens 6,3
Q → (( Q → R ) → R ) 8. удержание от 5 до 7 QED

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

( Q → R ) → ( Q → R ) 1. схема теорем ( A → A )
(( Q → R ) → ( Q → R )) → ((( Q → R ) → Q ) → (( Q → R ) → R )) 2. аксиома 2
(( Q → R ) → Q ) → (( Q → R ) → R ) 3. modus ponens 1,2
Q → (( Q → R ) → Q ) 4. аксиома 1
[(( Q → R ) → Q ) → (( Q → R ) → R )] → [ Q → (((( Q → R ) → Q ) → (( Q → R ) → R ))] 5. аксиома 1
Q → ((( Q → R ) → Q ) → (( Q → R ) → R )) 6. modus ponens 3,5
[ Q → ((( Q → R ) → Q ) → (( Q → R ) → R ))] → ([ Q → (( Q → R ) → Q )] → [ Q → (( Q → R ) → R ))]) 7. аксиома 2
[ Q → (( Q → R ) → Q )] → [ Q → (( Q → R ) → R ))] 8. modus ponens 6,7
Q → (( Q → R ) → R )) 9. modus ponens 4,8 QED

Эти три шага можно кратко сформулировать, используя соответствие Карри – Ховарда :

Во-первых, в лямбда-исчислении функция f = λa. λb. ba имеет тип q → ( q → r ) → r
во-вторых, методом исключения лямбда на b, f = λa. си (ка)
в-третьих, методом исключения лямбда на a, f = s (k (si)) k

Смотрите также

Заметки

Перейти ↑ Kleene 1967, p. 39, 112; Шенфилд 1967, стр. 33
^ Например, дедуктивные системы в стиле Гильберта , естественная дедукция , секвенциальное исчисление , метод таблиц и разрешение - см. Логику первого порядка.
^ Явную проверку этого результата можно найти в https://github.com/georgydunaev/VerifiedMathFoundations/blob/master/SHEN.v
^ Kohlenbach 2008, стр. 148
^ Теорема дедукции, от Кертиса Фрэнкса из Университета Нотр-Дам , получено 21 июля 2020 г.
Перейти ↑ Kleene, Stephen (1980). Введение в метаматематику . Северная Голландия. С. 102–106. ISBN 9780720421033.

Внешние ссылки

Введение в математическую логику Вилниса Детловса и Карлиса Подниекса Подниекса представляет собой исчерпывающее учебное пособие. См. Раздел 1.5.
«Теорема дедукции»

[1] Перейти ↑ Kleene 1967, p. 39, 112; Шенфилд 1967, стр. 33

[2] Например, дедуктивные системы в стиле Гильберта , естественная дедукция , секвенциальное исчисление , метод таблиц и разрешение - см. Логику первого порядка.

[3] Явную проверку этого результата можно найти в https://github.com/georgydunaev/VerifiedMathFoundations/blob/master/SHEN.v

[4] Kohlenbach 2008, стр. 148

[5] Теорема дедукции, от Кертиса Фрэнкса из Университета Нотр-Дам , получено 21 июля 2020 г.

[6] Перейти ↑ Kleene, Stephen (1980). Введение в метаматематику . Северная Голландия. С. 102–106. ISBN 9780720421033.

Languages

In other projects