Reference articles on history, science, culture and more
Surprise meSurprise meSubscribe
Encyclopedia

Cointerpretability

Wikipedia contributorsAdapted for Fathomly · View authors
1 min read
Source updated January 22, 2026

In mathematical logic, cointerpretability is a binary relation 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 of T. The "translation" here is required to preserve the logical structure of formulas.

This concept, in a sense dual to interpretability, was introduced by Japaridze (1993), who also proved that, for theories of Peano arithmetic and any stronger theories with computable axiomatizations, cointerpretability is equivalent to \Sigma _{1}-conservativity.

Watch videos about CointerpretabilityExplainers and documentaries on YouTube (opens in a new tab)

Sources and credits

This article is adapted from the Wikipedia article “Cointerpretability”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.

Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.

Continue exploring

Related topics

Interpretability logic

Interpretability logics comprise a family of modal logics that extend provability logic to describe interpretability or various related metamathematical properties and relations such as weak interpretability, Π1-conservativity, cointerpretability, tolerance, cotolerance, and arithmetic complexities. Main contributors to the field are Alessandro Berarducci, Petr Hájek, Konstantin Ignatiev, Giorgi Japaridze, Franco Montagna, Vladimir Shavrukov, Rineke Verbrugge, Albert Visser, and Domenico Zambella.

Tolerant sequence

In mathematical logic, a tolerant sequence is a sequence T 1 {\displaystyle T_{1}} ,..., T n {\displaystyle T_{n}} of formal theories such that there are consistent extensions S 1 {\displaystyle S_{1}} ,..., S n {\displaystyle S_{n}} of these theories with each S i + 1 {\displaystyle S_{i+1}} interpretable in S i {\displaystyle S_{i}} . Tolerance naturally generalizes from sequences of theories to trees of theories.