Т. А. Сливина математическая логика и теория алгоритмов

Теорема 1. Каждая формула, доказуемая в исчислении высказываний, является тождественно истинной в алгебре высказываний.
Теорема 2. (о выводимости). Пусть А – некоторая формула исчисления высказываний; х₁, х₂, ..., х_п – набор переменных, содержащий все переменные, входящие в формулу А; а₁, а₂,...,а_п – произвольный фиксированный набор значений этих переменных. Обозначим через Н конечную совокупность формул , где
1. Если , то Н├ А.
2. Если , то Н├ .
Теорема 3. Каждая тождественно истинная формула алгебры высказываний доказуема в исчислении высказываний.
Доказательство этих теорем предлагается рассмотреть самостоятельно или на семинарских занятиях.


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

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

1. 
   проблемы разрешимости,
   
2. 
   проблемы непротиворечивости,
   
3. 
   проблемы полноты,
   
4. 
   проблемы независимости.
   

1. Проблема разрешимости исчисления высказываний.
Проблема разрешимости исчисления высказываний заключается в доказательстве существования алгоритма, который позволил бы для любой заданной формулы исчисления высказываний определить, является ли она доказуемой или не является.
Теорема 1. Проблема разрешимости для исчисления высказываний разрешима.
2. Проблема непротиворечивости исчисления высказываний. Логическое исчисление называется непротиворечивым, если в нем не доказуемы никакие две формулы, из которых одна является отрицанием другой.
Иначе говоря, аксиоматическое исчисление называется непротиворечивым, если в нем не существует такая формула А, что доказуема А и доказуема .
Проблема непротиворечивости заключается в выяснении вопроса: является данное исчисление непротиворечивым или нет?
Если в исчислении обнаруживаются доказуемые формулы вида А и , то такое исчисление называется противоречивым.
Если бы в исчислении высказываний некоторые формулы А и оказались доказуемы, то в нем бы оказалась доказуемой любая формула В.