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

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à

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

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.

Voci correlate

• Tesi di Church-Turing

Collegamenti esterni

• (EN) Constructive Mathematics (Stanford Encyclopedia of Philosophy), su plato.stanford.edu.