Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Ai,A2,...,An (4.1) из гипотез G. Если некоторая формула Ai принадлежит G, то, очевидно, Ai е F. Следовательно, вывод (4.1) формулы А является выводом формулы А из гипотез F. Что и требовалось доказать. 2. G \- А тогда и только тогда, когда в G существует конечное подмножество //такое, что Н \-А. Доказательство следует из определения вывода. 3. Пусть G |- ^ и каждая формула В, принадлежащая G, выводима из некоторого множества формул F, тогда F \-А. Доказательство. Пусть ^4 имеет вывод Ai,A2,...,An (4.2) из гипотез G. По определению вывода некоторые А^ из (4.2) могут принадлежать G, но каждая формула из G имеет вывод из F. Заменим в (4.2) все Ai, принадлежащие G, выводом А^ из F. В результате получим последовательность формул: которая уже является выводом А из F. Что и требовалось доказать. Как частный случай п.З имеем: 3\Е СЛИУ 4 \-ВиВ |- С , ТО ^ |- С . 4. EcлиG ,Y4 \-В H G |-^, TO G \-В. Доказательство. Пусть В имеет вывод Bi,B2,...,Bn (4.3) из гипотез G и а формула^ имеет вывод A],A2,...,Afn (4.4) из гипотез G. В выводе (3) формулы В некоторые из В( могут быть равны А. Заменим такие Д последовательностью (4). В результате получим последовательность формул f f с ^2J - •• которая является выводом для В из гипотез G. Что и требовалось доказать. Первые понятия, с которых начинается какая- нибудь наука, должны быть ясны и приведены к самому меньшему числу. Тогда только они могут служить прочным и достаточным основанием учения. Н. Лобачевский § 7. Исчисление высказываний (теория L) В качестве первого примера формальной аксиоматической теории рассмотрим исчисление высказываний - теорию L. 1. Символами теории L являются: и буквы Ai с целыми положительными числами в качестве индексов: А1,А2,Аз,--- Символы— б у д е м 108