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
Tolerance or toleration is the state of tolerating, or putting up with, conditionally.
Economics, business, and politics
* Toleration Party, a historic political party active in Connecticut
* Tolerant Systems, the former name of Veritas Software ...
,
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.
Examples
Logic ILM
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
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
(PA)”, and
is understood as “
is interpretable in
”.
Axiom schemata:
1. All classical tautologies
2.
3.
4.
5.
6.
7.
8.
9.
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.
Logic TOL
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 ⊤):
1. All classical tautologies
2.
3.
4.
5.
6.
7.
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.
References
Giorgi Japaridzeand
Dick de Jongh, ''The Logic of Provability''. In Handbook of Proof Theory, S. Buss, ed., Elsevier, 1998, pp. 475-546.
Modal logic
Provability logic