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.

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

1. Orientation determines content. Reversing the translation or implication changes the relation. 2. Reflection blocks new translated theorems. If T proves τ(A) while S does not prove A, that translation does not witness cointerpretability. 3. The relation is directed. A witness from S to T does not automatically give one in reverse. 4. 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) — 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

• Formal Theory — 0.82
• Harrop Formula — 0.80
• Liskov Substitution Principle — 0.80
• Monoidal t-Norm Logic — 0.80
• Negation as Failure — 0.80

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