НАТУРАЛЬНОЕ УЗКОЕ ИСЧИСЛЕНИЕ ПРЕДИКАТОВ
В натуральном узком исчислении предикатов определение формулы исчисления предикатов такое же, как и в аксиоматическом представлении узкого исчисления предикатов.
Основными правилами вывода в натуральном исчислении предикатов являются:
1. Все основные правила вывода исчисления высказываний.
2. Правила введения и удаления кванторов общности и существования.
Для записи схем правил введения и удаления кванторов общности и существования можно пользоваться символом j (х/ w ), обозначающем выражение, полученное из j подстановкой вместо именной переменной х выражения w при выполнении следующих условий:
1) В выражении j замена переменной х производится лишь в тех местах, где она свободна. Если х входит в j несколько раз, то столько же раз она заменяется выражением w.
2) Если в j переменная х находится в области действия квантора, связывающую предметную переменную z, то вместо х не подставляется выражение содержащее z в качестве свободной переменной. Короче говоря, подстановку следует производить так, чтобы свободные переменные подставляемого выражения не оказались связанными в выражении, полученном в результате подстановки.
Если это правило нарушается, то можно получить ложное высказывание. Так, в выражении $ m (m>n) переменная m связана, а переменная n свободна. Если мы вместо n подставим m+1, то получим ложное выражение: $ m (m> m+1).
Правило удаление квантора общности:
|
|
У " .
Примером рассуждения по правилу У":
.
Правило введения квантора общности:
В " применяется лишь при условии, что переменная х не входит в качестве свободной в допущение косвенного доказательства.
Примером рассуждения по правилу
В " : .
Правило введение квантора существования :
В $ .
Примером рассуждения по правилу В$:
Четное и простое число
$ х (х – четное и простое).
Правило удаления квантора существования:
У $ ,
где у1, …уn - все свободные именные переменные выражения j, отличные от переменной х, а выражение j (х/σ у1, …уn) – результат подстановки в выражение j постоянной σ, отмеченной индексами у1, …уn вместо х. Заметим, что переменные у1, …уn, входящие в выражение σ у1, …уn рассматриваются в качестве свободных. Поэтому выражение σ у1, …уn можно подставлять в выражение j вместо переменной х тогда, и только тогда, когда эта переменная не находится в области действия квантора, связывающего переменные у1, …уп.
В качестве примеров вывода формул в натуральном узком исчислении предикатов рассмотрим вывод аксиом e),f), а также формул (37), (38).
е) " х F(х) ® F(у)
Доказательство:
1) "х F(х) {Допущение}
|
|
F(у) {У": 1}
f) F(у) ® $ х F(х)
Доказательство:
1) F(у) {Допущение}
$х F(х) {В$: 1}
Докажем формулу (37):
р ® " х (р Ú F(х))
Доказательство:
1) р {Допущение}
2) рÚ F(х) {ВД: 1}
"х рÚ F(х) {В": 2}
Докажем теперь формулу (38):
" х F(х) ® $ х F(х)
Доказательство:
1) "х F(х) {Допущение}
2) F(у) {У": 1}
$х F(х) {В$: 2}
Дата добавления: 2019-07-15; просмотров: 144; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!