Аксиоматическое построение исчисления высказываний.

Рассмотренный выше подход к исчислению высказываний (путём их представления в виде пропозиционных форм, проведения эквивалентных преобразований этих форм с целью их упрощения, построения таблиц истинности и установление факта тождественной истинности высказывания) базировался на интуитивных, содержательных понятиях и получил название «теории моделей», когда задавал различные возможные значения пропозиционных букв (истина или ложь) во всевозможных комбинациях мы получали «модели», «реализации», «воплощения» того, что могут выражать те или иные высказывания.

Сейчас мы рассмотрим другой подход к построению логики и исчислению высказываний; а именно, аксиоматический подход или метод формальных теорий. Этот подход ещё называют теорией доказательств, и он связан с вопросом о том, нельзя ли описать логические доказательства и выводы так, как это делается в геометрии. Введём ряд определений.

Формальная (аксиоматическая) теория Т считается определённой, если выполняются следующие условия:

1. Задано конечное или счетное множество символов теории Т (множество, элементы которого можно поставить во взаимно однозначное соответствие числам натурального ряда 1, 2, 3, … называется счётным). Конечные последовательности символов теории Т называются выражениями этой теории Т;

2. Имеется эффективно распознаваемое подмножество выражений теории Т, называемое формулами этой теории;

3. Выделено некоторое подмножество формул, называемых аксиомами теории Т;

4. Имеется конечное множество правил вывода P1,...,Pn. Для каждого правила Pi существует некоторое положительное значение j, такое, что для каждого подмножества содержащего j формул и некоторую форму А, эффективно решается вопрос о применимости правила Pi к этому подмножеству формул и формуле А. Если правило применимо, то А называется следствием данных формул по правилу Pi.

Под словом «эффективно» подразумевается то, что существует некоторая предопределённая последовательность действий (т.е. алгоритм, процедура), позволяющая за конечное число шагов ответить на требуемый вопрос положительно или отрицательно.

Выводом в теории Т называется всякая конечная последовательность А1,…,Аn формул такая, что для любого i формула Аi есть либо аксиома теории Т, либо непосредственное следствие каких-либо предыдущих формул по одному из правил вывода.

Формула А теории Т называется теоремой этой теории, если существует вывод в Т, в котором последней формулой является А. Такой вывод называется доказательством (выводом) формулы А.

Следует отметить, что понятие теоремы не обязательно эффективно, т.е. может и не существовать эффективной процедуры, позволяющей определить по данной формуле, существует ли её вывод в теории Т. Теория, для которой такой алгоритм существует называется разрешимой, в противном случае – неразрешимой.

Формула А является следствием множества формул Г в теории Т тогда и только тогда, когда существует такая конечная последовательность формул А1,…,Аn, что Аn есть А и для каждого i Ai есть либо аксиома, либо элемент Г, либо непосредственное следствие некоторых предыдущих формул по одному из правил вывода. Такая последовательность называется выводом А из Г. Члены множества формул Г называются гипотезами или посылками вывода. Утверждение типа «А есть следствие Г» обозначают Г├А (можно читать «Г даёт А»). Для указания того, что А есть следствие Г именно в теории Т пользуются обозначением Г├тА. Для конечного множества Г={В1,…,Вn},

(где Вi∈Г элементы множества Г) вместо {В1,…,Вn}├тА обычно пишут В1,…,Вn├тА.

Если Г пустое множество ∅ (т.е. множество не содержащее ни одного элемента), то Г├А тогда и только тогда, когда А является теоремой (т.е. аксиомой или формулой

выводимой из аксиомы). Вместо ∅├А пишут ├А (т.е. А теорема). Очевидными являются следующие свойства понятия выводимости:

1. Если Г⊆ Δ (т.е. «Г подмножество Δ », «Г включается в Δ») и Г├А, то Δ├А. Т.е. если А выводимо из Г, то оно выводимым будет если к Г добавить новые посылки.

2. Г├А тогда и только тогда, когда в Г существует конечное подмножество Δ, для которого Δ├А. Достаточность условия вытекает из предыдущего свойства. Необходимость вытекает из того, что каждый вывод А из Г использует лишь конечное число посылок из Г.

3. Если Δ├А и Г├В для любого В из множества Δ, то Г├А, т.е. если А выводима из Δ и каждая формула из Δ выводима из Г, то А выводима из Г.