Другие аксиоматизации исчисления высказываний

ЛОГИЧЕСКИЕ СОЕДИНИТЕЛИ, ЧАСТИЧНАЯ ФОРМУЛА, ФОРМУЛА ДОКАЗАТЕЛЬСТВА, СИСТЕМА АКСИОМ РАССУЖДЕНИЙ
ПЛАН

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

2. Другие аксиоматизации исчисления высказываний

.

Аксиоматическая теория высказываний
Применение логики в математических теориях, рассуждениях, связанных с доказательством и принятием решений, опирается на теорию логического вывода.
Пример рассуждения и вывод: «Если сегодня не будет дождя, то пойдем гулять, иначе пойдем в кино. Сегодня дождь. Следовательно, пойдем в кино». Формализация и доказательство истинности вывода:
Формула рассуждения — тавтология, поэтому выбор правильный.
Множество истинных высказываний составляет предметную область знаний. Меньшая часть этих высказываний (правил) считается доказуемой.
В математической теории доказуемые высказывания называются теоремами. Теоремы выводятся из некоторого множества априори истинных высказываний (тавтологий), которые называются аксиомами. Подобные математические теории называют аксиоматическими.
В математической логике минимальное множество первичных аксиом, из которых следуют все тавтологии, называют схемами аксиом. Логика высказываний является аксиоматической теорией исчисления высказываний. Теоремы этой теории являются тавтологиями.
Известны различные схемы аксиом^[1], например схемы аксиом Гильберта и Аккермана:
Al) A v А —> А;
А2) А —> (A v В);
АЗ) (A v В) —> (В v А);
А4) (A^B)^(CvA^Cv В).
Все аксиомы — тавтологии в классической логике. Следовательно, тавтологией является конъюнкция аксиом

Подстановки любых формул в аксиомы преобразуют их в новые формулы, которые являются тавтологиями.
Доказывается¹, что бесконечное (всё) множество тавтологий может быть получено из этой схемы аксиом с использованием подстановок и одного правила отделения МР (modus ponens (лат.) — правило вывода) — «если условие р истинно и доказано, что из р всегда следует q, то следствие q истинно»:

По-другому правило формулируется так: «если условие р — тавтология и из р следует q — тавтология, то следствие q — тавтология». Утверждение можно записать в виде

Доказательство этой тавтологии в любой области интерпретации:

Определение. Формальное доказательство (схема вывода) является методом подстановок аксиом в аксиомы и полученные при этом формулы с применением логических правил. Метод завершается получением заданной формулы. При этом:

• 
  • все формулы в последовательности — тавтологии, и последняя формула в этой последовательности — логическое следствие (теорема);
  
• 
  • из схемы аксиом выводятся только тавтологии, которые обозначаются I—> В.
  

Вывод — общий метод доказательства в любой правильной аксиоматической теории.
Для упрощения вывода в теории исчисления высказываний используются также тождественные алгебраические подстановки в аксиомы - любые подстановки в тавтологии преобразуют их в тавтологии.
Рассмотрим пример аксиоматического вывода — докажем теорему н» (A v -лЛ), используя вывод из аксиом:

• 
  1) A v А —> А (аксиома А1);
  
• 
  2) ((A v А) —> А) —> (-A v (A v А) —> -A v А) (аксиома А4: С/—Л, А/ (A v А), В/А);
  
• 
  3) —A v (A v А)^> —A v А (правило МР: (1,2) —> 3);
  
• 
  4) А —> A v А (подстановка в аксиому А2: В/А);
  
• 
  5) (А —> (A v А)) —> (А —> А) (подстановка в аксиому А1 и транзитивность);
  
• 
  6) А —> А (МР: (4, 5) -> 6);
  
• 
  7) -A v А (замена импликации 6 на дизъюнкцию);
  
• 
  8) —A v А —^ A v —А (подстанока в аксиому АЗ: В/A, А/ЧА);
  
• 
  9) A v -.А (правило МР: (7, 8) ^ 9).
  

Таким образом, в результате применения подстановок аксиом в аксиомы Гильберта и последующие промежуточные формулы выведена предполагаемая теорема в виде формулы h(Av —А). ^[2]
Свойства аксиоматической теории логического вывода:

• 
  1) полнота теории. Если формула А — тавтология, то она является теоремой исчисления высказываний;
  
• 
  2) непротиворечивость теории. Не существует формулы А, такой что А и —А являются теоремами.
  

Следствие. Существуют формулы в различных интерпретациях, которые не являются тавтологиями и невыводимы в аксиоматической теории Гильберта и Аккермана (т.е. если А — тавтология, то -иА не тавтология (противоречие) и не выводимо средствами аксиоматической теории — теорема К. Гёделя).