Главная страница Случайная страница КАТЕГОРИИ: АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника |
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.
|