Lógica de interpretabilidad

Las lógicas de interpretabilidad comprenden una familia de lógicas modales que extienden la lógica de demostrabilidad para describir la interpretabilidad o varias propiedades y relaciones metamatemáticas relacionadas, como la interpretabilidad débil , la conservatividad Π ₁ , la cointerpretabilidad , la tolerancia , la cotolerancia y las complejidades aritméticas.

Los principales contribuyentes al campo son Alessandro Berarducci, Petr Hájek , Konstantin Ignatiev, Giorgi Japaridze , Franco Montagna, Vladimir Shavrukov, Rineke Verbrugge , Albert Visser y Domenico Zambella.

Ejemplos

ILM lógica

El lenguaje de ILM extiende el de la lógica proposicional clásica agregando el operador modal unario y el operador modal binario (como siempre, se define como ). La interpretación aritmética de es “ es demostrable en aritmética de Peano (PA)”, y se entiende como “ es interpretable en ”. ${\displaystyle \Box }$ ${\displaystyle \triangleright }$ ${\displaystyle \Diamond p}$ ${\displaystyle \neg \Box \neg p}$ ${\displaystyle \Box p}$ ${\displaystyle p}$ ${\displaystyle p\triangleright q}$ ${\displaystyle PA+q}$ ${\displaystyle PA+p}$

Esquemas de axiomas:

1. Todas las tautologías clásicas.
2. ${\displaystyle \Box (p\rightarrow q)\rightarrow (\Box p\rightarrow \Box q)}$
3. ${\displaystyle \Box (\Box p\rightarrow p)\rightarrow \Box p}$
4. ${\displaystyle \Box (p\rightarrow q)\rightarrow (p\triangleright q)}$
5. ${\displaystyle (p\triangleright q)\wedge (q\triangleright r)\rightarrow (p\triangleright r)}$
6. ${\displaystyle (p\triangleright r)\wedge (q\triangleright r)\rightarrow ((p\vee q)\triangleright r)}$
7. ${\displaystyle (p\triangleright q)\rightarrow (\Diamond p\rightarrow \Diamond q)}$
8. ${\displaystyle \Diamond p\triangleright p}$
9. ${\displaystyle (p\triangleright q)\rightarrow ((p\wedge \Box r)\triangleright (q\wedge \Box r))}$

Reglas de inferencia:

1. “De y concluir ” ${\displaystyle p}$ ${\displaystyle p\rightarrow q}$ ${\displaystyle q}$
2. “De concluir ”. ${\displaystyle p}$ ${\displaystyle \Box p}$

La integridad del ILM con respecto a su interpretación aritmética fue probada de forma independiente por Alessandro Berarducci y Vladimir Shavrukov.

TOL lógico

El lenguaje de TOL amplía el de la lógica proposicional clásica al agregar el operador modal al que se le permite tomar cualquier secuencia de argumentos no vacía. La interpretación aritmética de es " es una secuencia tolerante de teorías". ${\displaystyle \Diamond }$ ${\displaystyle \Diamond (p_{1},\ldots ,p_{n})}$ ${\displaystyle (PA+p_{1},\ldots ,PA+p_{n})}$

Axiomas (que representan cualquier fórmula, cualquier secuencia de fórmulas e identificados con ⊤): ${\displaystyle p,q}$ ${\displaystyle {\vec {r}},{\vec {s}}}$ ${\displaystyle \Diamond ()}$

1. Todas las tautologías clásicas.
2. ${\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p\wedge \neg q,{\vec {s}})\vee \Diamond ({\vec {r}},q,{\vec {s}})}$
3. ${\displaystyle \Diamond (p)\rightarrow \Diamond (p\wedge \neg \Diamond (p))}$
4. ${\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},{\vec {s}})}$
5. ${\displaystyle \Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p,p,{\vec {s}})}$
6. ${\displaystyle \Diamond (p,\Diamond ({\vec {r}}))\rightarrow \Diamond (p\wedge \Diamond ({\vec {r}}))}$
7. ${\displaystyle \Diamond ({\vec {r}},\Diamond ({\vec {s}}))\rightarrow \Diamond ({\vec {r}},{\vec {s}})}$

Reglas de inferencia:

1. “De y concluir ” ${\displaystyle p}$ ${\displaystyle p\rightarrow q}$ ${\displaystyle q}$
2. “De concluir ”. ${\displaystyle \neg p}$ ${\displaystyle \neg \Diamond (p)}$

Giorgi Japaridze demostró la integridad de TOL con respecto a su interpretación aritmética .

Referencias

• Giorgi Japaridze y Dick de Jongh , La lógica de la demostrabilidad . En Handbook of Proof Theory , S. Buss, ed., Elsevier, 1998, págs. 475-546.