ПРОБЛЕМЫ АКСИОМ ИВ: 1) разрешимость; 2)непротиворечивость; 3) полнота; 4)независимость аксиом.
1) РАЗРЕШИМОСТЬ - заключается в том, что должен существовать алгоритм, позволяющий для любой заданной формулы ИВ определять, яв-ся она выводимой или нет. Для проверки разрешимости достаточно рассмотреть формулу ИВ как АВ и проверить, будет ли она тождественно истинной. Если в АВ она тождественно истинна, то она выводима в ИВ.
2) НЕПРОТИВОРЕЧИВОСТЬ - какова бы ни была формула а(альфа), никогда а и (not a) не могут быть одновременноиз аксиом этого исчисления с помощью указанных в нем правил ИВ непротиворечиво.
3) ПОЛНОТА - I. аксиоматич. исчисл. наз-ся полным в УЗКОМ смысле, если добавление к списку его аксиомлюбой невыводимой исчисл. форм. в кач-ве новой аксиомы приводит к противореичвому исчислению. ТЕОРЕМА: ИВ полное в узком смысле. II. аксиоматич. исчисление называется полным в ШИРОКОМ смысле, если любая тождественно истинная формула в нем доказуема (выводима).
4) НЕЗАВИСИМОСТЬ аксиом - заключается в невыводимости аксиомы из ост. аксиом по правилам вывода в данной системе. ТЕОРЕМА: Система аксиом ИВ независима.
