Схема - аксиома
Cтраница 1
Схема аксиом, - i-правила и структурные правила всех четырех родов само-двойственны. [1]
Схемы аксиом 1 - г 10 п правило модус поненс задают интуиционистское исчисление высказывании. [2]
Схема аксиомы дистрибутивности К: L ( p - g) - ( Lp - Lg), что соответствует АЗ в нормальном модальном исчислении высказываний. [3]
Эта схема аксиом говорит о следующем. Если имеется некая формула ( р ( х у ] с двумя свободными переменными х у, и на некотором множестве А данная формула определяет ( х н у) - отображение, т.е. задает функцию, то область значений этого отображения ( функции) есть множество. [4]
Из схемы аксиом 6, применяя э-удал. Отсюда с помощью э-правил получаем теорему: Если Г, А - - i - i С и Г, В н - i - i С ( с фиксированными свободными переменными для А и В соответственно), то Г, - i - i ( AyB) I - - i - i С. Мы, таким образом, обосновали модифицированное правило разбора случаев, в котором формула случаев А VВ и заключение С дважды отрицаются. [5]
Все схемы аксиом, рассмотренные выше для II. [6]
 |
Дерево вывода для доказательства секвенции S. [7] |
Имеется единственная схема аксиом А А и ряд ПВ, записываемых с помощью горизонтальной черты с одной или двумя секвенциями ( точнее - секвенциальными схемами) над ней, которые называются посылками ПВ, и с одной секвенциальной схемой под чертой, называемой заключением ПВ. [8]
Система схем аксиом называется независимой, если для каждой схемы аксиом существует ее вариант, независимый от множества вариантов остальных схем аксиом. [9]
Роль схемы аксиом подстановки и аксиомы бесконечности мы установим немного позднее, когда уже будет накоплен некоторый опыт работы с множествами. [10]
Теорема 7.2.8. Схемы аксиом ИВ независимы. [11]
Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы, аксиом. [12]
Аксиомой ( или вариантом схемы аксиом) называется выражение, получаемое из данной схемы аксиом подстановкой вместо символов А, В и С конкретных формул. [13]
При задании исчисления с помощью схем аксиом и правил вывода естественно возникает вопрос о независимости этих схем аксиом и правил вывода. Схема аксиом называется независимой в исчислении, если хотя бы один ее частный случай не доказуем в исчислении без этой схемы. Правило вывода называют независимым в исчислении, если оно не является допустимым в исчислении без этого правила. Исчисление называется независимым, если все его схемы аксиом и правила вывода независимы. [14]
Так как в ИВ только одна схема аксиом, то она независима. Для доказательства независимости правил вывода достаточно для каждого правила а найти характеристическое свойство Д, которым обладают все секвенции, доказуемые при помощи правил, отличных от а, и которым некоторые доказуемые в ИВ секвенции не обладают. Мы ограничимся только формулировками характеристических свойств для правил 1 - 12, оставляя необходимую проверку читателю. [15]
Страницы: 1 2 3 4