Konservative Erweiterung - Conservative extension
In der mathematischen Logik ist eine konservative Erweiterung eine Supertheorie einer Theorie, die oft zum Beweisen von Theoremen geeignet ist , aber keine neuen Theoreme über die Sprache der ursprünglichen Theorie beweist. Ebenso ist eine nicht-konservative Erweiterung eine Supertheorie, die nicht konservativ ist und mehr Theoreme beweisen kann als das Original.
Formaler ausgedrückt ist eine Theorie eine ( beweistheoretisch ) konservative Erweiterung einer Theorie, wenn jeder Satz von ein Satz von ist und jeder Satz von in der Sprache von bereits ein Satz von ist .
Allgemeiner gesagt , wenn ein Satz ist Formeln in der gemeinsamen Sprache und , dann ist -conservative über , wenn jede Formel von beweisbar in auch beweisbar in ist .
Beachten Sie, dass eine konservative Erweiterung einer konsistenten Theorie konsistent ist. Wenn dem nicht so wäre, dann wäre nach dem Explosionsprinzip jede Formel in der Sprache von ein Satz von , also wäre jede Formel in der Sprache von ein Satz von , wäre also nicht konsistent. Konservative Erweiterungen bergen daher nicht das Risiko, neue Inkonsistenzen einzuführen. Dies kann auch als Methodik zum Schreiben und Strukturieren großer Theorien angesehen werden: Beginnen Sie mit einer Theorie, , von der bekannt ist (oder angenommen wird), dass sie konsistent ist, und bauen Sie sukzessive konservative Erweiterungen , , ... davon auf.
Vor kurzem konservative Erweiterungen wurden für die Definition einer Vorstellung von gebrauchtem Modul für Ontologien : wenn eine Ontologie als eine logische Theorie formalisiert ist, ein Subtheorie ein Modul ist , wenn die ganze Ontologie eine konservative Erweiterung des Subtheorie ist.
Eine Erweiterung, die nicht konservativ ist, kann eine echte Erweiterung genannt werden .
Beispiele
- ACA 0 (ein Subsystem der Arithmetik zweiter Ordnung ) ist eine konservative Erweiterung der Peano-Arithmetik erster Ordnung .
- Die Von Neumann-Bernays-Gödel-Mengentheorie ist eine konservative Erweiterung der Zermelo-Fraenkel-Mengentheorie mit dem Auswahlaxiom (ZFC).
- Die interne Mengenlehre ist eine konservative Erweiterung der Zermelo-Fraenkel-Mengentheorie mit dem Auswahlaxiom (ZFC).
- Erweiterungen per Definition sind konservativ.
- Erweiterungen durch uneingeschränkte Prädikats- oder Funktionssymbole sind konservativ.
- IΣ 1 (ein Subsystem der Peano-Arithmetik mit Induktion nur für Σ 0 1 -Formeln ) ist eine Π 0 2 -konservative Erweiterung der primitiven rekursiven Arithmetik (PRA).
- ZFC ist eine Σ 1 3 -konservative Erweiterung von ZF nach dem Absolutheitssatz von Shoenfield .
- ZFC mit der Kontinuumshypothese ist eine Π 2 1 -konservative Erweiterung von ZFC.
Modelltheoretische konservative Erweiterung
Mit modelltheoretischen Mitteln erhält man einen stärkeren Begriff: Eine Erweiterung einer Theorie ist modelltheoretisch konservativ, wenn und jedes Modell von zu einem Modell von erweitert werden kann . Jede modelltheoretische konservative Erweiterung ist auch eine (beweistheoretisch) konservative Erweiterung im obigen Sinne. Der modelltheoretische Begriff hat gegenüber dem beweistheoretischen den Vorteil, dass er nicht so stark von der vorliegenden Sprache abhängt; Andererseits ist es in der Regel schwieriger, modelltheoretische Konservativität zu begründen.