Из чего вытекает закон исключенного третьего?

Рассматриваются теории, содержащие гейтинговскую арифметику и аксиому существования функций 1.4. Обычным образом задается элементарная теория вещественных чисел (см., например, [4]). Доказано, что закон исключенного третьего (как схема для арифметических формул) следует из любого из утверждений: равенство вещественных чисел разрешимо; всякая неубывающая ограниченная сверху последовательность сходится; всякая частичная функция может быть продолжена до всюду определенной. Следующие три теоремы эквивалентны при использовании принципа Маркова: (а) разрешимость равенства, (б) упомянутая выше теорема о неубывающей последовательности, (в) теорема Больцано–Вейерштрасса о том, что всякая ограниченная последовательность имеет сходящуюся подпоследовательность. Теорема Лебега о том, что всякое счетное открытое покрытие [0,1] содержит конечное подпокрытие, следует из каждой из теорем (а)–(в), но является более слабой, чем любая из них.