Skip to main content

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
13 votes
1 answer
412 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 ...
Trebor's user avatar
  • 4,015