Markovův princip

Markovův princip je jedním ze základních principů logiky konstruktivní matematiky , který formuloval na počátku 50. let Andrej Andrejevič Markov (junior) . Je také známý pod názvy „Leningradský princip“ a „princip konstruktivního výběru“ . Je to oslabená verze zákona dvojí negace .

Princip je formulován takto:

Nechť existuje algoritmus pro nějakou vlastnost , který zjistí pro libovolné přirozené číslo , zda má vlastnost . Pokud je vyvrácen předpoklad, že žádné přirozené číslo nemá vlastnost , pak existuje přirozené číslo s vlastností . ${\mathcal {Y}}$ $\mathfrak A$ $N$ $N$ ${\mathcal {Y}}$ ${\mathcal {Y}}$ ${\mathcal {Y}}$

Způsob, jak zkonstruovat požadované číslo, je sekvenční výčet přirozených čísel počínaje nulou a v každém kroku procesu se pomocí algoritmu zjišťuje, zda uvažované číslo má vlastnost . $\mathfrak A$ ${\mathcal {Y}}$

Pomocí formálních jazyků konstruktivní matematické logiky (například Markovův stupňovitý sémantický systém) je Markovův princip napsán takto:

((\forall X(D\lor (\neg D)))\supset ((\neg (\neg (\exists XD)))\supset (\exists XD)))