title: Principio di Markov
text: # 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.
  
  