Главная страница Случайная страница
Разделы сайта
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника
A) либо аксиомой;
|
|
B) либо ранее доказнной формулой (теоремой);
C) либо следует из формул, предшествующих ей в последовательности, по
правилам (MP), (У[), (В\), (В[);
d) либо формуле Вi предшествует формула \x B(x), а сама формула Вi есть B(t), где
T – новая константа.
При этом следует соблюдать еще такие требования:
1) не допускается применение правила (В[) по переменным, свободным хотя бы в
одной формуле вида \x B(x), к которым ранее было применено правило (У\);
Формула A не содержит новых предметных констант, введенных с помощью
правила (У\).
Формула В называется доказуемой в исчислении предикатов, если для нее существует процедура доказательства. Число n называется длиной доказательства.
Еще раз обратим внимание на то, что использование в доказательстве ранее доказанных теорем не расширяет класс доказуемых формул, но часто заметно упрощает процесс доказательства. Этой же цели служат вспомагательные (производные) правила выода, о чем речь пойдет чуть позже.
Построим доказательство нескольких формул логики предикатов.
І. |- $х " у А(х, у) É " у $х А(х, у)
Доказательство.
1. " у А(х, у) É А(x, z) - Ax. 11, где z – терм, не входящий
в формулу А(х, у).
2. A(x, z) É $n A(n, z) - Ах. 12, где n - терм, не входящий
в формулу А(x, z).
3. $n A(n, z) É $x A(x, z) - по правилу переименования
связанной переменной.
4. A(x, z) É $x A(x, z) - из (2, 3) по правилу транзитивности
импликации.
5. " у A(x, y) É $x A(x, z) - из (1, 4) по правилу транзитивности
импликации.
6. $х " у (х, у) É $х А(х, z) - (В$) к (5).
7. $х " у (х, у) É " z $x (x, z) - (B") к (6).
8. " z $x (x, z) É " y $x (x, y) - по правилу переименования
свяанной переменной.
9. |- $х " у А(х, у) É " у $х А(х, у) - из (7, 8) по правилу транзитивности
импликации
П. |- Ø $х А(х) É " х Ø А(х)
Доказательство.
1. А(у) É $х А(х) - Ах. 12.
2. Ø $х А(х) É Ø А(у) - из (1) по правилу контрапозиции.
3. Ø $х А(х) É " у Ø А(у) - (В") к (2).
4. " у Ø А(у) É " х Ø А(х) - по правилу переименования
связанной переменной.
5. |- Ø $х А(х) É " х Ø А(х) - из (3, 4) по правилу транзитивности
импликации.
Понятие доказательства в S5 можно расширить с помощью понятия вывода, если позволить вставлять в последовательностьВ1, В2..., Вn формулы допущения (гипотезы). Последнее обстоятельство также позволяет упрощать процесс получения следствий из посылок.
Построим вывод формулы В É " х Р(х) из формулы " у (В É Р(у)).
Вывод.
1. " у Р(у) É Р(х) - Ах. 12.
2. " у Р(у) É " х Р(х) - (В") к (1).
3. " у (В É Р(у)) - допущение.
4. " у (В É Р(у)) É (В É Р(z)) - Ах. 12.
5. В É Р(z) - (МР) к (3, 4).
6. В É " z Р(z) - (В") к (5).
7. (" у Р(у) É " х Р(х)) É ((В É (" z Р(z) É " х Р(х)) - Ах. 1.
8. В É (" z Р(z) É " х Р(х)) - (МР) к (2, 7).
9. (В É " z Р(z)) É ((В É (" z Р(z) É " х Р(х)) É (В É " х Р(х)) - Ах. 2а.
10. (В É (" z Р(z) É " х Р(х)) É (В É " х Р(х) - (МР) к (6, 9).
11. В É " х Р(х) - (МР) к (8, 10).
Рассмотрим теперь важнейшее производное правило исчисленич предикатов – теорему о дедукции.
2. Теорема о дедукции в S5.
Теорему о дедукции рассмотрим в ее простейшей версии:
А1,..., Аn-1, Аn |- В____
А1,..., Аn-1 |- Аn É B
(все переменные в допущении Аn связаны).
Представим дедукцию B в виде последовательности В1,..., Вn, где Вn = В. Посмотрим, можно ли превратить эту дедукцию в дедукцию В1,..., Вm, где Вm = Аn É B.
|
|