С помощью аксиом Coq действительных чисел completeness и total_order_T, используя ту же технику, что и в стандартной лемме lib Un_cv_crit_lub, мне удалось доказать
Lemma NatForallDec : forall (f : nat -> bool),
{ forall n:nat, f n = false } + { ~forall n:nat, f n = false }.
и
Lemma NatForallDecIncr : forall (f : nat -> bool),
(forall n m:nat, f n = true -> n <= m -> f m = true)
-> { forall n:nat, f n = false } + { exists n:nat, f n = true }.
Это беспокоит, потому что это похоже на своего рода оракула: если суждение f о натуральных числах разрешимо для каждого числа, то бесконечное соединение f также становится разрешимым. Таким образом, аксиомы действительных чисел говорят, что мы можем извлечь алгоритм, который принимает бесконечное число решений за конечное время ...
Существуют ли другие примеры исключенного среднего, которые следуют из аксиом вещественных чисел и имеют мало общего с действительными числами?
А что касается действительных чисел, может ли наименьшая верхняя граница быть реализована как сходящаяся последовательность?
Definition Cv_lub (A : R -> Prop) (l : R) (n : nat) :
is_lub A l
-> { x : R | A x /\ (l - x <= 1 / INR n)%R }.