Principio di Markov

Da Wikipedia, l'enciclopedia libera.

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.

In logica predicativa, 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 tipizzato, 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, seppure l'enunciato forte li contraddica. Sebbene posse essere derivato per mezzo di ragionamenti intuizionistici, di realizzabilità e classici, il principio non è valido in senso construttivo secondo Bishop.[1]

Voci correlate[modifica | modifica wikitesto]

Note[modifica | modifica wikitesto]

  1. ^ (EN) Ulrich Kohlenbach, "On weak Markov's principle". Mathematical Logic Quarterly (2002), vol 48, issue S1, pp. 59–65.

Collegamenti esterni[modifica | modifica wikitesto]

matematica Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica