HOME

TheInfoList



OR:

Interpretability logics comprise a family of
modal logic Modal logic is a kind of logic used to represent statements about Modality (natural language), necessity and possibility. In philosophy and related fields it is used as a tool for understanding concepts such as knowledge, obligation, and causality ...
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, 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, 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 \Box and the binary modal operator \triangleright (as always, \Diamond p is defined as \neg \Box\neg p). The arithmetical interpretation of \Box p is “p 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 nea ...
(PA)”, and p \triangleright q is understood as “PA+q is interpretable in PA+p”. Axiom schemata: # All classical tautologies # \Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q) # \Box(\Box p \rightarrow p) \rightarrow \Box p # \Box (p \rightarrow q) \rightarrow (p \triangleright q) # (p \triangleright q)\rightarrow (\Diamond p \rightarrow \Diamond q) # (p \triangleright q)\wedge (q \triangleright r)\rightarrow (p\triangleright r) # (p \triangleright r)\wedge (q \triangleright r)\rightarrow ((p\vee q)\triangleright r) # \Diamond p \triangleright p # (p \triangleright q)\rightarrow((p\wedge\Box r)\triangleright (q\wedge\Box r)) Rules of inference: # “From p and p\rightarrow q conclude q” # “From p conclude \Box p”. 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 \Diamond which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of \Diamond( p_1,\ldots,p_n) is “(PA+p_1,\ldots,PA+p_n) is a tolerant sequence of theories”. Axioms (with p,q standing for any formulas, \vec,\vec for any sequences of formulas, and \Diamond() identified with ⊤): # All classical tautologies # \Diamond (\vec,p,\vec)\rightarrow \Diamond (\vec, p\wedge\neg q,\vec)\vee \Diamond (\vec, q,\vec) # \Diamond (p)\rightarrow \Diamond (p\wedge \neg\Diamond (p)) # \Diamond (\vec,p,\vec)\rightarrow \Diamond (\vec,\vec) # \Diamond (\vec,p,\vec)\rightarrow \Diamond (\vec,p,p,\vec) # \Diamond (p,\Diamond(\vec))\rightarrow \Diamond (p\wedge\Diamond(\vec)) # \Diamond (\vec,\Diamond(\vec))\rightarrow \Diamond (\vec,\vec{s}) Rules of inference: # “From p and p\rightarrow q conclude q” # “From \neg p conclude \neg \Diamond( p)”. The completeness of TOL with respect to its arithmetical interpretation was proven by Giorgi Japaridze.


References


Giorgi Japaridze
and Dick de Jongh, ''The Logic of Provability''. In Handbook of Proof Theory, S. Buss, ed., Elsevier, 1998, pp. 475-546. Provability logic Interpretation (philosophy)