Principio di Markov

Il Principio di Markov, che deve il nome ad Andrej Andreevič Markov, è una tautologia della logica classica che non è intuizionisticamente valida ma può essere giustificata costruttivamente.

Ci sono diverse formulazioni equivalenti del principio di Markov.

Enunciato del principio[modifica | modifica wikitesto]

Nel linguaggio della teoria della calcolabilità, il principio di Markov è l'espressione formale dell'affermazione per cui, se è impossibile che un algoritmo non termini, allora termina. Ciò è equivalente all'affermare che se un insieme, assieme al suo complemento, è ricorsivamente enumerabile, allora l'insieme è ricorsivo.

Nella logica al primo ordine, se $P$ è un predicato sui numeri naturali, si può esprimere come:

(\forall n(P(n)\vee \neg P(n)))\wedge (\neg \forall n\neg P(n))\rightarrow (\exists n\;P(n))

.

Cioè, se $P$ è decidibile, e non può essere falso per ogni numero naturale $n$ , allora è vero per qualche $n$ . (In generale, un predicato $P$ su qualche dominio si dice "decidibile" se per ogni $x$ nel dominio, $P(x)$ è vero o $P(x)$ non è vero, e ciò non sempre vale costruttivamente).

Il principio è equivalente, in HA, a:

\neg \neg \exists n\;f(n)=0\rightarrow \exists n\;f(n)=0,

con $f$ una funzione ricorsiva totale sui numeri naturali.

Nel linguaggio dell'analisi reale, il principio è equivalente ai seguenti:

Per ogni numero reale $x$ , se è contraddittorio che $x$ sia uguale a 0, allora esiste $y\in \mathbb {Q}$ tale che $0<y<|x|$ , spesso espresso dicendo che $x$ è costruttivamente diverso da 0.
Per ogni numero reale $x$ , se è contraddittorio che $x$ sia uguale a 0, allora esiste un $y\in \mathbb {R}$ tale che $x\cdot y=1$ .

Realizzabilità[modifica | modifica wikitesto]

Il principio di Markov può essere giustificato tramite la realizzabilità: un realizzatore è una ricerca illimitata che controlla successivamente se $P(0),P(1),P(2),\dots$ sia vero. Dato che $P$ non è sempre falsa, la ricerca non può continuare all'infinito. Per la logica classica si conclude che la ricerca termina su un valore per cui $P$ vale.

La realizzabilità modificata non giustifica il principio di Markov, anche se si usa la logica classica nella meta-teoria: non c'è nessun realizzatore nel linguaggio del lambda calcolo tipato, dato che non è Turing completo e non si possono definire cicli arbitrari.

Principio di Markov debole[modifica | modifica wikitesto]

Una forma più debole del principio di Markov può essere espressa nel linguaggio dell'analisi come:

\forall x\in \mathbb {R} \ (\forall y\in \mathbb {R} \ \neg \neg (0<y)\vee \neg \neg (y<x))\to 0<x.

Questa forma può essere giustificata dai principi di continuità di Brouwer, anche se invece l'enunciato forte li contraddice. Sebbene possa essere derivato per mezzo di ragionamenti intuizionistici, di realizzabilità e classici, il principio non è valido in senso costruttivo secondo Bishop.^[1]