Математическая логика
жүктеу/скачать 0.93 Mb.
|
| B1 = A
B2 = - аксиома 1 B3 = B = - получено из B1 и B2 в силу правила заключения. Заметим, что если посылки являются аксиомами или теоремами исчисления высказываний, то класс выводимых из них формул совпадает с классом всех истинных формул, выводимых из любой системы посылок. Выводимость формулы из системы посылок отличается от доказательства теоремы в исчислении высказываний тем, что здесь допускается использование только правила заключения. Но при выводе формулы разрешается использовать любую теорему исчисления высказываний, для получения которой может применяться правило подстановки. Из каждой формулы U с помощью правила подстановки, производящего замену высказывательных переменных в этой формуле любыми формулами, может быть получено бесконечное множество формул. Это множество формул называется схемой формулы U и обозначается выражением, полученным заменой в формуле U всех входящих в нее высказывательных переменных метасимволами . Например, из формулы возникает схема формул . (5) Этой схеме принадлежит формула . Новые схемы формул можно получить заменой ее метасимволов схемами формул. Эти схемы выделяют некоторое подмножество формул из множества формул, принадлежащих исходной схеме. Например, из схемы (5) можно получить схему формул . (6) Формула принадлежит как схеме формул (5), так и (6). Для формул, являющимися аксиомами или теоремами, схемы формул называются соответственно схемами аксиом или схемами теорем. Схемами аксиом являются: Таким образом, при выводе формулы из системы посылок (которая может быть и пустой) будут использоваться схемы аксиом и правило заключения, правило подстановки применяется неявно в схеме аксиом. Наряду с правилом заключения, мы будем использовать и другие правила образования истинных и выводимых формул. Эти правила являются производными от основных и используются для сокращения многократного применения основных правил. Перечислим основные из производных правил вывода. Как и прежде, метасимволы являются произвольными формулами, а через T обозначим конечное множество формул (возможно пустое). Правило повторения посылки. жүктеу/скачать 0.93 Mb. Достарыңызбен бөлісу:
|