Content deleted Content added
m grammar |
m →Logic TOL: style & layout |
||
| (12 intermediate revisions by 11 users not shown) | |||
Line 1:
'''Interpretability logics''' comprise a family of [[modal logic]]s that extend [[provability logic]] to describe [[interpretability]]
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.
==
* [http://www.csc.villanova.edu/~japaridz/ Giorgi Japaridze] and Dick de Jongh, ''The Logic of Provability''. In '''Handbook of Proof Theory''', S.Buss, ed. Elsevier, 1998, pp. 475-546.▼
=== Logic ILM ===
[[Category:Modal logic]]▼
The language of ILM extends that of classical propositional logic by adding the unary modal operator <math>\Box</math> and the binary modal operator <math>\triangleright</math> (as always, <math>\Diamond p</math> is defined as <math>\neg \Box\neg p</math>). The arithmetical interpretation of <math>\Box p</math> is “<math>p</math> is provable in [[Peano arithmetic]] (PA)”, and <math>p \triangleright q</math> is understood as “<math>PA+q</math> is interpretable in <math>PA+p</math>”.
Axiom schemata:
# All classical tautologies
# <math>\Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q)</math>
# <math>\Box(\Box p \rightarrow p) \rightarrow \Box p</math>
# <math> \Box (p \rightarrow q) \rightarrow (p \triangleright q)</math>
# <math> (p \triangleright q)\wedge (q \triangleright r)\rightarrow (p\triangleright r)</math>
# <math> (p \triangleright r)\wedge (q \triangleright r)\rightarrow ((p\vee q)\triangleright r)</math>
# <math> (p \triangleright q)\rightarrow (\Diamond p \rightarrow \Diamond q) </math>
# <math> \Diamond p \triangleright p </math>
# <math> (p \triangleright q)\rightarrow((p\wedge\Box r)\triangleright (q\wedge\Box r)) </math>
Rules of inference:
# “From <math>p</math> and <math>p\rightarrow q</math> conclude <math>q</math>”
# “From <math>p</math> conclude <math>\Box p</math>”.
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 <math>\Diamond</math> which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of <math>\Diamond( p_1,\ldots,p_n)</math> is “<math>(PA+p_1,\ldots,PA+p_n)</math> is a [[tolerant sequence]] of theories”.
Axioms (with <math>p,q</math> standing for any formulas, <math>\vec{r},\vec{s}</math> for any sequences of formulas, and <math>\Diamond()</math> identified with ⊤):
# All classical tautologies
# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r}, p\wedge\neg q,\vec{s})\vee \Diamond (\vec{r}, q,\vec{s}) </math>
# <math>\Diamond (p)\rightarrow \Diamond (p\wedge \neg\Diamond (p)) </math>
# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r},\vec{s})</math>
# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r},p,p,\vec{s})</math>
# <math>\Diamond (p,\Diamond(\vec{r}))\rightarrow \Diamond (p\wedge\Diamond(\vec{r}))</math>
# <math>\Diamond (\vec{r},\Diamond(\vec{s}))\rightarrow \Diamond (\vec{r},\vec{s})</math>
Rules of inference:
# “From <math>p</math> and <math>p\rightarrow q</math> conclude <math>q</math>”
# “From <math>\neg p</math> conclude <math>\neg \Diamond( p)</math>”.
The completeness of TOL with respect to its arithmetical interpretation was proven by [[Giorgi Japaridze]].
==References==
▲* [https://web.archive.org/web/20190419120954/http://www.csc.villanova.edu/~japaridz/ Giorgi Japaridze] and [[Dick de Jongh]], ''The Logic of Provability''. In '''Handbook of Proof Theory''', S. Buss, ed., Elsevier, 1998, pp. 475-546.
[[Category:Interpretation (philosophy)]]
| |||