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

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

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

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

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

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

   • П 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
       • R 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
   • R 3. Настройка режима 2.1

   • (( P →( Q → P ))→ R )→ R 4. вычет от 1 до 3 QED

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

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

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

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

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

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

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. Обратите внимание ,

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

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

$A\to A$

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

$(B\to C)\to ((A\to B)\to (A\to C))$

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

$(A\to (B\to C))\to (B\to (A\to C))$

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

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

$(A\to B)\to ((B\to C)\to (A\to C))$

$(A\to (A\to C))\to (A\to C)$

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

$((A\to B)\to A)\to A$

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

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

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

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

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

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

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

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

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

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

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

• Если T — теория и F , G — формулы с F замкнутой , и $T\cup \{F\}\vdash G$, затем $T\vdash F\rightarrow G$.

Здесь символ $\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 из $T\cup \{F\}$. В случае, когда при выводе менялась свободная переменная v из F, мы пишем $T\cup \{F\}\vdash ^{v}G$ (верхний индекс на турникете указывает на то, что v менялось) и соответствующая форма теоремы о выводе: $T\vdash (\forall vF)\rightarrow G$.

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

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

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

• Вопрос 1. гипотеза
  • Q → R 2. гипотеза
  • R 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. Настройка режима 1,2
• Q →(( Q → R )→ Q ) 4. аксиома 1
  • Вопрос 5. гипотеза
  • ( Q → R )→ Q 6. Настройка режима 5,4
  • ( Q → R )→ R 7. Настройка режима 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. Настройка режима 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. Настройка режима 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. Настройка режима 6,7
• Q →(( Q → R )→ R )) 9. Настройка режима 4.8 QED

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

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

См. также

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

Ссылки

• Карл Хьюитт (2008), «Организационные организации для масштабируемых, надежных и безопасных для конфиденциальности клиентских облачных вычислений», IEEE Internet Computing , 12 (5): 96–99, doi : 10.1109/MIC.2008.107 , S2CID   27828219 . Сентябрь/октябрь 2008 г.
• Коленбах, Ульрих (2008), Прикладная теория доказательств: интерпретации доказательств и их использование в математике , Монографии Springer по математике, Берлин, Нью-Йорк: 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.
• «Теорема о дедукции»