5. Определение формулы, выводимой из совокупности формул h.

В исчислении высказываний некоторые формулы могут быть получены не только из совокупности аксиом, но и из совокупности формул Н, не являющихся аксиомами. Такие формулы называют выводимыми из совокупности формул Н. Дадим определение таким формулам.

Пусть у нас имеется некоторая совокупность формул

Тогда:

1. всякая формула является формулой, выводимой из Н;

2. всякая доказуемая формула выводима из Н;

3. если формулы С и выводимы из совокупности Н, то формула В также выводима из Н (правило заключения для выводимых формул).

То, что некоторая формула В выводима из совокупности Н, записывают так:.

Число формул совокупности Н может быть самым различным. Если Н=0, то предполагается, что совокупность (множество) Н не содержит никаких других формул, кроме аксиом исчисления высказываний. Если указано, что совокупность Н состоит из некоторых формул, например A,B,C, то предполагается (по умолчанию), что в эту совокупность входят и аксиомы. Причем формулы A, B и C не обязательно должны быть доказуемыми.

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

Если же совокупность формул Н содержит хотя бы одну недоказуемую формулу, то класс формул, выводимых из совокупности Н, шире класса доказуемых формул.

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

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

1. он является одной из формул совокупности Н;

2. он является доказуемой формулой;

3. он получается по ПЗ (для доказуемых и выводимых формул) из двух любых предшествующих членов последовательности .

Из определения выводимой формулы и вывода из совокупности формул Н следуют свойства вывода:

1. всякий начальный отрезок вывода из совокупности Н есть вывод из Н;

2. если между двумя соседними членами вывода из Н (в начале или в конце) вставить некоторый вывод из Н, то полученная новая последовательность формул будет выводом из Н. Например, если совокупности формул и являются выводами из Н, то совокупность , является тоже выводом из Н.

3. всякий член вывода из совокупности Н является формулой, выводимой из Н;

4. если ( ₋ знак включения, читается: “множество Н включено в множество W “ или “Н содержится в W “), то всякий вывод из совокупности Н является и выводом из совокупности W.

5. для того чтобы формула В была выводима из совокупности формул Н, необходимо и достаточно, чтобы существовал вывод этой формулы из Н.

7.Проблемы аксиоматического исчисления высказываний

Всякая аксиоматическая теория для своего обоснования требует рассмотренных четырех проблем:

1) проблемы разрешимости,

2) проблемы непротиворечивости,

3) проблемы полноты,

4) проблемы независимости.

Раскроем эти проблемы чуть детальнее, сформулировав их в виде теорем, но, не приводя соответствующего доказательства.

1. Проблема разрешимости исчисления высказываний заключается в доказательстве существования алгоритма, который позволил бы для любой заданной формулы исчисления высказываний определить, является она доказуемой или нет.

Теорема 1. Проблема разрешимости для исчисления высказываний разрешима.

2. Суть проблемы непротиворечивости исчисления высказываний состоит в следующем. Логическое исчисление называется непротиворечивым, если в нем недоказуемы никакие две формулы, из которых одна является отрицанием другой.

Иначе говоря, аксиоматическое исчисление называется непротиворечивым, если в нем не существует такая доказуемая формула А, что наряду с ней доказуема и формула .

Теорема 2. Исчисление высказываний непротиворечиво.

3. Проблема полноты исчисления высказываний. Существует два понятия полноты − в узком смысле и в широком смысле.

Аксиоматическое исчисление называется полным в узком смысле, если добавление к списку его аксиом любой недоказуемой в исчислении формулы в качестве новой аксиомы приводит к противоречивому исчислению.

Исчисление высказываний называется полным в широком смысле, если любая тождественно истинная формула в алгебре логики доказуема в исчислении высказываний.

Теорема 3. Исчисление высказываний полно в узком смысле.

Теорема 4. Исчисление высказываний полно в широком смысле.

4. Проблема независимости аксиом исчисления высказываний. Для каждого аксиоматического исчисления возникает вопрос о независимости его аксиом; а именно: нельзя ли какую-нибудь аксиому вывести из остальных аксиом, применяя правила вывода?

Если для некоторой аксиомы это возможно, то ее можно исключить из списка аксиом системы, и возможности логического исчисления при этом не изменятся. Иначе говоря, класс доказуемых формул не изменится.

Аксиома называется независимой от всех остальных аксиом исчисления, если она не может быть выведена из остальных аксиом.

Система аксиом исчисления высказываний называется независимой, если каждая аксиома системы независима.

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

Существует и обратная теорема о том, что каждая формула, доказуемая в исчислении высказываний, является тождественно истинной в алгебре логики. Эту теорему можно применять в тех случаях, когда установление тождественной истинности формулы (ТИФ) заменяют установлением ее доказуемости.

О тесной взаимосвязи ТИФ и доказуемых формул свидетельствует тот факт, что часто в математической логике тождественная истинность формулы обозначается символом (ранее в подразд.1.3 для этой цели мы использовали запись ), по своему начертанию очень похожим на символ доказуемой формулы. Тождественно истинную формулу еще называют общезначимой или логическим законом.

Таким образом, прямую и обратную теоремы о полноте в широком смысле кратко можно записать так:

следует, следует