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) The importance of conservative extensions for the foundations of mathematics, su cs.nyu.edu.