Questions tagged [markovs-principle]
In constructive mathematics, Markov's principle is the (classically trivial) statement that any infinite sequence of 0 and 1 that is not all 1s must have a 0 somewhere. (from nLab)
2
questions
9
votes
1
answer
564
views
What axioms do I need to search the naturals?
Theorem search
{P : nat -> Prop} (dec : forall n, {P n} + {~P n})
: ~~(exists n, P n) -> {n | P n}.
Admitted.
I don't think this is provable in Coq without ...
- 413
12
votes
1
answer
273
views
Incorporating Markov's principle in various proof assistants
The Markov's principle states that if a Turing machine does not run forever, then it halts. Equivalently, if I have a function $f : \mathbb N \to \mathrm{Bool}$, such that I have proved that $\neg\neg ...
- 3,480