Equiconsistency
From Wikipedia, the free encyclopedia
In mathematics, specifically in mathematical logic, formal theories are studied as mathematical objects. Since some theories are powerful enough to model different mathematical objects, it is natural to wonder about their own consistency.
Hilbert proposed a program at the beginning of the 20th century whose ultimate goal was to show, using mathematical methods, the consistency of mathematics. Since most mathematical disciplines can be reduced to arithmetic, the program quickly became the establishment of the consistency of arithmetic by methods formalizable within arithmetic itself.
Gödel's incompleteness theorems show that Hilbert's program cannot be realized: If a consistent recursively enumerable theory is strong enough to formalize its own meta-mathematics (whether something is a proof or not), i.e. strong enough to model a weak fragment of arithmetic (Robinson arithmetic suffices), then the theory cannot prove its own consistency. There are some technical caveats as to what requirements the formal statement representing the metamathematical statement "The theory is consistent" need to satisfy, but the outcome is that if a (sufficiently strong) theory can prove its own consistency then either there is no computable way of identifying whether a statement is even an axiom of the theory or not, or else the theory itself is inconsistent (in which case it can prove anything, including false statements such as its own consistency).
Given this, instead of outright consistency, one usually considers relative consistency: Let S and T be formal theories. Assume that S is a consistent theory. Does it follow that T is consistent? If so, then T is consistent relative to S. Two theories are equiconsistent if each one is consistent relative to the other.
[edit] Consistency strength
If T is consistent relative to S, but S is not known to be consistent relative to T, then we say that S has greater consistency strength than T. Of course, when discussing these issues of consistency strength the metatheory in which the discussion takes places needs to be carefully addressed. For theories at the level of second order arithmetic, the reverse mathematics program has much to say. Consistency strength issues are a usual part of set theory, since this is a recursive theory that can certainly model most of mathematics. The usual set of axioms of set theory is called ZFC. When a set theoretic statement A is said to be equiconsistent to another B, what is being claimed is that in the metatheory Peano Arithmetic it can be proven that the theories ZFC + A and ZFC + B are equiconsistent. Usually, primitive recursive arithmetic can be adopted as the metatheory in question, but even if the metatheory is ZFC or an extension of it, the notion is meaningful. Thus, the method of forcing allows one to show that the theories ZFC, ZFC + CH and 
are all equiconsistent.
When discussing fragments of ZFC or their extensions (for example, ZF, set theory without the axiom of choice, or ZF + AD, set theory with the axiom of determinacy), the notions described above are adapted accordingly. Thus, ZF is equiconsistent with ZFC, as shown by Gödel.
