Понятие выводимости формулы из совокупности формул

Правило снятия двойного отрицания

Правило контрпозиции

Правило силлогизма

Правило сложного заключения

Правило одновременной подстановки

Пусть А – доказуемая формула; – переменные, а – любые формулы исчисления высказываний. Тогда результат одновременной подстановки в А вместо переменных формул соответственно является доказуемой формулой.

Схематично операция одновременной подстановки записывается в виде:

.

├ А

├

Это производное правило применяется к формулам вида

и формулируется таким образом:

Если формулы и доказуемы, то и формула доказуема.

Правило сложного заключения схематично записывается следующим образом:

.

├ ├ ,…,├ ;├

├

Если доказуемы формулы А → В и В → С, то доказуемаформула А → С. Схематическая запись силлогизма

.

├ А → В; ├ В → С

├ А → С

Если доказуема формула , то доказуема формула .

Схематическая запись контрпозиции

.

├ А → В_

├

а) Если доказуема формула , то доказуема формула .

б) Если доказуема формула , то доказуема формула .

Схематическая запись двойного отрицания

.

├ ├

├ ├

Пусть имеется конечная совокупность формул . Тогда формула выводима из совокупности (запись ├ ), если

а) либо ,

б) либо – доказуемая формула исчисления высказываний,

в) либо получается по правилу заключения из формул и , которые выводимы из совокупности .

Также можно сказать, что конечная совокупность формул есть вывод из , если для каждой формулы () этой совокупности

а) либо ,

б) либо доказуема,

в) либо получается по правилу заключения из формул и , которые находятся в выводе, предшествуя .

Дата добавления: 2017-02-01