Interpretability logics comprise a family of
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
s that extend
provability logic Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic.
Examples
...
to describe
interpretability In mathematical logic, interpretability is a relation between formal theories that expresses the possibility of interpreting or translating one into the other.
Informal definition
Assume ''T'' and ''S'' are formal theories. Slightly simplified, '' ...
or various related metamathematical properties and relations such as
weak interpretability, Π
1-conservativity,
cointerpretability In mathematical logic, cointerpretability is a binary relation on formal theories: a formal theory ''T'' is cointerpretable in another such theory ''S'', when the language of ''S'' can be translated into the language of ''T'' in such a way that ''S' ...
,
tolerance,
cotolerance, and arithmetic complexities.
Main contributors to the field are Alessandro Berarducci,
Petr Hájek
Petr Hájek (; 6 February 1940 – 26 December 2016) was a Czech scientist in the area of mathematical logic and a professor of mathematics. Born in Prague, he worked at the Institute of Computer Science at the Academy of Sciences of the Czech Rep ...
, Konstantin Ignatiev,
Giorgi Japaridze Giorgi Japaridze (also spelled Giorgie Dzhaparidze) is a Georgian-American researcher in logic and theoretical computer science. He currently holds the title of Full Professor at the Computing Sciences Department of Villanova University. Japaridze i ...
, 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 u ...
(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 Giorgi Japaridze (also spelled Giorgie Dzhaparidze) is a Georgian-American researcher in logic and theoretical computer science. He currently holds the title of Full Professor at the Computing Sciences Department of Villanova University. Japaridze i ...
.
References
Giorgi Japaridzeand
Dick de Jongh
Dick Herman Jacobus de Jongh (born 19 October 1939, Enschede) is a Dutch logician and mathematician and a retired professor at the University of Amsterdam.
He received his PhD degree in 1968 from the University of Wisconsin–Madison under supervi ...
, ''The Logic of Provability''. In Handbook of Proof Theory, S. Buss, ed., Elsevier, 1998, pp. 475-546.
Modal logic
Provability logic