title: Estensione conservativa
text: # Estensione conservativa
  
  In logica matematica, nell'ambito della teoria della dimostrazione, un'estensione conservativa di una teoria logica $T_1$ è una teoria $T_2$ tale che:
  
  * tutti i simboli di $T_1$ sono presenti anche in $T_2$
  * ogni teorema di $T_1$ è anche un teorema di $T_2$
  * ogni teorema di $T_2$ esprimibile usando soltanto il linguaggio di $T_1$ è un teorema di $T_1.$
  
  Nella teoria dei modelli, $T_2$ si dice un'estensione conservativa di $T_1$ se ogni modello di $T_1$ può essere esteso in un modello di $T_2.$ Tutte le estensioni conservative nel senso della teoria dei modelli lo sono anche nella definizione della teoria della dimostrazione.
  
  ## Proprietà
  
  Un'estensione conservativa di $T_1$ non può dimostrare nessun teorema che usi solo il linguaggio di $T_1$ e che $T_1$ non dimostri. Se $T_1$ è consistente, lo è anche la sua estensione conservativa $T_2.$ Questo permette di costruire teorie complesse rimanendo certi della loro consistenza, purché esse siano estensioni conservative di altre teorie sicuramente consistenti; gli algoritmi per dimostrazioni Isabelle e ACL2 usano questo metodo per espandere i loro linguaggi formali.
  
  Nella teoria delle ontologie, una teoria $T_1$ è un modulo di $T_2$ se e solo se $T_2$ è un'estensione conservativa di $T_1.$
  
  ## Generalizzazioni
  
  Dato un insieme Γ di formule in un linguaggio comune a $T_1$ e a $T_1,$ $T_2$ si dice Γ-conservativa rispetto a $T_1$ se ogni formula appartenente a Γ e dimostrabile in $T_2$ è anche dimostrabile in $T_1.$ Una teoria che estenda il linguaggio di un'altra, ma che non ne sia un'estensione conservativa, è chiamata estensione propria.
  
  ## Esempi
  
  * $ACA_0$ (un sottosistema dell'aritmetica del secondo ordine) è un'estensione conservativa dell'aritmetica di Peano (una teoria del primo ordine).
  * La teoria degli insiemi di Von Neumann-Bernays-Gödel è un'estensione conservativa della teoria degli insiemi di Zermelo-Fraenkel con l'assioma di scelta (ZFC).
  * La teoria degli insiemi interna è un'estensione conservativa della teoria degli insiemi di Zermelo-Fraenkel con l'assioma di scelta (ZFC)
  * Le estensioni per definizione sono conservative.
  * Le estensioni che aggiungono soltanto predicati o funzioni non trattate dalla prima teoria sono conservative.
  * $IΣ_1$ (un sottosistema dell'aritmetica di Peano comprendente solo gli $Σ^0_1-enunciati)$ è un'estensione $Π^0_2-conservativa$ dell'aritmetica primitiva ricorsiva (PRA).
  * ZFC è un'estensione $Π^1_3-conservativa$ di ZF, per il teorema di Shoenfield.
  * ZFC con l'ipotesi del continuo è un'estensione $Π^2_1-conservativa$ di ZFC.
  