29 Большая пятерка арифметик

Немного обратной математики. Рассматриваем 3 основных и чуть-чуть 2 дополнительных формализма арифметики: 1. RCA0 2. WKL0 3. ACA0 4. ATR0 5. Π_1^1-CA Сравнение первых трех по их умению доказывать известные теоремы анализа, такие как: - лемма о промежуточном значении, - лемма Гейне-Бореля, - признак сходимости Коши, - теорема Больцано-Вейерштрасса, - лемма Кёнига, - теорема Гёделя о полноте.