Аннотация:
Результаты о том, что доказательства некоторых утверждений в одной системе доказательств могут быть существенно короче, чем в другой, часто называются теоремами об ускорении. Первый результат такого рода был получен К. Гёделем еще в 1936 году. Мы рассматриваем различные аксиоматизации арифметики Пресбургера - элементарной теория натурального ряда со сложением. Установлено, что для некоторых пар аксиоматизаций имеет место результат об ускорении с экспоненциальной нижней оценкой и конечной итерацией экспоненты в качестве верхней оценки.
|
