4.1.2.3. Метод дедуктивного вывода

Выводом формулы В из множества формул F₁; F₂; . . . F_n называется такая последовательность формул, что любая F_i есть либо аксиома, либо выводима из множества предшествующих ей формул F₁; F₂; . . . F_n.

В этом случае формулу B называют заключением, а последовательность формул F₁; F₂; . . . F_n, сформированная отношением следования, представляет схему дедуктивного вывода.

Схему дедуктивного вывода записывают так:

F₁; F₂; . . . F_n  B,

где символ “ “ означает “верно, что B выводима из F₁; ... F_n“.

Известна другая форма записи схемы:

F ₁; F₂; . . . F_n

B,

где над чертой записывают множество посылок и аксиом F₁; F₂;...F_n, а под чертой - заключение В.

На языке математики схема дедуктивного вывода есть доказательство теоремы:

 F₁F₂. . . F_nB.

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

1) (F₁F₂...F_nB);

2) ((F₁F₂...F_n )B);

3) (F₁F₂ ...F_nB);

4) (F₁F₂ ...F_n-1(F_nB));

.....................................................

n) (F₁(F₂ ...(F_n-1(F_nB))...).

Таким образом, вывод заключения всегда логически следует из множества посылок и аксиом. Кроме того, вывод заключения опирается на два основных правила:

а ) если F_i и (F_i  F_j ) выводимые формулы, то F_j также выводимая формула:

F_i; (F_iF_j)

F_j.

Это правило называют modus ponens (m.p.) или способ прямого доказательства.

b) если F_j и (F_iF_j) выводимые формулы, то F_i также выводимая формула:

(F_iF_j)

F_i.

Это правило называют modus tollens (m.t.) или способ обратного доказательства.

Пример: суждение: “Сумма внутренних углов многоугольника равна 180^о (А). Если сумма внутренних углов многоугольника равна 180^о (A), то многоугольник есть треугольник (В). Следовательно, дан треугольник (В)”.

Формула этого суждения (m.p.) имеет вид:

А; AB

B.

Пример: суждение: ”Дан не треугольник (B). Если сумма внутренних углов многоугольника равна 180^о (А), то многоугольник есть треугольник (В). Следовательно, сумма внутренних углов многоугольника не равна 180^о(A)”.

Формула этого суждения (m.t.) имеет вид:

B; AB

A.

Пример. доказать истинность заключения:

(AB); (AC); (BD)

(CD).

• F₁=(AC) - посылка;

• F₂=(AB)(CB) - заключение по F₁ и или правилу П6;

• F₃=(BD) - посылка;

• F₄=(CB)(CD) - заключение по F₃ и правилу П6;

• F₅=(AB)(CD) заключение по F₂ и F₄ и правилуП8;

• F₆=(AВ) - посылка;

• F₇=(CD) - заключение по F₅ и F₆ и правилу m. p..

Так доказана истинность (CD).

Процесс дедуктивного вывода удобно проследить на графе, вершинами которого являются формулы, а дугами – отношения

Пример: доказать истинность заключения:

(AB)(CD); ( DBE );  E

C A.

Ниже показан процесс дедуктивного вывода заключения.

• F₁=(DBE) - посылка;

• F₂=E - посылка;

• F₃=(DB) - заключение по F₁ и F₂ и правилу m. t.;

• F₄=(АВ)(СD) - посылка;

• F₅=(AВ) - заключение по F₄ и правилу П2;

• F₆=(СD) - заключение по F₄ и правилу П2;

• F₇=(BA) - заключение по F₅ и правилу П2;

• F₈=(DB) - заключение по F₃ и закону де Моргана;

• F₉=(DB) - заключение по F₈;

• F₁₀=(D A) - заключение по F₇ и F₉ и правилу П8;

• F₁₁=(С A) - заключение по F₆ и F₁₀ и правилу П8;

• F₁₂=(С A) - заключение по F_II .

Пример: доказать истинность заключения:

((A  B) С); (С(D  M )); (MN); (( D)( N))

 A.

• F₁=(( D)( N)) - посылка;

• F₂=N - заключение по F₁ и правилу П2;

• F₃=(MN) - посылка;

• M - заключение по F₂ и F₃ и правилу m.t;

• F₅=D - заключение по F₁ и правилу П2;

• F₆=(D)(M) - заключение по F₄ и F₅ и правилу П1;

• F₇=(DМ) – заключение по F₆; заключение по формуле F₆ и закону де Моргана;

• F₈=(( AB)C) - посылка;

• F₉=(С (DМ)) - посылка;

• F₁₀=((AB)(DM)) - заключение по F₈ и F₉ и правилу П8;

• F₁₁=(AB) - заключение по F₇ и F₁₀ и правилу m.t.;

• F₁₂=(А)(B) - заключение по F₁₁ и закону де Моргана;

• F₁₃=A - заключение по F₁₂ и правилу П2.

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