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.

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

.

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

Il principio è equivalente, in HA, a:

con una funzione ricorsiva totale sui numeri naturali.

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

  • Per ogni numero reale , se è contraddittorio che sia uguale a 0, allora esiste tale che , spesso espresso dicendo che è costruttivamente diverso da 0.
  • Per ogni numero reale , se è contraddittorio che sia uguale a 0, allora esiste un tale che .

Realizzabilità[modifica | modifica wikitesto]

Il principio di Markov può essere giustificato tramite la realizzabilità: un realizzatore è una ricerca illimitata che controlla successivamente se sia vero. Dato che 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 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:

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 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