Контрольная работа: Исчисления предикатов и их применение в логическом умозаключении
Для записи схем правил введения и удаления кванторов общности и существования можно пользоваться символом j (х/ w ), обозначающем выражение, полученное изj подстановкой вместо именной переменной х выражения w при выполнении следующих условий:
1) В выражении j замена переменной х производится лишь в тех местах, где она свободна. Если х входит в j несколько раз, то столько же раз она заменяется выражением w .
2) Если в j переменная х находится в области действия квантора, связывающую предметную переменную z , то вместо х не подставляется выражение содержащее z в качестве свободной переменной. Короче говоря, подстановку следует производить так, чтобы свободные переменные подставляемого выражения не оказались связанными в выражении, полученном в результате подстановки.
Если это правило нарушается, то можно получить ложное высказывание. Так, в выражении $ m (m>n) переменная m связана, а переменная n свободна. Если мы вместо n подставим m+1 , то получим ложное выражение: $ m (m> m+1).
Правило удаление квантора общности:
У " .
Примером рассуждения по правилу У":
.
Правило введения квантора общности:
В " применяется лишь при условии, что переменная х не входит в качестве свободной в допущение косвенного доказательства.
Примером рассуждения по правилу
В " : .
Правило введение квантора существования :
В $ .
Примером рассуждения по правилу В$:
2 – четное и простое число
$ х (х – четное и простое).
Правило удаления квантора существования:
У $ ,
где у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}