Estensione conservativa

In logica matematica, nell'ambito della teoria della dimostrazione, un'estensione conservativa di una teoria logica T1 è una teoria T2 tale che:

  • tutti i simboli di T1 sono presenti anche in T2
  • ogni teorema di T1 è anche un teorema di T2
  • ogni teorema di T2 esprimibile usando soltanto il linguaggio di T1 è un teorema di T1.

Nella teoria dei modelli, T2 si dice un'estensione conservativa di T1 se ogni modello di T1 può essere esteso in un modello di T2. Tutte le estensioni conservative nel senso della teoria dei modelli lo sono anche nella definizione della teoria della dimostrazione.

Un'estensione conservativa di T1 non può dimostrare nessun teorema che usi solo il linguaggio di T1 e che T1 non dimostri. Se T1 è consistente, lo è anche la sua estensione conservativa T2. 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 T1 è un modulo di T2 se e solo se T2 è un'estensione conservativa di T1.

Generalizzazioni

[modifica | modifica wikitesto]

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

Voci correlate

[modifica | modifica wikitesto]

Collegamenti esterni

[modifica | modifica wikitesto]
  Portale Matematica: accedi alle voci di Wikipedia che trattano di Matematica