Понятия формальной теории

Содержание
Формальная теория
Выводимость в формальной теории
Интерпретация
Разрешимость
Общезначимость
Непротиворечивость
Полнота и независимость

Формальная теория
множество А символов, образующих алфавит
множество слов F в алфавите А, которые называются формулами
подмножество В формул,
которые называются аксиомами
множество R отношений на множестве формул , которые называются правилами вывода
.

Ограничения (1)
Алфавит A может быть конечным или бесконечным
Множество формул F обычно задается индуктивно, как правило, оно бесконечно
Множества A и F по совокупности определяют язык формальной теории, или сигнатуру

Ограничения (2)
Множество аксиом B может быть конечно или бесконечно
Бесконечное множество аксиом B , как правило, задают в виде конечного множества схем и правил порождения из этих схем конкретных аксиом
Множество правил вывода R обычно конечно

Свойства формальной теории
выводимость
интерпретация
общезначимость
разрешимость
непротиворечивость
полнота
независимость

Выводимость
Пусть - формулы теории Т, т.е.
Если существует такое правило вывода R, что
, то говорят, что формула G
непосредственно выводима из формул
по правилу вывода R:
где формулы F называются посылками, а формула G заключением

Вывод, гипотеза, теорема
Вывод формулы G из формул – – это такая последовательность формул , что Fn=G , а любая формула Fi - либо аксиома, либо исходная формула, либо непосредственный вывод из ранее полученных формул
Если в теории Т существует вывод формулы G из формул , то записывают
├ G, где – - гипотезы
Теорема – формула, выводимая только из аксиом, без гипотез

Интерпретация
Интерпретацией формальной теории T в область интерпретации M называется функция, h:F→M, которая каждой формуле F теории T однозначно сопоставляет некое содержательное высказывание относительно объектов множества M
Высказывание может быть истинно или ложно, или не иметь истинностного значения. Если оно истинно, то говорят, что формула выполняется в данной интерпретации

Интерпретация
Например, припишем значение 0 или 1 атомарным формулам (простым высказываниям), которые входят в сложные, что будет называться интерпретацией h
Говорят, что формула A исчисления истинна при некоторой интерпретации h тогда и только тогда, когда h(А)=1, в противном случае говорят, что А ложна при интерпретации h

Разрешимость
Формальная теория Т называется разрешимой, если существует алгоритм, который для любой формулы теории определяет, является она теоремой или нет

Алгоритм
Под алгоритмом в интуитивном смысле мы понимает такую последовательность действий, выполнение которых позволяет получить решение задачи регулярным путем за конечное число шагов

Свойства алгоритма
дискретность шагов
детерминируемость
регулярность
конечность
массовость

Алгоритм
Например, правила дорожного движения не являются алгоритмом, т.к. содержат неоднозначность
Ярким примером такой неоднозначности может служить дорожный знак «прямо и направо»

Общезначимость
Формула общезначима (тавтология), если она истинна в любой интерпретации
Формула называется противоречием, если она ложна в любой интерпретации

Непротиворечивость
Формальная теория семантически непротиворечива, если ни одна из ее теорем не является противоречием
Формальная теория формально непротиворечива, если в ней не являются выводимыми одновременно формулы F и