Формальные теории. Основные понятия и определения

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

Выводимость

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

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

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

Если в теории Т существует вывод формулы G из формул F1, …, Fn, то это записывают следующим образом:

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

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

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

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

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

Синтаксис

Синтаксисом называется набор правил конструирования ППФ.

Семантика

Семантикой называется набор правил интерпретации формул.

Интерпретация

Интерпретацией  называется приписывание формуле одного из двух значений истинности: 1 (истинно) или 0 (ложно). Композиционность семантики заключается в том, что приписываемое значение истинности некоторой формулы зависит от значений истинности составляющих высказываний и структуры формулы.

 

Логика - доступно для всех