Markov's Principle

A semi-constructive principle asserting that for a decidable predicate P on natural numbers, if it is impossible that no n satisfies P (¬¬∃n P(n)), then there exists n such that P(n); informally, double negation of existence collapses to existence for decidable predicates over the naturals.