Cointerpretability¶

Compare formal theories by a logic-preserving translation in the reverse language direction that reflects the translated theory's theorems, a dual of interpretability tied to Σ₁-conservativity for suitable arithmetical theories.

Version: v2 · 2026-09-19 · History
Domain-specific #: 1496
Domain group: Formal Sciences
Origin domain: Mathematics
Subdomains: Mathematical Logic, Relations Between Formal Theories → Mathematics
Aliases: Co-interpretability

Core Idea¶

Cointerpretability is a directed relation between formal theories introduced by Giorgi Japaridze as a dual to interpretability. In a simplified orientation, theory T is cointerpretable in theory S when there is a logical-structure-preserving translation τ from the language of S into the language of T such that, for every sentence A of S, if T proves the translation τ(A), then S already proves A.

The direction is load-bearing. Ordinary interpretability translates the interpreted theory into the interpreting theory and preserves theoremhood forward: proofs in the source become proofs of translations in the target. Cointerpretability reverses the language direction relative to the named pair and imposes theorem reflection: T must not prove a translated S-sentence unless S proves the original.

How would you explain it like I'm…

No faithful explanation at this level. All three generators agree that any child-level picture collapses into 'one rulebook copies or matches another', which is mutual simulation or forward interpretability and erases the reversed translation direction and the theorem-reflection condition.

No-Sneaking-In Translation

Imagine two rulebooks, S and T, that each let you prove facts, plus a dictionary that turns any sentence in S's language into T's language. Cointerpretability is a rule about that dictionary: if T can prove the translated sentence, then S must already have been able to prove the original. In other words, translating over to T never lets you sneak in a new fact about S's sentences that S couldn't prove itself. The direction matters: this is a check that T doesn't overclaim, not a claim that the two rulebooks can copy each other.

Theorem-Reflecting Translation

In logic, a formal theory is a set of axioms plus everything provable from them. Cointerpretability is a one-way relation between two theories, introduced by Giorgi Japaridze as the dual of interpretability. Roughly, T is cointerpretable in S when there is a translation τ from S's language into T's language, preserving logical structure, such that whenever T proves τ(A), S already proves A. Ordinary interpretability works the other way: it guarantees that what the source proves, the target proves in translation, pushing theorems forward. Cointerpretability instead reflects theorems backward, so T cannot 'know more' about translated S-sentences than S does. That makes it a conservativity-style comparison, not a statement that one theory can simulate the other.

Cointerpretability, introduced by Giorgi Japaridze as a dual to interpretability, is a directed relation between formal theories. In a simplified orientation, T is cointerpretable in S if there is a translation τ from the language of S into the language of T, preserving logical structure, such that for every S-sentence A, T ⊢ τ(A) implies S ⊢ A. By contrast, ordinary interpretability translates the interpreted theory into the interpreting one and carries theorems forward. Cointerpretability reverses the language direction relative to the named pair and demands theorem reflection, so it is conservativity-like rather than a form of mutual simulation. Japaridze introduced it, together with cotolerance, in his 1993 study of generalized weak interpretability. For essentially reflexive arithmetical theories, he characterized Σ₁-conservativity in terms of cointerpretability. That equivalence depends on those hypotheses and should not be asserted for arbitrary theories.

Scope of Application¶

Cointerpretability belongs to metamathematics, proof theory, theories of arithmetic, interpretability logic, conservativity analysis, and modal logics of relative strength. It offers a translation-based account of when one arithmetic theory adds no new theorems of a specified low complexity over another.

The relation requires formal theories and an admissible translation scheme. Results depend on whether theories are recursively axiomatized, sequential, essentially reflexive, extend Peano arithmetic, or meet other technical conditions. The frozen summary's broad phrase “Peano arithmetic and stronger computably axiomatized theories” should be read through the original theorem rather than treated as an unrestricted slogan.

Clarity¶

Write the relation with languages before reasoning verbally:

T cointerpretable in S via τ: L_S → L_T only if T ⊢ τ(A) ⇒ S ⊢ A for every relevant L_S sentence A.

This diagram prevents the most common mistake. The translation arrow points from S's language to T's language, while theoremhood reflects back from T to S.

Manages Complexity¶

Relations among theories can be compared semantically through models, syntactically through proof transformations, or extensionally through shared consequences. Cointerpretability packages a conservativity-like comparison into one translation plus a reflection condition. It lets tools from interpretability logic address statements about what a theory fails to add.

The relation also separates language difference from proof strength. Two theories may use different vocabularies; a translation aligns their sentences, and reflection checks whether the target proves any translated claim unavailable in the source.

Abstract Reasoning¶

Orientation determines content. Reversing the translation or implication changes the relation.
Reflection blocks new translated theorems. If T proves τ(A) while S does not prove A, that translation does not witness cointerpretability.
The relation is directed. A witness from S to T does not automatically give one in reverse.
Equiconsistency is insufficient. Consistency comparison does not control individual translated consequences.

Knowledge Transfer¶

Within mathematical logic, the concept transfers between arithmetic conservativity, modal interpretability logics, and proof-theoretic strength comparisons. The common object is the formal translation and theorem-reflection condition.

It may inform programming-language conservativity or proof-assistant embeddings when an exact analogue is defined, but terminological transfer should be cautious. A compiler that rejects new results is not cointerpretability without theories and derivability.

Relationships to Other Abstractions¶

Current abstraction Cointerpretability Domain-specific

Parents (1) — outgoing typed relations

Cointerpretability includes Duality Prime

provability is controlled across representation.

Hierarchy path (1) — routes to 1 parentless root

Cointerpretability → includes Duality

Neighborhood in Abstraction Space¶

Cointerpretability sits in a sparse region of the domain-specific corpus (86^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Formal Arithmetic & Incompleteness (6 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-25