Теорема дедукции

Метатеорема в математической логике

В математической логике теорема о дедукции — это метатеорема , которая оправдывает выполнение условных доказательств из гипотезы в системах, которые явно не аксиоматизируют эту гипотезу, то есть, чтобы доказать импликацию A  →  B , достаточно предположить A в качестве гипотезы, а затем перейти к выводу B. Теоремы о дедукции существуют как для пропозициональной логики , так и для логики первого порядка . ^[1] Теорема о дедукции является важным инструментом в системах дедукции в стиле Гильберта, поскольку она позволяет писать более понятные и обычно гораздо более короткие доказательства, чем это было бы возможно без нее. В некоторых других системах формального доказательства такое же удобство обеспечивается явным правилом вывода; например, естественная дедукция называет его введением в импликацию .

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

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

Примеры вычета

1. «Докажите» аксиому 1: P →( Q → P ) ^[a]

   • П 1. гипотеза
     • Вопрос 2. гипотеза
     • П 3. повторение 1
   • Q → P 4. вычитание из 2 в 3

   • P →( Q → P ) 5. вычет из 1 в 4 QED
2. «Докажите» аксиому 2:

   • P →( Q → R ) 1. гипотеза
     • P → Q 2. гипотеза
       • П 3. гипотеза
       • Вопрос 4. модус поненс 3,2
       • Q → R 5. модус поненс 3,1
       • Р 6. модус поненс 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
3. Используя аксиому 1, покажем (( P →( Q → P ))→ R )→ R :

   • ( P →( Q → P ))→ R 1. гипотеза
   • P →( Q → P ) 2. аксиома 1
   • Р 3. модус поненс 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-му уровню и произнесением ^[b]

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

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

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

• гипотеза 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 (рефлексивность импликации), которая используется ниже:

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

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

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

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

При преобразовании modus ponens, если A находится вне области действия H , то необходимо применить аксиому 1, A →( H → A ), и modus ponens, чтобы получить 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. Обратите внимание, что комбинатор I соответствует схеме теоремы P → P.

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

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

${\displaystyle A\to A}$

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

${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

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

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

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

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

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle (A\to (A\to C))\to (A\to C)}$

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

${\displaystyle ((A\to B)\to A)\to A}$

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

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

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

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

Так как , существует доказательство из . Докажем теорему индукцией по длине доказательства n ; таким образом, гипотеза индукции состоит в том, что для любого и такого , что существует доказательство из длины до 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\to B}$

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

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

1. ${\displaystyle B}$является членом множества формул ; в этом случае действуем так же, как для n =1. ${\displaystyle \Delta \cup \{A\}}$
2. ${\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\to C}$ ${\displaystyle \Delta \vdash A\to (C\to B)}$ ${\displaystyle \Delta \vdash (A\to (C\to B))\to ((A\to C)\to (A\to B))}$ ${\displaystyle \Delta \vdash A\to B}$

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

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

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

• Если T — теория , а F , G — формулы, причем F замкнута , и , то . ${\displaystyle T\cup \{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 ( ЧАС → K ))→( ЧАС → ∀ vK ).

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

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

Пример преобразования

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

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

• Вопрос 1. гипотеза
  • Q → R 2. гипотеза
  • Р 3. модус поненс 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
  • Вопрос 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. si (ka)
• в-третьих, путем исключения лямбда-функции по a, f = s (k (si)) k

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

• Теорема об исключении разрезов
• Условное доказательство
• Каррирование
• Пропозициональное исчисление
• Закон Пирса

Примечания

1. См. пояснение к обозначению § ниже.
2. Гипотеза обозначена отступом, а заключение обозначено без отступа ^[5], как цитируется в ^[6]

1. Клини 1967, стр. 39, 112; Шенфилд 1967, стр. 33
2. Например, дедуктивные системы в стиле Гильберта , естественная дедукция , секвенциальное исчисление , метод таблиц и резолюция — см. Логика первого порядка.
3. Явную проверку этого результата можно найти по адресу https://github.com/georgydunaev/VerifiedMathFoundations/blob/master/SHEN.v
4. Коленбах 2008, стр. 148
5. Фредрик Б. Фитч (1952) Символическая логика: Введение
6. Питер Смит (13 октября 2010 г.) Типы систем доказательств, страницы 5 и последующие
7. Теорема дедукции, от Кертиса Фрэнкса из Университета Нотр-Дам, получено 21 июля 2020 г.
8. Клини, Стивен (1980). Введение в метаматематику . Северная Голландия. С. 102–106. ISBN 9780720421033.

Ссылки

• Карл Хьюитт (2008), «ORG для масштабируемых, надежных, конфиденциальных клиентских облачных вычислений», IEEE Internet Computing , 12 (5): 96–99, doi :10.1109/MIC.2008.107, S2CID  27828219.Сентябрь/октябрь 2008 г.
• Коленбах, Ульрих (2008), Прикладная теория доказательств: интерпретации доказательств и их использование в математике , Springer Monographs in Mathematics, Берлин, Нью-Йорк: Springer-Verlag , ISBN 978-3-540-77532-4, г-н  2445721
• Клини, Стивен Коул (2002) [1967], Математическая логика , Нью-Йорк: Dover Publications , ISBN 978-0-486-42533-7, МР  1950307
• Раутенберг, Вольфганг (2010), Краткое введение в математическую логику (3-е изд.), Нью-Йорк : Springer Science+Business Media , doi :10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6.
• Шоенфилд, Джозеф Р. (2001) [1967], Математическая логика (2-е изд.), AK Peters , ISBN 978-1-56881-135-2

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

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