Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Interpretability logic
open-in-new
<h2 id="examples">Examples</h2> <h3>Logic ILM</h3> <p>The language of ILM extends that of classical propositional logic by adding the unary modal operator ◻ {\displaystyle \Box } and the binary modal operator ▹ {\displaystyle \triangleright } (as always, ◊ p {\displaystyle \Diamond p} is defined as ¬ ◻ ¬ p {\displaystyle \neg \Box \neg p} ). The arithmetical interpretation of ◻ p {\displaystyle \Box p} is “ p {\displaystyle p} is provable in <a href="/facts/Peano_arithmetic/DhhDnNug">Peano arithmetic</a> (PA)”, and p ▹ q {\displaystyle p\triangleright q} is understood as “ P A + q {\displaystyle PA+q} is interpretable in P A + p {\displaystyle PA+p} ”. </p><p>Axiom schemata: </p> <ol><li>All classical tautologies</li> <li> ◻ ( p → q ) → ( ◻ p → ◻ q ) {\displaystyle \Box (p\rightarrow q)\rightarrow (\Box p\rightarrow \Box q)} </li> <li> ◻ ( ◻ p → p ) → ◻ p {\displaystyle \Box (\Box p\rightarrow p)\rightarrow \Box p} </li> <li> ◻ ( p → q ) → ( p ▹ q ) {\displaystyle \Box (p\rightarrow q)\rightarrow (p\triangleright q)} </li> <li> ( p ▹ q ) → ( ◊ p → ◊ q ) {\displaystyle (p\triangleright q)\rightarrow (\Diamond p\rightarrow \Diamond q)} </li> <li> ( p ▹ q ) ∧ ( q ▹ r ) → ( p ▹ r ) {\displaystyle (p\triangleright q)\wedge (q\triangleright r)\rightarrow (p\triangleright r)} </li> <li> ( p ▹ r ) ∧ ( q ▹ r ) → ( ( p ∨ q ) ▹ r ) {\displaystyle (p\triangleright r)\wedge (q\triangleright r)\rightarrow ((p\vee q)\triangleright r)} </li> <li> ◊ p ▹ p {\displaystyle \Diamond p\triangleright p} </li> <li> ( p ▹ q ) → ( ( p ∧ ◻ r ) ▹ ( q ∧ ◻ r ) ) {\displaystyle (p\triangleright q)\rightarrow ((p\wedge \Box r)\triangleright (q\wedge \Box r))} </li></ol> <p>Rules of inference: </p> <ol><li>“From p {\displaystyle p} and p → q {\displaystyle p\rightarrow q} conclude q {\displaystyle q} ”</li> <li>“From p {\displaystyle p} conclude ◻ p {\displaystyle \Box p} ”.</li></ol> <p>The completeness of ILM with respect to its arithmetical interpretation was independently proven by Alessandro Berarducci and Vladimir Shavrukov. </p> <h3>Logic TOL</h3> <p>The language of TOL extends that of classical propositional logic by adding the modal operator ◊ {\displaystyle \Diamond } which is allowed to take any nonempty sequence of arguments. The arithmetical interpretation of ◊ ( p 1 , … , p n ) {\displaystyle \Diamond (p_{1},\ldots ,p_{n})} is “ ( P A + p 1 , … , P A + p n ) {\displaystyle (PA+p_{1},\ldots ,PA+p_{n})} is a <a href="/facts/Tolerant_sequence/hQ26XBml">tolerant sequence</a> of theories”. </p><p>Axioms (with p , q {\displaystyle p,q} standing for any formulas, r → , s → {\displaystyle {\vec {r}},{\vec {s}}} for any sequences of formulas, and ◊ ( ) {\displaystyle \Diamond ()} identified with ⊤): </p> <ol><li>All classical tautologies</li> <li> ◊ ( r → , p , s → ) → ◊ ( r → , p ∧ ¬ q , s → ) ∨ ◊ ( r → , q , s → ) {\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p\wedge \neg q,{\vec {s}})\vee \Diamond ({\vec {r}},q,{\vec {s}})} </li> <li> ◊ ( p ) → ◊ ( p ∧ ¬ ◊ ( p ) ) {\displaystyle \Diamond (p)\rightarrow \Diamond (p\wedge \neg \Diamond (p))} </li> <li> ◊ ( r → , p , s → ) → ◊ ( r → , s → ) {\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},{\vec {s}})} </li> <li> ◊ ( r → , p , s → ) → ◊ ( r → , p , p , s → ) {\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p,p,{\vec {s}})} </li> <li> ◊ ( p , ◊ ( r → ) ) → ◊ ( p ∧ ◊ ( r → ) ) {\displaystyle \Diamond (p,\Diamond ({\vec {r}}))\rightarrow \Diamond (p\wedge \Diamond ({\vec {r}}))} </li> <li> ◊ ( r → , ◊ ( s → ) ) → ◊ ( r → , s → ) {\displaystyle \Diamond ({\vec {r}},\Diamond ({\vec {s}}))\rightarrow \Diamond ({\vec {r}},{\vec {s}})} </li></ol> <p>Rules of inference: </p> <ol><li>“From p {\displaystyle p} and p → q {\displaystyle p\rightarrow q} conclude q {\displaystyle q} ”</li> <li>“From ¬ p {\displaystyle \neg p} conclude ¬ ◊ ( p ) {\displaystyle \neg \Diamond (p)} ”.</li></ol> <p>The completeness of TOL with respect to its arithmetical interpretation was proven by <a href="/facts/Giorgi_Japaridze/jIqdKMln">Giorgi Japaridze</a>. </p> <ul><li><a href="https://web.archive.org/web/20190419120954/http://www.csc.villanova.edu/~japaridz/">Giorgi Japaridze</a> and <a href="/facts/Dick_de_Jongh/pQ25w4cs">Dick de Jongh</a>, <i>The Logic of Provability</i>. In Handbook of Proof Theory, S. Buss, ed., Elsevier, 1998, pp. 475-546.</li></ul>