МЛОИ

Например, подстановка в формулу X&(X?Y)?Y вместо переменной Y формулы ?(A?B) приводит к формуле X&(X??(A?B))??(A?B), которая будет логическим следствием формулы X&(X?Y)?Y, в чем легко убедиться, построив таблицу истинности для формулы:
(X&(X?Y)?Y)?(X&(X??(A?B))??(A?B)).
3.Правило modus ponens. Это правило позволяет из двух формул X и X?Y выводить третью формулу Y.
Формула Y является логическим следствием формул X и X?Y в смысле приведенного выше определения, поскольку формула (X&(X?Y))?Y является тождественно-истинной (тавтологией), в чем можно убедиться с помощью следующей таблицы истинности:

(
X
&
(
X
?
Y
)
)
?
Y

Л
Л

Л
И
Л

И
Л

Л
Л

Л
И
И

И
И

И
Л

И
Л
Л

И
Л

И
И

И
И
И

И
И

Например, из формул A?B ?C и A?B правило modus ponens позволяет вывести формулу С.
4.Правило modus tollens. Это правило формулируется так: из формул X&Y и ?Y выводится формула ?X.
Формула ?X является логическим следствием формул X&Y и ?Y в смысле приведенного выше определения, поскольку формула ((X&Y)&?Y)??X является тождественно-истинной (тавтологией), в чем можно убедиться с помощью следующей таблицы истинности:

(
(
X
&
Y
)
&
?
Y
)
?
?
X

Л
Л
Л

Л
И
Л

И
И
Л

Л
Л
Л

Л
И
Л

И
И
Л

И
Л
Л

Л
Л
И

И
Л
И

И
И
И

Л
Л
И

И
Л
И

Например, из формул (A?B)&C и ?C по правилу modus tollens выводится формула ?(A?B).
Итак, можно следующим образом более формально определить понятие логического вывода (и логического следования):
Логическим выводом (или просто, выводом) формулы Ф из множества посылок (гипотез) F={F1, F2, F3, … , Fm} называют последовательность формул вида: Ф1,Ф2,…,Фi-1,Фi,…,Фn=Ф, таких, что либо Фi — тавтология, либо Фi? F, либо Фi является конъюнкцией формул из F, либо Фi получена из формул множества F, или тавтологий логики высказываний, или ранее выведенных в данном выводе формул Ф1, Ф2, …,Фi-1 с помощью правил вывода.
Формулу Ф будем называть в этом случае логическим следствием множества формул F={F1,F2,F3,…, Fm}.
Тот факт, что формула Ф выводима из множества посылок F={F1,F2,F3,…, Fm} будем обозначать: F1,F2,F3,…, Fm ?? Ф.
Заметим, что в соответствии с определением вывода все тавтологии логики высказываний считаются выводимыми формулами, притом из пустого множества посылок, то есть, если A — тавтология, то ??A.
Примем без доказательства следующую теорему, которая называется теоремой дедукции.
Теорема дедукции:
Если F1,F2,F3,…, Fm ?? Ф, то F1,F2,F3,…, Fm-1 ?? (Fm ?Ф), и наоборот.
Эта теорема говорит о возможности переноса формул логики высказываний через знак выводимости ??.
Замечание: m-кратное применение теоремы дедукции приведет к утверждению выводимости формулы
??(F1?(F2?(F3 ?(…?(Fm-1 ?(Fm ?Ф))…)))).

Приведем примеры логического вывода формул логики высказываний из множества посылок.