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. The language of ILM extends that of classical propositional logic by adding the unary modal operator and the binary modal operator (as always, is defined as ). The arithmetical interpretation of is “ is provable in Peano arithmetic (PA)”, and is understood as “ is interpretable in ”. Axiom schemata:

  1. All classical tautologies

Rules of inference:

  1. “From and conclude ”
  2. “From conclude ”. The completeness of ILM with respect to its arithmetical interpretation was independently proven by Alessandro Berarducci and Vladimir Shavrukov. The language of TOL extends that of classical propositional logic by adding the modal operator which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of is “ is a tolerant sequence of theories”. Axioms (with standing for any formulas, for any sequences of formulas, and identified with ⊤):
  3. All classical tautologies

Rules of inference:

  1. “From and conclude ”
  2. “From conclude ”. The completeness of TOL with respect to its arithmetical interpretation was proven by Giorgi Japaridze.
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Publications associées (1)
Concepts associés (2)
Interpretability
In mathematical logic, interpretability is a relation between formal theories that expresses the possibility of interpreting or translating one into the other. Assume T and S are formal theories. Slightly simplified, T is said to be interpretable in S if and only if the language of T can be translated into the language of S in such a way that S proves the translation of every theorem of T. Of course, there are some natural conditions on admissible translations here, such as the necessity for a translation to preserve the logical structure of formulas.
Tolerant sequence
In mathematical logic, a tolerant sequence is a sequence of formal theories such that there are consistent extensions of these theories with each interpretable in . Tolerance naturally generalizes from sequences of theories to trees of theories. Weak interpretability can be shown to be a special, binary case of tolerance. This concept, together with its dual concept of cotolerance, was introduced by Japaridze in 1992, who also proved that, for Peano arithmetic and any stronger theories with effective axiomatizations, tolerance is equivalent to -consistency.

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.