Markovin periaate

Markovin periaate on yksi rakentavan matematiikan logiikan perusperiaatteista, jonka Andrey Andreevich Markov (nuori) muotoili 1950 -luvun alussa . Se tunnetaan myös nimillä "Leningradin periaate" ja "rakentavan valinnan periaate" . Se on heikennetty versio kaksoisnegaation laista .

Periaate on muotoiltu seuraavasti:

Olkoon jollekin ominaisuudelle algoritmi , joka selvittää mille tahansa luonnolliselle luvulle , onko sillä ominaisuus . Jos oletus, että millään luonnollisella luvulla ei ole ominaisuutta, kumotaan , niin ominaisuuden kanssa on luonnollinen luku . ${\mathcal {Y}}$ $\mathfrak A$ $N$ $N$ ${\mathcal {Y}}$ ${\mathcal {Y}}$ ${\mathcal {Y}}$

Haluttu luku muodostetaan peräkkäin laskemalla luonnolliset luvut nollasta alkaen ja jokaisessa prosessin vaiheessa selvitetään algoritmin avulla, onko tarkasteltavalla luvulla ominaisuus . $\mathfrak A$ ${\mathcal {Y}}$

Käyttämällä konstruktiivisen matemaattisen logiikan muodollisia kieliä (esimerkiksi Markovin porrastettu semanttinen järjestelmä) Markovin periaate kirjoitetaan seuraavasti:

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