Estensione conservativa
# 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.
