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

Одним из возможных вариантов (Гильбертовской) аксиоматизации логики высказываний является следующая система аксиом:

;

;

;

;

;

;

;

;

.

вместе с единственным правилом:

(Modus ponens)

Теорема корректности исчисления высказываний утверждает, что все перечисленные выше аксиомы являются тавтологиями, а с помощью правила modus ponens из истинных высказываний можно получить только истинные. Доказательство этой теоремы тривиально и сводится к непосредственной проверке. Куда более интересен тот факт, что все остальные тавтологии можно получить из аксиом с помощью правила вывода — это так называемая теорема полноты логики высказываний.

 

18. Правило вывода Modus ponens. Modus ponens (правило заключения): если A и A→B — выводимые формулы, то B также выводима.

Форма записи: , где A, B — любые формулы.

Modus ponens — правило вывода в исчислении высказываний. Является частным случаем правила резолюций. С помощью правила modus ponens из истинных высказываний можно получить только истинные. Доказательство этой теоремы тривиально и сводится к непосредственной проверке. Куда более интересен тот факт, что все остальные тавтологии можно получить из аксиом с помощью правила вывода — это так называемая теорема полноты логики высказываний.

Понятие вывода.

Определение. Выводом из конечной совокупности формул H называется всякая конечная последовательность формул , всякий член которой удовлетворяет одному из следующих трех условий: 1) является одной из формул совокупности H; 2) является доказуемой формулой; 3) получается по правилу заключения из двух любых предшествующих членов последовательности .

Свойства вывода:

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

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

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

Следствие. Всякий вывод из H является выводом его последней формулы.

4) Если , то всякий вывод из H является из W.

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

 

Понятие вывода

ками вывода. Свойства:

 

23. Теорема о дедукции

Лемма Кальмара

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

Формулы исчисления предикатов

Сигнатура, алгебры и модели.

Сигнатурой называется набор Σ = (R, F, C,ρ) состоящий из множеств:

R — множество символов для отношений (предикатов),

F — множество функциональных символов,

C — множество символов констант

и функции ρ — сопоставляющей элементам R и F их арность. Пример σ=<+,*,<,=,1>

 

Формальная система исчисления предикатов.

Язык логики первого порядка строится на основе сигнатуры, состоящей из множества функциональных символов и множества предикатных символов . С каждым функциональным и предикатным символом связана арность, то есть число возможных аргументов. Допускаются как функциональные, так и предикатные символы арности 0. Первые иногда выделяют в отдельное множество констант. Кроме того, используются следующие дополнительные символы

Символы переменных (обычно и т. д.),

Пропозициональные связки: ,

Кванторы: всеобщности и существования ,

Служебные символы: скобки и запятая.

Перечисленные символы вместе с символами из и образуют Алфавит логики первого порядка. Более сложные конструкции определяются индуктивно:

Терм есть символ переменной, либо имеет вид , где — функциональный символ арности , а — термы.

Атом имеет вид , где — предикатный символ арности , а — термы.

Формула — это либо атом, либо одна из следующих конструкций: , где — формулы, а — переменная.

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

 

Система аксиом исчисления предикатов.