Extensie conservatoare
În logica matematică , în contextul teoriei dovezilor , o extensie conservatoare a unei teorii logice T 1 este o teorie T 2 astfel încât:
- toate simbolurile lui T 1 sunt prezente și în T 2
- fiecare teoremă a lui T 1 este, de asemenea, o teoremă a lui T 2
- orice teoremă a lui T 2 exprimabilă folosind doar limbajul lui T 1 este o teoremă a lui T 1 .
În teoria modelelor, T 2 se spune că este o extensie conservatoare a T 1 dacă orice model de T 1 poate fi extins într-un model de T 2 . Toate extensiile conservatoare în sensul teoriei modelelor sunt, de asemenea, conservatoare în definiția teoriei dovezilor.
Proprietate
O extensie conservatoare a lui T 1 nu poate dovedi vreo teoremă care utilizează doar limbajul lui T 1 și pe care T 1 nu o dovedește. Dacă T 1 este consecvent , la fel este și extensia sa conservatoare T 2 . Acest lucru permite construirea unor teorii complexe, rămânând însă sigur de consistența lor, cu condiția să fie extensii conservatoare ale altor teorii cu siguranță consistente; algoritmii de probă Isabelle și ACL2 folosesc această metodă pentru a-și extinde limbajele formale.
În teoria ontologiei , o teorie T 1 este un modul al lui T 2 dacă și numai dacă T 2 este o extensie conservatoare a lui T 1 .
Generalizări
Având în vedere un set Γ de formule într-un limbaj comun lui T 1 și T 1 , se spune că T 2 este Γ-conservator față de T 1 dacă fiecare formulă aparținând lui Γ și demonstrabilă în T 2 este, de asemenea, demonstrabilă în T 1 .
O teorie care extinde limbajul altuia, dar care nu este o extensie conservatoare a acesteia, se numește propria extensie .
Exemple
- ACA 0 (un subsistem de aritmetică de ordinul doi ) este o extensie conservatoare a aritmeticii lui Peano (o teorie de ordinul întâi ).
- Teoria mulțimilor Von Neumann-Bernays-Gödel este o extensie conservatoare a teoriei mulțimilor Zermelo-Fraenkel cu axioma de alegere (ZFC).
- Teoria internă a mulțimilor este o extensie conservatoare a teoriei mulțimilor Zermelo-Fraenkel cu axioma de alegere (ZFC)
- Extensiile sunt, prin definiție, conservatoare.
- Extensiile care adaugă numai predicate sau funcții care nu sunt acoperite de prima teorie sunt conservatoare.
- IΣ 1 (un subsistem de aritmetică Peano care cuprinde doar Σ 0 1 - enunțuri ) este o extensie conservatoare Π 0 2 -conservator al aritmeticii recursive primitive (PRA).
- ZFC este o extensie conservatoare de Π 1 3 a ZF, prin teorema lui Shoenfield .
- ZFC cu ipoteza continuumului este o extensie conservativă Π 2 1 a ZFC.
Elemente conexe
linkuri externe
- ( EN ) Importanța extensiilor conservatoare pentru fundamentele matematicii , su cs.nyu.edu .
