Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Interpretability logic
Summary
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:
- All classical tautologies
- “From and conclude ”
- “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 ⊤):
- All classical tautologies
- “From and conclude ”
- “From conclude ”. The completeness of TOL with respect to its arithmetical interpretation was proven by Giorgi Japaridze.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related courses (1)
MATH-804: MLSTATS
ML for predictive modeling is important in both industry and research. We join experts from stats and math to shed light on particular aspects of the theory and interpretability of DL. We discuss the
Related publications (1)
Related concepts (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.