Логика интерпретируемости - Interpretability logic

Логика интерпретируемости составляют семью модальная логика которые расширяют логика доказуемости описать интерпретируемость или различные связанные метаматематические свойства и отношения, такие как слабая интерпретируемость, Π₁-консервативность, интерпретируемость, толерантность, толерантность, и арифметические сложности.

Основными авторами в этой области являются Алессандро Берардуччи, Петр Гайек, Константин Игнатьев, Георгий Джапаридзе, Франко Монтанья, Владимир Шавруков, Ринеке Вербрюгге, Альберт Виссер и Доменико Замбелла.

Примеры

Логика ILM

Язык ILM расширяет язык классической логики высказываний, добавляя унарный модальный оператор ${\displaystyle \Box }$ и бинарный модальный оператор ${\displaystyle \triangleright }$ (как всегда, ${\displaystyle \Diamond p}$ определяется как ${\displaystyle \neg \Box \neg p}$). Арифметическая интерпретация ${\displaystyle \Box p}$ является "${\displaystyle p}$ доказуемо в арифметике Пеано PA », и ${\displaystyle p\triangleright q}$ понимается как «${\displaystyle PA+q}$ интерпретируется в ${\displaystyle PA+p}$”.

Схемы аксиом:

1. Все классические тавтологии

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))}$

Правила вывода:

1. «От ${\displaystyle p}$ и ${\displaystyle p\rightarrow q}$ заключить ${\displaystyle q}$”

2. «От ${\displaystyle p}$ заключить ${\displaystyle \Box p}$”.

Полнота ILM с точки зрения арифметической интерпретации была независимо доказана Алессандро Берардуччи и Владимиром Шавруковым.

Логика ТОЛ

Язык TOL расширяет язык классической логики высказываний, добавляя модальный оператор ${\displaystyle \Diamond }$ которому разрешено принимать любую непустую последовательность аргументов. Арифметическая интерпретация ${\displaystyle \Diamond (p_{1},\ldots ,p_{n})}$ является "${\displaystyle (PA+p_{1},\ldots ,PA+p_{n})}$ это толерантная последовательность теорий ».

Аксиомы (с ${\displaystyle p,q}$ стоит для любых формул, ${\displaystyle {\vec {r}},{\vec {s}}}$ для любых последовательностей формул, и ${\displaystyle \Diamond ()}$ обозначается ⊤):

1. Все классические тавтологии

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}})}$

Правила вывода:

1. «От ${\displaystyle p}$ и ${\displaystyle p\rightarrow q}$ заключить ${\displaystyle q}$”

2. «От ${\displaystyle \neg p}$ заключить ${\displaystyle \neg \Diamond (p)}$”.

Полнота ТОЛ относительно его арифметической интерпретации была доказана Георгий Джапаридзе.

использованная литература

• Георгий Джапаридзе и Дик де Йонг, Логика доказуемости. В Справочник по теории доказательств, S. Buss, ed., Elsevier, 1998, стр. 475-546.