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 diversas 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

Lógica ILM

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

Esquemas axiomáticos :

Todas las tautologías clásicas
$\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))$

Reglas de inferencia :

"De $p$ y $p\rightarrow q$ concluir $q$ ”
"De $p$ concluir $\Box p$ ”.

La exhaustividad de ILM con respecto a su interpretación aritmética fue demostrada independientemente por Alessandro Berarducci y Vladimir Shavrukov.

Lógica TOL

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

Axiomas (con $p,q$ representando cualquier fórmula, ${\vec {r}},{\vec {s}}$ para cualquier secuencia de fórmulas, y $\Diamond ()$ identificado con ⊤):

Todas las tautologías clásicas
$\Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p\wedge \neg q,{\vec {s}})\vee \Diamond ({\vec {r}},q,{\vec {s}})$
$\Diamond (p)\rightarrow \Diamond (p\wedge \neg \Diamond (p))$
$\Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},{\vec {s}})$
$\Diamond ({\vec {r}},p,{\vec {s}})\rightarrow \Diamond ({\vec {r}},p,p,{\vec {s}})$
$\Diamond (p,\Diamond ({\vec {r}}))\rightarrow \Diamond (p\wedge \Diamond ({\vec {r}}))$
$\Diamond ({\vec {r}},\Diamond ({\vec {s}}))\rightarrow \Diamond ({\vec {r}},{\vec {s}})$

Reglas de inferencia:

"De $p$ y $p\rightarrow q$ concluir $q$ ”
"De $\neg p$ concluir $\neg \Diamond (p)$ ”.

La exhaustividad de TOL con respecto a su interpretación aritmética fue demostrada por Giorgi Japaridze .

Referencias

Giorgi Japaridze y Dick de Jongh , La lógica de la demostrabilidad . En Manual de teoría de la demostración , S. Buss, ed., Elsevier, 1998, págs. 475-546.