Skip to main content
16 votes
Accepted

Incorporating Markov's principle in various proof assistants

There are different ways to implement Markov's principle, and they're not equivalent. I know of at least three techniques to implement MP. MP as a loop I personally find this to be a hack inherited ...
Pierre-Marie Pédrot's user avatar
11 votes
Accepted

What axioms do I need to search the naturals?

This is an axiom in itself, known as Markov's principle. A more compact but equivalent way to state this axiom is ...
Pierre-Marie Pédrot's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible