Математическая логика и теория алгоритмов

§12. Дру гие аксиоматизации исчисления высказываний В предыдущих параграфах рассматривался пример формальной аксиоматической теории - исчисление высказываний (теория L), кото­ рая была задана множеством символов, формул, аксиом и правил вы­ вода. Теперь рассмотрим некоторую формализованную теориюС. Для задания формализованной теории необходимо задать ее символы, формулы (правильно построенные выражения) и из множества фор­ мул выделить подмножество, элементы которого считаются «истин­ ными» формулами. Пусть формализованная теория С задана так, что: 1) алфавиты теорий I и С совпадают, т.е. алфавитом для С явля­ ется следующее множество символов.- 1, =>,), (,Ai,A2, 2) множества формул I и С совпадают {Ф^^Фс , где Ф1{Фс ) - мно­ жество формул теории L{C)). Таким образом, формулой в С является всякая пропозициональная форма, построенная из букв А\, AJ, — с помощью связок 1 и =>; 3) "истинными" формулами в теории С считаются те и только те формулы теории С, которые являются тавтологиями. Пусть Vq обо­ значает множество "истинных" формул теории С. В исчислении высказываний было задано Г/, - множество теорем (с помощью аксиом А\-АЪ и правила вывода MP). При этом теорема­ ми в I оказались те, и только те формулы из L, которые являются тавтологиями. Следовательно, множество теорем формальной теории L совпадает с множеством "истинных" формул формализованной тео­ р ии С: TI=VC. Итак, формальная теория L оказалась построенной таким обра­ зом, что ее множество теорем (Г/,) в точности совпадает с множеством "истинных" формул (VC ) формализованной теории С. Из полноты в узком смысле теории L следует, что всякая по­ пытка расширить множество Т/^ приводит к противоречивой теории, поэтому нельзя к А1-АЗ добавите недоказуемую из них формулу, не приходя при этом к противоречию. Естественно выяснить, можно ли. 167