Implementation of mathematics in set theory: Difference between revisions

Revision as of 22:05, 12 August 2014

Revision as of 15:33, 14 August 2014

Line 15:

Expressions definable in set-builder notation make sense in both ZFC and NFU: it may be that both theories prove that a given definition succeeds, or that neither do (the expression <math>\{x \mid x\not\in x\}</math> fails to refer to anything in ''any'' set theory with classical logic; in class theories like [[Von Neumann–Bernays–Gödel set theory|NBG]] this notation does refer to a class, but it is defined differently), or that one does and the other doesn't. Further, an object defined in the same way in ZFC and NFU may turn out to have different properties in the two theories (or there may be a difference in what can be proved where there is no provable difference between their properties).

Further, set theory imports concepts from other branches of mathematics (in intention, ''all'' branches of mathematics). In some cases, there are different ways to import the concepts into ZFC and NFU. For example, the usual definition of the first infinite ordinal <math>\omega</math> in ZFC is not suitable for NFU because the object (defined in purely set theoretical language as the set of all finite von Neumann ordinals) cannot be shown to exist in NFU. The usual definition of <math>\omega</math> in NFU is defined (in purely set theoretical language) as the set of all infinite well-orderings all of whose proper initial segments are finite, an object which can be shown not to exist in ZFC. In the case of such imported objects, there may be different definitions, one for use in ZFC and related theories, and one for use in NFU and related theories. For such "implementations" of imported mathematical concepts to make sense, it is necessary to be able to show that the two parallel interpretations have the expected properties: for example, the implementations of the natural numbers in ZFC and NFU are different, but both are implementations of the same mathematical structure, because both include definitions for all the primitives of Peano arithmetic and satisfy (the translations of) the Peano axioms. It is then possible to compare what happens in the two theories as when only set theoretical language is in use, as long as the definitions appropriate to ZFC are understood to be used in the [[ZFC]] context and the definitions appropriate to NFU are understood to be used in the NFU context.

Whatever is proven to exist in a theory clearly provably exists in any extension of that theory; moreover, analysis of the proof that an object exists in a given theory may show that it exists in weaker versions of that theory (one may consider [[Zermelo set theory]] instead of [[ZFC]] for much of what is done in this article, for example).