Wikipedia

Interpretability logic: Difference between revisions

Browse history interactively
← Previous edit
Content deleted Content added
VisualWikitext
No edit summary
m →‎Logic TOL: style & layout
 
(3 intermediate revisions by 2 users not shown)
Line 11:
Axiom schemata:
 
1.# All classical tautologies
7.# <math> \Box(p \trianglerightrightarrow q) \rightarrow (\DiamondBox p \rightarrow \DiamondBox q) </math>▼
 
2.# <math>\Box(\Box p \rightarrow qp) \rightarrow (\Box p \rightarrow \Box q)</math>
9.# <math> \Box (p \trianglerightrightarrow q) \rightarrow( (p\wedge\Box r)\triangleright (q\wedge\Box r)) </math>▼
 
3.# <math>\Box(\Box (p \rightarrowtriangleright pq)\wedge (q \rightarrowtriangleright r)\Boxrightarrow (p\triangleright r)</math>
6.# <math> (p \triangleright r)\wedge (q \triangleright r)\rightarrow ((p\vee q)\triangleright r)</math>▼
 
4.# <math> \Box (p \rightarrowtriangleright q) \rightarrow (\Diamond p \trianglerightrightarrow \Diamond q) </math>
8.# <math> \Diamond p \triangleright p </math>▼
 
5.# <math> (p \triangleright q)\wedge rightarrow(q (p\trianglerightwedge\Box r)\rightarrowtriangleright (pq\trianglerightwedge\Box r)) </math>
 
▲6. <math> (p \triangleright r)\wedge (q \triangleright r)\rightarrow ((p\vee q)\triangleright r)</math>
 
▲7. <math> (p \triangleright q)\rightarrow (\Diamond p \rightarrow \Diamond q) </math>
 
▲8. <math> \Diamond p \triangleright p </math>
 
▲9. <math> (p \triangleright q)\rightarrow((p\wedge\Box r)\triangleright (q\wedge\Box r)) </math>
 
Rules of inference:
 
1.# “From <math>p</math> and <math>p\rightarrow q</math> conclude <math>q</math>”
2.# “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. ▼
▲2. “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 ===
Line 43 ⟶ 34:
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 ⊤):
 
1.# All classical tautologies
5.# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r}, p\wedge\neg q,p\vec{s})\vee \Diamond (\vec{r}, q,\vec{s}) </math>▼
 
2.# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r}, p\wedge \neg q,\vec{s})\vee \Diamond (\vec{r}, q,\vec{s}p)) </math>
7.# <math>\Diamond (\vec{r},\Diamond(p,\vec{s}))\rightarrow \Diamond (\vec{r},\vec{s})</math>▼
 
3.# <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r},p,p,\wedge \neg\Diamond (pvec{s})) </math>
6.# <math>\Diamond (p,\Diamond(\vec{r}))\rightarrow \Diamond (p\wedge\Diamond(\vec{r}))</math>▼
 
4.# <math>\Diamond (\vec{r},p,\Diamond(\vec{s}))\rightarrow \Diamond (\vec{r},\vec{s})</math>
 
▲5. <math>\Diamond (\vec{r},p,\vec{s})\rightarrow \Diamond (\vec{r},p,p,\vec{s})</math>
 
▲6. <math>\Diamond (p,\Diamond(\vec{r}))\rightarrow \Diamond (p\wedge\Diamond(\vec{r}))</math>
 
▲7. <math>\Diamond (\vec{r},\Diamond(\vec{s}))\rightarrow \Diamond (\vec{r},\vec{s})</math>
 
Rules of inference:
 
1.# “From <math>p</math> and <math>p\rightarrow q</math> conclude <math>q</math>”
2.# “From <math>\neg p</math> conclude <math>\neg \Diamond( p)</math>”.▼
 
▲2. “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:Modal logic]]
[[Category:Provability logic]]
[[Category:Interpretation (philosophy)]]
Retrieved from "https://en.wikipedia.org/wiki/Interpretability_logic"