Теория 1. Понятие логического вывода

ВЫВОД ЛОГИЧЕСКИЙ — рассуждение, в котором осуществляется переход по правилам от высказывания или системы высказываний к высказыванию или системе высказываний. К логическому выводу обычно предъявляются (совместно или по отдельности) следующие требования: 1) правила перехода должны воспроизводить отношение следования логического (ту или иную его разновидность); 2) переходы в логическом выводе должны осуществляться на основе учета только синтаксических характеристик высказываний или систем высказываний.

Определение правила логического следования:

Фигура A1, A2, A3, …, An/C называется корректной фигурой, или правилом следования , если формула вида A1->(A2-> … (An -> C)…) есть логическое тождество.

2. Система естественного вывода в логике высказываний

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

Впервые были изобретены независимо друг от друга польским логиком С. Яськовским и немецким логиком Г. Генценом в 30х годах 20го столетия.

3. Основные и производные правила в логических системах

Основные правила.

1. Модус Поненс: А, А->B/ B

2. Правило Введения Конъюнкции: А, В/ А^B

3. Правило Удаления Конъюнкции: А ^B/ A; A^B/ В

4. Правило Введения Дизъюнкции: А/ А˅В; В/ А˅В

5. Правило Удаления Дизъюнкции: А˅В, А->C; B->C/ C

Производные правила.

Правило называется производным в логической системе, если добавление к ней данного правила даёт равнообъёмную ей систему. Другими словами, применение производных правил не увеличивает класса формул, доказуемых в соответствующей логической системе.

1. Модус Толленс: А->B, ~B/ ~A; А->~B, B/ ~A

2. Удаление Отрицания Конъюнкции: ~ (A^B), A, / ~B; ~ (A^B), B/ ~A

3. Удаление Дюзъюнкции посредством Отрицания: А˅В, ~A/ B; А˅В, ~B/ A; ~А˅В, А/ В, А˅~В, В/ А

4. Введение Эквиволентности: A->B; B->A/ A <-> B;

5. Удаление Эквиволентности: A <-> B/ A->B; A <-> B/ B->A

6. Правило Удаления Отрицания (Т. 34): A, ~A/ B

4. Чистое прямое доказательство

[II. 1]Прямое доказательство формулы (кратной импликации) вида

A1 -> (A2 -> … (An -> C)…) (*)

строится согласно следующему предписанию:

На любом шаге построения можно написать:

1. Одну из формул А1, А2, …, An в качестве допущения:

2. Формулу, следующую из ранее написанных формул по одному из правил логического следования;

3. Ранее доказанную формулу

Прямое доказательство формулы (*) считается построенным, если в соответствии с пп. 1)-3) получена последовательность формул, оканчивающаяся формулой С.

Чисто прямое доказательство – это такое доказательство, которое не имеет косвенных доказательств в качестве предшедствующих (необязательно непосредственно).

5. Положительная логика как фрагмент естественного вывода

Фрагмент системы N, определяемый правилами [I], логического следования и правилом [II. 1], построения прямого доказательства представляет собой один из вариантов исчисления положительной (или позитивной), логики. В данной теории изучаются логические законы и правила, не содержащие знака отрицания. С помощью этих законов и правил строются чисто прямые доказательства. Поэтому положительную логику можно было также назвать логикой чисто прямого доказательства. 6. Правило построения доказательства по частям

Правило доказательства по частям (ДЧ) формулируется так: для того чтобы доказать формулу А1 -> (A2 -> … (An -> (C1^C2))…) (*)

достаточно построить

1. доказательство формулы

А1 -> (A2 -> … (An -> C1)…) (**)

(часть 1) и

2. доказательство формулы

А1 -> (A2 -> … (An -> C2)…) (***)

(часть 2)

7. Правило построения доказательства посредством разбора случаев

Правило Разбора Случаев (РС) формулируется следующим образом: для того чтобы доказать формулу вида

A1 -> ( A2 -> … ( An -> (( B1 ˅B2) -> C)) … ), (*)

Достаточно построить

1. доказательство формулы

A1 -> ( A2 -> … ( An -> (( B1 -> C)) … ), (**)

(случай 1) и

2. доказательство формулы

A1 -> ( A2 -> … ( An -> ((B2-> C)) … ), (***)

(случай 2).

8. Слабое косвенное доказательство

Слабое косвенное доказательство формулы

A1 -> (A2 -> … (An -> C) … ) (*)

строится согласно следующему предписанию.

На любом шаге построения можно написать:

1. одну из формул A1, A2, …, An в качестве допущения.

1а) формулу С’, полученную из С стиранием первого слева знака отрицания, в качестве допущения слабого косвенного доказательства.

2. формулу, следующую из ранее написанных формул, по одному из правил логического следования.

3. Ранее доказанную формулу.

Слабое косвенное доказательство формулы (*) считается построенным, если в соответствии с пп. 1)-3), включая и п. 1а), получена последовательность формул, содержащая формулу С’, пару противоречащих формул и оканчивающаяся одной из формул данной пары.

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

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

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

9. Исчисление минимальной логики как фрагмент естественного вывода

Логическая система, имеющая такие правила, как (1) правила логического следования, (2) правило построения прямого доказательства, (3) правило построения слабого косвенного доказательства, представляет собой одно из логических исчислений так называемой минимальной логики.

Если в полной системе N, вообще говоря, можно было бы обойтись без правила построения прямого доказательства, то в описанной логической системе минимальной логики правило (3) не делает избыточным применение (2) потому, что ни одна кратная импликация, консеквент которой не начинается со знака отрицания, не может быть доказана с помощью правила (3).