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: v1 · 2026-08-30 · History
Domain-specific #: 1496
Origin domain: mathematical logic
Subdomain: relations between formal theories
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. It therefore expresses a conservativity-like comparison rather than mutual simulation.

Japaridze introduced cointerpretability and cotolerance in his 1993 study of generalized weak interpretability. For essentially reflexive arithmetical theories, the paper characterizes Σ₁-conservativity in terms of cointerpretability by translations.^[1] The equivalence is hypothesis-sensitive; it must not be stated for arbitrary theories without the relevant effectiveness and arithmetic conditions.

Structural Signature¶

formal theory T — axioms and derivability over language L_T;
formal theory S — comparison theory over language L_S;
directed relation — “T cointerpretable in S” is ordered, not automatically symmetric;
translation τ: L_S → L_T — maps atomic formulas and extends compositionally;
logical preservation — translation respects connectives and quantifiers under its formal definition;
translated sentence τ(A) — an S-sentence is represented in T;
theorem-reflection condition — T ⊢ τ(A) implies S ⊢ A;
nontrivial admissibility requirements — domains, equality, parameters, or coding follow the chosen interpretation framework;
duality with interpretability — source/target and preservation/reflection roles are reversed in a precise sense;
conservativity connection — under suitable arithmetical hypotheses, the relation captures Σ₁-conservativity;
modal/metamathematical setting — the relation can be studied alongside tolerance, cotolerance, and interpretability logics.

The invariant is a reverse-directed admissible translation satisfying theorem reflection between the compared theories.

What It Is Not¶

Not interpretability. Interpretability preserves translated theorems forward; cointerpretability uses the dual orientation and reflection condition.
Not bi-interpretability. Bi-interpretability requires interpretations both ways with definable equivalences to identity; cointerpretability is not that package.
Not mutual interpretability. Symmetric interpretability does not by itself yield the same relation.
Not ordinary language translation. The map is formal, compositional, and proof-theoretically constrained.
Not equiconsistency. Having the same consistency strength is weaker and does not supply a theorem-reflecting translation.
Not conservative extension generally. The notions are related, and Σ₁-conservativity has a characterization under hypotheses, but definitions differ.
Not cotolerance. Cotolerance is another dual relation introduced in the same program.
Not model-theoretic co-interpretability under unrelated terminology. Some literature uses similar words for structures; scope must be explicit.

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.

This node is narrow because the term is uncommon and definition orientation is easy to reverse. Any implementation or cross-reference should display the implication explicitly.

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. If instead one has S ⊢ A ⇒ T ⊢ τ(A), that is the preservation direction familiar from an interpretation of S in T.

Full definitions may encode domains and relativize quantifiers, so the simplified map is not a substitute for the cited formalism. It is a reader-facing diagnostic. Claims about Σ₁-conservativity must also specify which theory is conservative over which and the sentence class.

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. Without translation, consequence sets in different languages cannot be compared directly.

Its duality with interpretability creates a systematic family. Preservation and reflection, interpretation and cointerpretation, tolerance and cotolerance can be analyzed together rather than as unrelated definitions.

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.
Conservativity equivalence is conditional. Arithmetic hypotheses are part of the theorem, not dispensable context.
Translation can compare different signatures. Vocabulary mismatch is handled compositionally rather than by literal sentence identity.
Mutual variants require separate proof. Two directed cointerpretations may yield a stronger relation but should not be called bi-interpretability automatically.

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.

The broader structural residue is faithful translation plus reflection. That can instantiate primes such as duality, translation, or conservativity outside this named theory relation.

Examples¶

Witness test. Propose τ: L_S → L_T; verify logical compositionality and prove uniformly that T ⊢ τ(A) yields S ⊢ A.
Failure witness. Find an S-sentence A unprovable in S whose translation is provable in T; cointerpretability via τ fails.
Arithmetic case. Under Japaridze's hypotheses, a Σ₁-conservativity relation can be characterized by existence of an appropriate cointerpretation.
Different signatures. Definitions or coding can translate arithmetic vocabulary into a richer theory while reflection constrains added consequences.
Direction check. A forward theorem-preserving translation may witness interpretability yet fail the reverse reflection required here.

Structural Tensions¶

Preservation vs. reflection. Interpretation transports provability; cointerpretability prevents translated overreach.
Language flexibility vs. proof fidelity. Translation bridges signatures but must preserve logical form.
Semantic intuition vs. syntactic definition. Model comparison motivates the relation; derivability and translation define it.
General theory relation vs. arithmetic theorem. The definition is broad, while the Σ₁ characterization needs strong hypotheses.
Duality vs. symmetry. Being dual to a relation does not make the relation symmetric.

Structural–Framed Character¶

The node is structural. Once theories, derivability, sentence class, and translation notion are fixed, the relation is mathematical. Variant conventions require explicit orientation but not interpretive judgment.

Structural Core vs. Domain Accent¶

The core is reflection across a translation: the receiving theory cannot establish translated content absent from the source. The domain accent is formal theories, proof systems, arithmetic complexity, and interpretability logic.

Duality — cointerpretability reverses roles associated with interpretability.
Translation — formulas move compositionally between languages.
Reflection — translated theoremhood implies source theoremhood.
Conservativity — no new consequences of a specified class are added under hypotheses.
Directionality — the ordered pair matters.
Invariant — provability is controlled across representation.

The prospective DAG edge uses composition under prime:duality because no Interpretability or Conservativity parent is present.

Relationships to Other Abstractions¶

Current abstraction Cointerpretability Domain-specific

Parents (1) — more general patterns this builds on

Cointerpretability is part of Duality Prime

provability is controlled across representation.

Hierarchy path (1) — routes to 1 parentless root

Cointerpretability → Duality

Neighborhood in Abstraction Space¶

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

Family — Automata, Model Checking & Formal Semantics (10 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

Interpretability — forward theorem-preserving translation relation.
Bi-Interpretability — mutual interpretations coherent up to definable isomorphism.
Mutual Interpretability — interpretations in both directions.
Conservative Extension — same-language consequence relation.
Equiconsistency — equality of consistency strength.
Cotolerance / Tolerance — related but distinct metamathematical notions.

References¶

[1] Giorgi Japaridze, “A generalized notion of weak interpretability and the corresponding modal logic,” Annals of Pure and Applied Logic 61 (1993), 113–160, https://doi.org/10.1016/0168-0072(93)90201-N. registry ↩

[2] Giorgi Japaridze and Dick de Jongh, “The Logic of Provability,” in Handbook of Proof Theory, 1998, pp. 476–546. registry

[3] “Cointerpretability,” Wikipedia, frozen revision 1334265590 (2026-01-22), https://en.wikipedia.org/wiki/Cointerpretability. registry