- •Исчисления высказываний
- •Определение формального исчисления
- •Исчисление высказываний генценовского типа
- •Эквивалентность формул
- •Нормальные формы
- •Семантика исчисления секвенций
- •Исчисление высказываний гильбертовского типа
- •Алгоритмы проверки общезначимости и противоречивости в ив
- •Логика и исчисления предикатов
- •Алгебраические системы. Формулы сигнатуры σ. Истинность формулы на алгебраической системе
- •Секвенциальное исчисление предикатов
- •Эквивалентность формул в
- •Нормальные формы
- •Теорема о существовании модели
- •Исчисление предикатов гильбертовского типа
- •Скулемизация алгебраических систем
- •Метод резолюций в исчислении предикатов
- •Некоторые проблемы аксиоматического исчисления предикатов
- •Разрешимость
- •Непротиворечивость и независимость
- •Полнота в узком смысле
- •Полнота в широком смысле
- •Элементы теории алгоритмов
- •Машины Тьюринга
- •Функции, вычислимые на машинах Тьюринга.
- •Рекурсивные функции и отношения
- •Примитивно рекурсивные функции.
- •Примитивно рекурсивные отношения.
- •Частично рекурсивные функции.
- •Рекурсивно перечислимые отношения
- •Неразрешимость исчисления предикатов. Теорема Геделя о неполноте. Разрешимые и неразрешимые теории.
Секвенциальное исчисление предикатов
Зафиксируем некоторую произвольную сигнатуру Σ и определим секвенциальное исчисление предикатов сигнатуры Σ (ИПС).
Алфавит ИПС получается из алфавита ИΠΣ добавлением символа следования ├, т.е. Α(ИΠСΣ) = Σ V {,¬,,, , , , (,),,, ├}. Формулами ИПС будут формулы сигнатуры Σ.
Секвенциями ИПС называются конечные последовательности следующих двух видов, где φ1,...,φn,φ — формулы ИПС:
φ1,…,φn ├φ
φ1,…,φn├ .
Примем следующие соглашения. Пусть x1,... ,хn — переменные, t1,...,tn — термы сигнатуры Σ и φ — формула сигнатуры Σ. Запись будет обозначать результат одновременной подстановки термов t1,...,tn вместо всех свободных вхождений в φ переменных x1,... ,хn соответственно, причем, если в тексте встречается запись , то предполагается, что для всех i = 1,..,n ни одно свободное вхождение в φ переменной xi не входит в подформулу φ вида yφ1 или yφ1, где у — переменная, входящая в ti. Вместо записи будем иногда писать φ( t1,...,tn). При этом, наряду с тем, что переменные x1,... ,хn в записи φ(x1,... ,хn) будут всегда предполагаться попарно различными, среди t1,...,tn могут быть равные термы.
Пример . 1. Обозначим через φ формулу х R(x, у, z), через t1 — терм F1(y,z,u), через t2 — терм F2(F3(z), w). Результат подстановки равен xR(x, F1 (y,z,u),F2(F3(z),w)), a результат подстановки равен х R(x, F1(y,z,u), F1(y,z,u)). Заметим, что результат последовательной подстановки может не совпадать с результатом одновременной подстановки.
2. Для формулы φ = х R(x, у, z) и терма t = F(y, x, и) запись (φ)ty недопустима, поскольку после подстановки терма t вместо свободной переменной у в формуле хR(x,F(y,x,u),z) вхождение переменной x в терм t становится связанным.
Аксиомами ИПС являются следующие секвенции:
φ├φ, где φ — формула сигнатуры Σ;
├(xx), где x— переменная;
(t1q1),...,( tnqn), ├
где t1,...,tn , q1,...,qn — термы сигнатуры Σ, φ — формула, удовлетворяющая условиям на записи и
Правила вывода ИПС задаются следующими записями, где Г — произвольные (возможно пустые) конечные последовательности формул ИΠСΣ, φ, ψ, χ — произвольные формулы ИПС:
(введение Λ).
(удаление ).
(удаление ).
(введение ).
(введение ).
(удаление , или правило разбора двух случаев).
(введение →).
(удаление →).
(удаление , или доказательство от противного).
(выведение противоречия)
(перестановка посылок).
(утончение, или правило лишней посылки).
где переменная х не входит свободно в формулы из Г (введение справа)
(введение слева)
(введение справа)
где переменная х не входит свободно в ψ и в формулы из Г (введение слева)
Понятия линейного доказательства в ИПС, доказательства в виде дерева в ИПС, доказуемой в ИПС секвенции (теоремы ИПС) и доказуемой в ИПС формулы определяются аналогично соответствующим понятиям ИС на основе аксиом 1-3 и правил вывода 1-16. Также аналогично предложению 1.2.1 устанавливается
Предложение 1. Секвенция S имеет доказательство в ИПС в виде дерева тогда и только тогда, когда S — теорема ИПС.
Пример. Приведем доказательство секвенции хyφ(x,y)├yхφ(х,у) в виде дерева для любой формулы φ(х,у):
Следующая теорема является синтаксическим аналогом теоремы 2.1.2 и позволяет преобразовывать доказуемые формулы ИС в доказуемые формулы ИПС.
Теорема 2. Пусть φ(Αι,..., Αn) — доказуемая формула ИС, φ1,...,φn — формулы сигнатуры Σ. Тогда в результате подстановки формул φ1,...,φn вместо всех соответствующих вхождений пропозициональных переменных Αι,..., Αn образуется доказуемая в ИПС формула φ(φ1,...,φn).
Доказательство. Пусть D — дерево доказательства секвенции ├ φ (Αι,..., Αn) в ИС. Тогда, заменяя в дереве D переменные Αι,..., Αn соответственно на φ1,...,φn, а остальные пропозициональные переменные — на формулу (x х), получаем дерево D1, являющееся деревом доказательства секвенции ├ φ(φ1,...,φn).
Предложение 3. Для любой формулы φ, удовлетворяющей условиям на запись , в ИПС доказуемы следующие секвенции:
x1,…,xn├
├ x1,…,xn
Доказательство. а) Пусть y1,…,yn – попарно различные переменные, не входящие в , в t1,…,tn и отличных от x1,…,xn. Для k=1..n имеет место равенство: т.е. одновременная подстановка совпадает с последовательной, (т.к. yi так выбраны) и выполнены все условия на запись формулы. Тогда следующее дерево будет доказательством в ИПС:
обозначим =. Для выполнено условие на запись и для всех k=1..n , тогда т.е. секвенция доказуема. Т.к. , то доказана секвенция . Осталось применить правило сечения к данным секвенция:
пункт b) доказать аналогично с помощью правил 15 и 16.
Предложение 4. В ИПС допустимы правила а) …о) и
п) (подстановка термов)
р) (удаление )
Доказательство. Первые 14 правил доказываются как и в ИС. Докажем правило п). Будем использовать Предложение 3.
докажем р):
.
Покажем, что для отношения на множестве термов доказуемы обычные свойства равенства (рефлексивности, симметричности и транзитивности), т.е. доказуемо в ИПС , что — отношение эквивалентности.
Предложение 5. Для любых термов t,q,r Τ(Σ) следующие секвенции доказуемы в ИПС:
├(tt);
(tq)├(qt);
(tq),(qr)├(tr).
Доказательство. Доказуемость секвенции ├ (tt) устанавливается применением допустимого правила (п) из предложения.4:
Для доказательства секвенции (б) рассмотрим аксиому которая равна секвенции (tq),( tt)├ (qt). Выпишем дерево, которое с участием этой аксиомы представляет доказательство свойства симметричности:
Доказуемость секвенции (в) устанавливает следующее дерево:
.
Пусть A = <Α;Σ> — алгебраическая система, S = S(x1,..., xn) — секвенция ИПС, все свободные переменные формул которой содержатся среди x1,..., xn. Будем говорить, что секвенция S истинна на элементах a1,...,an А в алгебраической системе A и писать A ╞ S(a1,...,an), если выполняется одно из следующих условий:
S равна φ1,..., φn ├ψ и из A |= φi(a1,...,an) для всех i = 1,... n следует A ╞ ψ(a1,...,an);
S равна φ1,..., φn ├ и хотя бы одна из формул φ1,..., φn ложна на элементах a1,...,an А в алгебраической системе A.
Если секвенция S не истинна на элементах a1,...,an А в алгебраической системе A, то будем говорить, что S ложна на элементах a1,...,an А в A. В частности, секвенция ├ ложна на любой алгебраической системе.
Секвенция S = S(x1,..., xn) в ИПС называется тождественно истинной, если S истинна на любых элементах a1,...,an А в любой алгебраической системе A = <Α; Σ>.
В дальнейшем нам предстоит доказать теорему о полноте для исчисления предикатов, установленную К. Гёделем и утверждающую, что класс доказуемых в ИПС секвенций совпадает с классом тождественно истинных секвенций ИПС. Одна часть этого утверждения — это
Теорема 6. (теорема о непротиворечивости ИПС). Если секвенция S доказуема в ИПС, то S тождественно истинна. В частности, не все формулы ИПС доказуемы в ИПС.
Доказательство проводится индукцией по высоте дерева доказательства секвенции S. Тождественная истинность аксиом ИПС очевидна. Проверку сохранения тождественной истинности при переходе по правилам 1-16 мы проведем на примере правила 14
оставив рассмотрения остальных правил в качестве упражнения. Итак, пусть секвенция Г, (φ)tx├ψ тождественно истинна, т.е. в предположении истинности в системе A = <Α; Σ> на каких-то элементах a1,...,an А всех формул из Г и формулы (φ)tx мы имеем A |= ψ(a1,...,an). Если в системе A на каких-то элементах a1,...,an А истинны все формулы из Г и формула х φ, то, в частности, будет справедливо A ╞ ψ(a1,...,an). Значит, по условию будет верно A╞ ψ(аι,..., αη). Следовательно, секвенция Г, x φ├ψ тождественно истинна.