Principe de Markov

Un principe semi-constructif qui affirme que pour un prédicat décidables P sur les entiers naturels, si il est impossible qu’aucun n ne vérifie P (¬¬∃n P(n)), alors il existe un n tel que P(n) ; en pratique, la double négation d’une existence se réduit à une existence quand P est décidale sur les naturels.