Slutsky equation: Difference between revisions
en>Thisisausernamelikenoother mNo edit summary |
en>Addbot m Bot: Migrating 10 interwiki links, now provided by Wikidata on d:q431721 (Report Errors) |
||
Line 1: | Line 1: | ||
In [[mathematical logic]], a [[logical theory]] <math>T_2</math> is a ([[Proof theory|proof theoretic]]) '''conservative extension''' of a theory <math>T_1</math> if the language of <math>T_2</math> extends the language of <math>T_1</math>; every theorem of <math>T_1</math> is a theorem of <math>T_2</math>; and any theorem of <math>T_2</math> that is in the language of <math>T_1</math> is already a theorem of <math>T_1</math>. | |||
More generally, if Γ is a set of formulas in the common language of <math>T_1</math> and <math>T_2</math>, then <math>T_2</math> is '''Γ-conservative''' over <math>T_1</math> if every formula from Γ provable in <math>T_2</math> is also provable in <math>T_1</math>. | |||
To put it informally, the new theory may possibly be more convenient for proving [[theorem]]s, but it proves no new theorems about the language of the old theory. | |||
Note that a conservative extension of a [[consistent]] theory is consistent. Hence, conservative extensions do not bear the risk of introducing new inconsistencies. This can also be seen as a [[methodology]] for writing and structuring large theories: start with a theory, <math>T_0</math>, that is known (or assumed) to be consistent, and successively build conservative extensions <math>T_1</math>, <math>T_2</math>, ... of it. | |||
The theorem provers [[Isabelle (theorem prover)|Isabelle]] and [[ACL2]] adopt this methodology by providing a language for conservative extensions by definition. | |||
Recently, conservative extensions have been used for defining a notion of [[ontology modularization|module]] for [[Ontology (computer science)|ontologies]]: if an ontology is formalized as a logical theory, a subtheory is a module if the whole ontology is a conservative extension of the subtheory. | |||
An extension which is not conservative may be called a '''proper extension'''. | |||
==Examples== | |||
* ACA<sub>0</sub> (a subsystem of [[second-order arithmetic]]) is a conservative extension of first-order [[Peano arithmetic]]. | |||
* [[Von Neumann–Bernays–Gödel set theory]] is a conservative extension of [[Zermelo–Fraenkel set theory]] with the [[axiom of choice]] (ZFC). | |||
* [[Internal set theory]] is a conservative extension of [[Zermelo–Fraenkel set theory]] with the [[axiom of choice]] (ZFC). | |||
* [[Extension by definitions|Extensions by definitions]] are conservative. | |||
* Extensions by unconstrained predicate or function symbols are conservative. | |||
* IΣ<sub>1</sub> (a subsystem of Peano arithmetic with induction only for [[arithmetical hierarchy|Σ<sup>0</sup><sub style="margin-left:-0.65em">1</sub>-formulas]]) is a Π<sup>0</sup><sub style="margin-left:-0.65em">2</sub>-conservative extension of the [[primitive recursive arithmetic]] (PRA). | |||
* ZFC is a [[analytical hierarchy|Π<sup>1</sup><sub style="margin-left:-0.65em">3</sub>]]-conservative extension of ZF by [[absoluteness (mathematical logic)|Shoenfield's absoluteness theorem]]. | |||
* ZFC with the [[continuum hypothesis]] is a Π<sup>2</sup><sub style="margin-left:-0.65em">1</sub>-conservative extension of ZFC. | |||
==Model-theoretic conservative extension== | |||
With [[Model theory|model-theoretic]] means, a stronger notion is obtained: an extension <math>T_2</math> of a theory <math>T_1</math> is '''model-theoretically conservative''' if every model of <math>T_1</math> can be expanded to a model of <math>T_2</math>. It is straightforward to see that each model-theoretic conservative extension also is a (proof-theoretic) conservative extension in the above sense. The model theoretic notion has the advantage over the proof theoretic one that it does not depend so much on the language at hand; on the other hand, it is usually harder to establish model theoretic conservativity. | |||
{{Further2|[[Conservativity theorem]]}} | |||
<!--* [[relative consistency]]--> | |||
==External links== | |||
*[http://www.cs.nyu.edu/pipermail/fom/1998-October/002306.html The importance of conservative extensions for the foundations of mathematics] | |||
[[Category:Proof theory]] | |||
[[Category:Model theory]] |
Revision as of 00:26, 27 February 2013
In mathematical logic, a logical theory is a (proof theoretic) conservative extension of a theory if the language of extends the language of ; every theorem of is a theorem of ; and any theorem of that is in the language of is already a theorem of .
More generally, if Γ is a set of formulas in the common language of and , then is Γ-conservative over if every formula from Γ provable in is also provable in .
To put it informally, the new theory may possibly be more convenient for proving theorems, but it proves no new theorems about the language of the old theory.
Note that a conservative extension of a consistent theory is consistent. Hence, conservative extensions do not bear the risk of introducing new inconsistencies. This can also be seen as a methodology for writing and structuring large theories: start with a theory, , that is known (or assumed) to be consistent, and successively build conservative extensions , , ... of it.
The theorem provers Isabelle and ACL2 adopt this methodology by providing a language for conservative extensions by definition.
Recently, conservative extensions have been used for defining a notion of module for ontologies: if an ontology is formalized as a logical theory, a subtheory is a module if the whole ontology is a conservative extension of the subtheory.
An extension which is not conservative may be called a proper extension.
Examples
- ACA0 (a subsystem of second-order arithmetic) is a conservative extension of first-order Peano arithmetic.
- Von Neumann–Bernays–Gödel set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice (ZFC).
- Internal set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice (ZFC).
- Extensions by definitions are conservative.
- Extensions by unconstrained predicate or function symbols are conservative.
- IΣ1 (a subsystem of Peano arithmetic with induction only for Σ01-formulas) is a Π02-conservative extension of the primitive recursive arithmetic (PRA).
- ZFC is a Π13-conservative extension of ZF by Shoenfield's absoluteness theorem.
- ZFC with the continuum hypothesis is a Π21-conservative extension of ZFC.
Model-theoretic conservative extension
With model-theoretic means, a stronger notion is obtained: an extension of a theory is model-theoretically conservative if every model of can be expanded to a model of . It is straightforward to see that each model-theoretic conservative extension also is a (proof-theoretic) conservative extension in the above sense. The model theoretic notion has the advantage over the proof theoretic one that it does not depend so much on the language at hand; on the other hand, it is usually harder to establish model theoretic conservativity.