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)

Filter by
Sorted by
Tagged with
9 votes
1 answer
531 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 ...
user avatar
  • 303
11 votes
1 answer
227 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 ...
user avatar
  • 2,256