Equiconsistency
Encyclopedia
In mathematical logic
, two theories
are equiconsistent if, roughly speaking, they are "as consistent as each other".
It is not in general 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.
s. 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 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" 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.
, 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 ZFC+¬CH 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.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, two theories
Theory (mathematical logic)
In mathematical logic, a theory is a set of sentences in a formal language. Usually a deductive system is understood from context. An element \phi\in T of a theory T is then called an axiom of the theory, and any sentence that follows from the axioms is called a theorem of the theory. Every axiom...
are equiconsistent if, roughly speaking, they are "as consistent as each other".
It is not in general possible to prove the absolute consistency
Consistency
Consistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
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.
Consistency
In mathematical logic, formal theories are studied as mathematical objectMathematical object
In mathematics and the philosophy of mathematics, a mathematical object is an abstract object arising in mathematics.Commonly encountered mathematical objects include numbers, permutations, partitions, matrices, sets, functions, and relations...
s. Since some theories are powerful enough to model different mathematical objects, it is natural to wonder about their own consistency
Consistency
Consistency can refer to:* Consistency , the psychological need to be consistent with prior acts and statements* "Consistency", an 1887 speech by Mark Twain...
.
Hilbert
David Hilbert
David Hilbert was a German mathematician. He is recognized as one of the most influential and universal mathematicians of the 19th and early 20th centuries. Hilbert discovered and developed a broad range of fundamental ideas in many areas, including invariant theory and the axiomatization of...
proposed a program
Hilbert's program
In mathematics, Hilbert's program, formulated by German mathematician David Hilbert, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies...
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
Arithmetic
Arithmetic or arithmetics is the oldest and most elementary branch of mathematics, used by almost everyone, for tasks ranging from simple day-to-day counting to advanced science and business calculations. It involves the study of quantity, especially as the result of combining numbers...
, the program quickly became the establishment of the consistency of arithmetic by methods formalizable within arithmetic itself.
Gödel
Kurt Gödel
Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
's incompleteness theorems show that Hilbert's program cannot be realized: If a consistent recursively enumerable
Recursively enumerable set
In computability theory, traditionally called recursion theory, a set S of natural numbers is called recursively enumerable, computably enumerable, semidecidable, provable or Turing-recognizable if:...
theory is strong enough to formalize its own metamathematics
Metamathematics
Metamathematics is the study of mathematics itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories...
(whether something is a proof or not), i.e. strong enough to model a weak fragment of arithmetic (Robinson arithmetic
Robinson arithmetic
In mathematics, Robinson arithmetic, or Q, is a finitely axiomatized fragment of Peano arithmetic , first set out in R. M. Robinson . Q is essentially PA without the axiom schema of induction. Since Q is weaker than PA, it is incomplete...
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.
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 arithmeticSecond-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their...
, the reverse mathematics
Reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of...
program has much to say. Consistency strength issues are a usual part of set theory
Set theory
Set theory is the branch of mathematics that studies sets, which are collections of objects. Although any type of object can be collected into a set, set theory is applied most often to objects that are relevant to mathematics...
, 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
Primitive recursive arithmetic
Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist...
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
Forcing (mathematics)
In the mathematical discipline of set theory, forcing is a technique invented by Paul Cohen for proving consistency and independence results. It was first used, in 1963, to prove the independence of the axiom of choice and the continuum hypothesis from Zermelo–Fraenkel set theory...
allows one to show that the theories ZFC, ZFC+CH and ZFC+¬CH 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
Axiom of determinacy
The axiom of determinacy is a possible axiom for set theory introduced by Jan Mycielski and Hugo Steinhaus in 1962. It refers to certain two-person games of length ω with perfect information...
), the notions described above are adapted accordingly. Thus, ZF is equiconsistent with ZFC, as shown by Gödel.