Логический вывод

Логический вывод — это рассуждение (см. Рассуждение), в ходе которого осуществляется переход от исходного суждения (высказывания или системы высказываний) с помощью логических правил к заключению — новому суждению (высказыванию или системе высказываний).

К логическому выводу обычно предъявляются (совместно или по отдельности) два основных требования:

1. Правила перехода должны воспроизводить отношение логического следования (ту или иную его разновидность);
2. Переходы в логическом выводе должны осуществляться на основе учёта только синтаксических характеристик высказываний или систем высказываний.

В современной логике понятие логического вывода определяется для формальных систем, в которых высказывания представлены формулами. Обычно выделяют три основных типа формальных систем: аксиоматические исчисления, исчисления натурального вывода, исчисления секвенций. Стандартное определение логического вывода (из множества формул Г) для аксиоматического исчисления S таково: логический вывод в S из множества формул Г есть такая последовательность Α₁… A_n формул языка исчисления S, что для каждой A_i (1 ≤ i ≤ n) выполняется, по крайней мере, одно из следующих трёх условий:

• A_i есть формула из Г;
• A_i есть аксиома исчисления S;
• A_i есть формула, получающаяся из предшествующей ей в последовательности A₁ … A_n формулы или из предшествующих ей в этой последовательности формул по одному из правил вывода исчисления S.

Если α есть логический вывод в S из множества формул Г, то формулы из Г называются посылками α, a сам вывод α называется выводом в S из посылок Г; если при этом A есть последняя формула α, то α называется логическим выводом в S формулы A из посылок Г. Запись «Г ⊦ _sA» означает, что существует логический вывод в S формулы A из посылок Г. Логический вывод в S из пустого множества формул называется доказательством в S. Запись «⊦ _s A» означает, что существует доказательство в S формулы A. Формула A называется доказуемой в S, если ⊦ A.

В качестве примера рассмотрим аксиоматическое исчисление S₁ со стандартным определением вывода, являющееся вариантом классической логики высказываний. Алфавит этого исчисления содержит только пропозициональные переменные p₁, p₂, … p_n, … логические связки ⊃, ⌉ и круглые скобки. Определение формулы в этом языке обычное. Аксиомы S₁ — это формулы следующих шести видов (и только эти формулы):

I. (A ⊃ A);
II. (A ⊃ B) ⊃ (B ⊃ C) ⊃ (A ⊃ C);
III. (A ⊃ (B ⊃ C) ⊃ (B ⊃ (A ⊃ C)));
IV. (A ⊃ (⌉B)) ⊃ (B ⊃ (⌉A)));
V. (⌉ (⌉A) ⊃ A);
VI. (A ⊃ B) ⊃ A) ⊃ A).

Единственное правило исчисления S₁ modus ponens: A ⊃ B ⊦ B.

Определение логического вывода для S₁ является очевидной конкретизацией определения, данного выше. Следующая последовательность формул Ф1 — Ф6 является логическим выводом в S₁ формулы (p₁ ⊃ p₂) ⊃ (p₂) из посылок (p₁).

Ф1. ((p₁ ⊃ p₂) ⊃ (p₁ ⊃ p₂),
Ф2. (((p₁ ⊃ p₂) ⊃ (p₁ ⊃ p₂) ⊃ (p₁ ⊃ (p₁ ⊃ p₂) ⊃ p₂),
Ф3. (p₁ ⊃ (p₁ ⊃ p₂) ⊃ p₂),
Ф4. p₁,
Ф5. (p₁ ⊃ p₂) ⊃ p₂).

Анализ: Ф1 есть аксиома вида I, Ф2 есть аксиома вида III, ФЗ получена по правилу modus ponens из Ф1 и Ф2, Ф4 есть посылка, Ф5 получена по правилу modus ponens из Ф4 и ФЗ. Итак, {p₁} ⊦ _s1 ((p₁ ⊃ p₂) ⊃ p₂). Рассмотрев последовательность формул Φ1, Φ2, Ф3, убеждаемся, что ⊦ _s1 (p₁ ⊃ p₂) ⊃ p₂).

В ряде случаев логический вывод определяется так, что на использование некоторых правил накладываются ограничения. Например, в аксиоматических исчислениях, являющихся вариантами классической логики предикатов первого порядка (см. Логика предикатов) и содержащих среди правил вывода только modus ponens и правило обобщения, логический вывод часто определяется так, что на использование правила обобщения накладывается ограничение: любое применение правилам обобщения в α таково, что переменная, по которой проводится обобщение в этом применении правила обобщения, не входит ни в одну посылку, предшествующую в α нижней формуле этого применения правила обобщения. Цель этого ограничения обеспечить ряд полезных с точки зрения логики свойств вывода (например, выполнение для простых форм теоремы дедукции).

Существуют определения логического вывода (как для аксиоматических, так и для исчислений других типов), которые:

• задают логический вывод не только из множества посылок, но допускают другие формы организации посылок (например, списки или последовательности);
• структурируют вывод не только линейно, но, например, в форме дерева;
• имеют явно выраженный индуктивный характер; при этом индуктивное определение вывода может вестись как по одной переменной (например, по длине вывода), так и по нескольким переменным (например, по длине логического вывода и по числу его посылок);
• содержат формализацию зависимости между формулами в логическом выводе, и многие другие определения логического вывода, обусловленные иными способами формализации и аксиоматизации классических и неклассических систем логики.