Estensione conservativa

In logica matematica, nell'ambito della teoria della dimostrazione, un'estensione conservativa di una teoria logica T₁ è una teoria T₂ tale che:

tutti i simboli di T₁ sono presenti anche in T₂
ogni teorema di T₁ è anche un teorema di T₂
ogni teorema di T₂ esprimibile usando soltanto il linguaggio di T₁ è un teorema di T₁.

Nella teoria dei modelli, T₂ si dice un'estensione conservativa di T₁ se ogni modello di T₁ può essere esteso in un modello di T₂. 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₁ non può dimostrare nessun teorema che usi solo il linguaggio di T₁ e che T₁ non dimostri. Se T₁ è consistente, lo è anche la sua estensione conservativa T₂. 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₁ è un modulo di T₂ se e solo se T₂ è un'estensione conservativa di T₁.

Generalizzazioni

Dato un insieme Γ di formule in un linguaggio comune a T₁ e a T₁, T₂ si dice Γ-conservativa rispetto a T₁ se ogni formula appartenente a Γ e dimostrabile in T₂ è anche dimostrabile in T₁.
Una teoria che estenda il linguaggio di un'altra, ma che non ne sia un'estensione conservativa, è chiamata estensione propria.

Esempi

ACA₀ (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Σ₁ (un sottosistema dell'aritmetica di Peano comprendente solo gli Σ⁰₁-enunciati) è un'estensione Π⁰₂-conservativa dell'aritmetica primitiva ricorsiva (PRA).
ZFC è un'estensione Π¹₃-conservativa di ZF, per il teorema di Shoenfield.
ZFC con l'ipotesi del continuo è un'estensione Π²₁-conservativa di ZFC.

Voci correlate

Teorema della conservatività
Teoria della dimostrazione
Teoria dei modelli

Collegamenti esterni

(EN) conservative extension, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
(EN) The importance of conservative extensions for the foundations of mathematics, su cs.nyu.edu.