Выдержка из книги
Драгалин А.Г.
Конструктивная теория доказательств и нестандартный анализ
Классическая формальная арифметика FA есть по определению система FA ( 7) для случая, когда множество U пусто. Аксиома 4) при этом, естественно, исключается из списка ее нелогических аксиом, а в аксиомах 7) употребляются лишь описания, не содержащие аргументов для функций. Напомним, что кванторы для переменных по функциям в языке A ( Z7) отсутствуют.
