Понятие выводимости формул из совокупности формул.
Будем рассматривать конечную совокупность формул Н={А1,А2,…,Аn}.
Определение формулы, выводимой из совокупности Н.
1)Всякая формула Аi ,является формулой, выводимой из Н.
2) Всякая доказуемая формула выводима из Н.
3) Если формулы С и С→В выводимы из совокупности Н, то формула В также выводима из Н.
Если некоторая формула В выводима из совокупности Н, то это записывают так: Н├В.
Нетрудно видеть, что класс формул, выводимых из совокупности Н, совпадает с классом доказуемых формул в случае, когда совокупность Н содержит только доказуемые формулы, и в случае, когда Н пуста.
Если же совокупность формул Н содержит хотя бы одну не доказуемую формулу, то класс формул, выводимых из Н, шире класса доказуемых формул.
Пример.
Доказать, что из совокупности формул Н={А ,В} выводима формула .
Так как А и В , то по определению выводимой формулы
Н├А, (1)
Н├В. (2)
Возьмемксиомы и , и выполним подстановки и .
В результате получим доказуемые формулы, которые выводимы из Н по определению выводимой формулы, т. е.
Н├(А→А)→((А→В)→(А )), (3)
Н├В→(А→В), (4)
Так как формула А→А доказуема, то Н├А→А. (5)
Из формул (5) и (3) по правилу заключения получаем: Н├(А→В)→(А )). (6)
Из формулы (2) и (4) по правилу заключения получаем: Н├А→В. (7)
Из формул (7) и (6) по правилу заключения получаем: Н├А . (8)
И, наконец, из формул (1) и (8) получаем:
Н├ (9)
Ясно, что при доказательстве выводимости формулы из совокупности формул можно пользоваться не только основным правилом заключения, но и правилом сложного заключения. Тогда, пользуясь этим правилом , предложение (9) можно получить из предложений (5), (7), (1) и (3).
Понятие вывода.
Определение.
Выводом из конечной совокупности формул Н называется всякая конечная последовательность формул В1,В2,…,Вк, всякий член которой удовлетворяет одному из следующих трех условий:
1) он является одной из формул совокупности Н,
2) он является доказуемой формулой,
3) он получается по правилу заключения из двух любых предшествующих членов последовательности В1,В2,…,Вк.
Как было показано в предыдущем примере, выводом из совокупности формул Н={А,В} является конечная последовательность формул:
А, В, (А→А)→((А→В)→(А )), (А→В), А→А, (А→В)→(А )), А→В, А , . (см. формулы 1,2,3,7,5,6,8).
Если же здесь воспользоваться правилом сложного заключения , то вывод можно записать так:
А, В, (А→А)→((А→В)→(А )), В→(А→В), А→А, А→В, . (см. формулы 5, 7, 1, 3).
Из определения выводимой формулы и вывода из совокупности формул следуют очевидные свойства вывода:
1)Всякий начальный отрезок вывода из совокупности Н есть вывод из Н.
2)Если между двумя соседними членами вывода из Н (или в начале или в конце его) вставить некоторый вывод из Н, то полученная новая последовательность формул будет также выводом из Н.
3)Всякий член вывода из совокупности Н является формулой, выводимой из Н. Всякий вывод из Н является выводом его последней формулы.
4)Если (включено), то всякий вывод из Н является выводом из W.
5)Для того, чтобы формула В была выводима из совокупности Н, необходимо и достаточно, чтобы существовал вывод этой формулы из Н.
Дата добавления: 2022-05-27; просмотров: 108;