Выводимость

Пусть F₁,..., F_n, G - формулы теории Т, то есть F₁,..., F_n, G являются ППФ. Если существует такое правило вывода R, что (F₁,..., F_n, G) Î R, то говорят, что формула G непосредственно выводима из формул F₁,..., F_n по правилу вывода R. Обычно этот факт записывают следующим образом:

, где формулы F₁,..., F_n называются посылками, а формула G – заключением.

ЗАМЕЧАНИЕ. Обозначение правила вывода справа от черты, разделяющей посылки и заключение, часто опускают, если оно ясно из контекста.

Если в теории Т существует вывод формулы G из формул F₁,..., F_n, то это записывают следующим образом:

F₁,..., F_n├ _Т G, где формулы F₁,..., F_n называются гипотезами вывода. Если теория Т подразумевается, то ее значение обычно опускают.

Если ├ _Т G, то формула G называется теоремой теории Т (то есть теорема – это формула, выводимая только из аксиом, без гипотез).

Если Г├ _Т G, то Г, D├ _Т G, где Г и D- любые множества формул (то есть при добавлении лишних гипотез выводимость сохраняется).

Правила вывода делятся на прямые и непрямые. Прямые правила вывода – это правила непосредственного перехода от одних формул к другим, т.е. переход от посылки к заключению. Им сопоставляются определенные шаги формального вывода. Непрямые правила вывода суть правила перехода от одних формальным выводам к другим. Таким правилам соответствуют мета утверждения о преобразованиях одних формальных выводов в другие.

Еще одним интересным способом рассуждения, который может быть оформлен в виде непрямого производного правила, является метод доказательства от противного. Суть его сводится к следующему. Пусть нам надо доказать вывод формулы А из посылок Г. Тогда применяют следующий формальный прием: отрицание формулы А добавляют к множеству формул Г и пытаются получить из посылок ØА, Г противоречие. Если такое противоречие получено, то это означает, что можно построить вывод А из Г