Type a search term to find related articles by LIMS subject matter experts gathered from the most trusted and dynamic collaboration tools in the laboratory informatics industry.
In mathematical logic, two theories are equiconsistent if the consistency of one theory implies the consistency of the other theory, and vice versa. In this case, they are, roughly speaking, "as consistent as each other".
In general, it is not possible to prove the absolute consistency of a theory T. Instead we usually take a theory S, believed to be consistent, and try to prove the weaker statement that if S is consistent then T must also be consistent—if we can do this we say that T is consistent relative to S. If S is also consistent relative to T then we say that S and T are equiconsistent.
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 computably enumerable theory is strong enough to formalize its own metamathematics (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" needs 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.
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. 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 computable theory that can certainly model most of mathematics. The most widely used 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 really being claimed is that in the metatheory (Peano arithmetic in this case) 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. The method of forcing allows one to show that the theories ZFC, ZFC+CH and ZFC+¬CH are all equiconsistent (where CH denotes the continuum hypothesis).
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.
The consistency strength of numerous combinatorial statements can be calibrated by large cardinals. For example:
| General | |||||||||
|---|---|---|---|---|---|---|---|---|---|
| Theorems (list) and paradoxes | |||||||||
| Logics |
| ||||||||
| Set theory |
| ||||||||
| Formal systems (list), language and syntax |
| ||||||||
| Proof theory | |||||||||
| Model theory | |||||||||
| Computability theory | |||||||||
| Related | |||||||||
LIMS forum content by LIMS forum members is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License. Based on a work at www.limsforum.com.
