Markov's principle

Content sourced from Wikipedia, licensed under CC BY-SA 3.0.

Markov's principle, also called the Leningrad principle, is a rule about turning a certain kind of negative statement into an existence claim, but only for predicates that are decidable.

What it says
- If P is a decidable predicate on the natural numbers, and it is not the case that P(n) is false for every n, then there exists a natural number n for which P(n) is true.
- In symbols: if not not exists n P(n) then exists n P(n), assuming P is decidable.

Classical vs constructive
- In classical logic this is always true.
- In constructive (intuitionistic) logic it is not provable in general, though many specific instances are.

Intuition from computability
- A simple reading: if a program is impossible to prove to never terminate, then there must be some input on which it does terminate.
- Equivalently: if a set and its complement can both be listed by an algorithm (are computably enumerable), then the set is decidable.

Weak form and limits
- There is a weaker version called the weak Markov principle, focused on the positivity of real numbers. It fits with some constructive viewpoints, but the full principle is not accepted in all constructive frameworks.
- The strong form has stronger consequences and is not generally accepted in all forms of constructive mathematics.

Relation to math and logic
- Markov's principle connects classical and constructive ideas about existence and computation.
- It has several equivalent formulations in arithmetic and analysis, especially when paired with ideas about realizability and computability.
- Overall, it helps clarify what kinds of existence statements can be justified using only constructive (algorithmic) reasoning.