Подформулы

1. Если формула есть переменная, то единственной ее подформулой является она сама.

2. Если формула имеет вид ù А, то ее подформулами являются она сама и все подформулы формулы А.

3. Если формула имеет вид А * В, где знак * Î {&, V, ®}, то ее подформулами являются она сама и все подформулы формул А и В.

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

Проинтерпретируем логические связки &, V, ®, ùсоответствующими логическими операциями (функциями).

Если все переменные формулы А содержатся среди переменных р₁,р₂,...,р_n, то пишем А(р₁,р₂,...,р_n). Если формула А(р₁,р₂,...,р_n) построена из переменных р₁,р₂,...,р_n и только из них, то скажем тогда, что р₁,р₂,...,р_n есть полный список переменных формулы А.

Интерпретация формулы А(р₁,...,р_n) есть набор I = (a₁,...,a_n) из И и Л.

Индукцией по построению формулы А определим понятие значения I(A) формулы А(р₁,...,р_n) на интерпретации I.

1. Если А есть р_i, то I(A) = а_i.

2. Если А есть формула (В * С), где знак * Î {&,V,®}, или же формула ù В, то I (В * С) = I(В) * I(С); I(ù В) = ù (I(В)).

Для удобства вместо I(A) будем писать также А(a₁,...,a_n).

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

Интерпретация I удовлетворяет формуле А (А выполняется на I), если А истинна на I. Интерпретация I опровергает А, если А ложна на I. Если интерпретация I удовлетворяет формуле А, то I называется также моделью формулы А.

Подстановка (П). Индуктивное определение.

1. Если формула А есть переменная р, то подстановка формулы В на место переменной р в формуле А есть В.

2. Если формула А переменной р не содержит, то подстановка есть снова формула А.

3. Если формула А имеет вид ù C или С * Е, где * есть один из знаков &, V, ®, то подстановки

ù

= ù; = *.

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

Система аксиом (П.С.Новикова).

А1) р ® (q ® р).

А2) (р ® (q ® r)) ® ((р ® q) ® (р ® r)).

A3) р & q ® р.

А4) р & q ® q.

А5) (р ® q) ® ((р ® r) ® (р ® q & r)).

А6) р ® р V q.

А7) q ® р V q.

А8) (р ® r) ® ((q ® r) ® (р V q ® r)).

А9) (р ® q) ® (ù q ® ù р).

А10) р ® ù ù р.

А11) ù ù р ® р.

Заметим, что в качестве аксиом взяты тождественно истинные формулы.

Правила вывода (ПВ)

Правило подстановки имеет вид

,

т.е. от формулы А(р) с переменной р можно перейти к формуле

Правило заключения (ПЗ) имеет вид

т.е. от двух формул А и А ® В можно перейти к формуле В. Это правило известно еще как правило ²modus ponens² (утверждающий модус).

Исчисление высказываний (ИВ) составляют формальные символы, формулы, аксиомы и правила вывода.

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

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

Всякая аксиома есть доказуемая формула, длина доказательства которой
равна 1.

Приведем примеры доказуемых формул и некоторых вспомогательных (производных) правил вывода, применение которых к формулам при необходимости можно исключить, но использование их сделает формальную систему ИВ выразительнее и естественнее.

Доказательства формул сопроводим краткими пояснениями. Например, A3 будет означать, что формула является аксиомой A3; ПЗ(2,3) - формула получена применением правила заключения (ПЗ) к формулам (2) и (3); - формула получена подстановкой в формулу (4) формулы ù р на место переменной q. Знак ├ будет означать: формула доказуема в ИВ.

Теорема 1. ├ р ® р.