In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, cointerpretability is a
binary relation
In mathematics, a binary relation associates some elements of one Set (mathematics), set called the ''domain'' with some elements of another set called the ''codomain''. Precisely, a binary relation over sets X and Y is a set of ordered pairs ...
on
formal theories: a formal theory ''T'' is cointerpretable in another such theory ''S'', when the language of ''S'' can be translated into the language of ''T'' in such a way that ''S'' proves every formula whose translation is a
theorem
In mathematics and formal logic, a theorem is a statement (logic), statement that has been Mathematical proof, proven, or can be proven. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to esta ...
of ''T''. The "translation" here is required to preserve the logical structure of formulas.
This concept, in a sense dual to
interpretability
In mathematical logic, interpretability is a relation between formal theories that expresses the possibility of interpreting or translating one into the other.
Informal definition
Assume ''T'' and ''S'' are formal theories. Slightly simplified, ...
, was introduced by , who also proved that, for theories of
Peano arithmetic
In mathematical logic, the Peano axioms (, ), also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nea ...
and any stronger theories with effective
axiomatization
In mathematics and logic, an axiomatic system is a set of formal statements (i.e. axioms) used to logically derive other statements such as lemmas or theorems. A proof within an axiom system is a sequence of deductive steps that establishes ...
s, cointerpretability is equivalent to
-conservativity.
See also
*
Cotolerance
*
Interpretability logic
*
Tolerance (in logic)
References
*.
*.
Mathematical relations
Mathematical logic
{{logic-stub