Логика интерпретируемости составляют семью модальная логика которые расширяют логика доказуемости описать интерпретируемость или различные связанные метаматематические свойства и отношения, такие как слабая интерпретируемость, Π1-консервативность, интерпретируемость, толерантность, толерантность, и арифметические сложности.
Основными авторами в этой области являются Алессандро Берардуччи, Петр Гайек, Константин Игнатьев, Георгий Джапаридзе, Франко Монтанья, Владимир Шавруков, Ринеке Вербрюгге, Альберт Виссер и Доменико Замбелла.
Примеры
Логика ILM
Язык ILM расширяет язык классической логики высказываний, добавляя унарный модальный оператор
и бинарный модальный оператор
(как всегда,
определяется как
). Арифметическая интерпретация
является "
доказуемо в арифметике Пеано PA », и
понимается как «
интерпретируется в
”.
Схемы аксиом:
1. Все классические тавтологии
2. ![Box (p rightarrow q) rightarrow ( Box p rightarrow Box q)](https://wikimedia.org/api/rest_v1/media/math/render/svg/378bbb022b019f390c5aedc4c0581f32a3179ea6)
3. ![Box ( Box p rightarrow p) rightarrow Box p](https://wikimedia.org/api/rest_v1/media/math/render/svg/3da9af6a03a02c8c77dbd4d7dfc7b44088d73723)
4. ![Box (p rightarrow q) rightarrow (p triangleright q)](https://wikimedia.org/api/rest_v1/media/math/render/svg/c3457bdfc4985887cd10a942e816114b1e5027af)
5. ![(p triangleright q) клин (q triangleright r) rightarrow (p triangleright r)](https://wikimedia.org/api/rest_v1/media/math/render/svg/12aae21987dcc4fbe69d248ed260bbcd04038c7e)
6. ![(p triangleright r) клин (q triangleright r) rightarrow ((p vee q) triangleright r)](https://wikimedia.org/api/rest_v1/media/math/render/svg/6d6dfce7718e6f6a1b6bf55f37bc6351079848a4)
7. ![{ Displaystyle (п triangleright q) rightarrow ( Diamond p rightarrow Diamond q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f603b81ca91e1edeb0a7e4ae78cbc021093d118e)
8. ![Diamond p triangleright p](https://wikimedia.org/api/rest_v1/media/math/render/svg/0b757c99196fa942ea816b101b462eac2e0b8d46)
9. ![(p triangleright q) rightarrow ((p wedge Box r) triangleright (q wedge Box r))](https://wikimedia.org/api/rest_v1/media/math/render/svg/9ff3f034ab104e014116bd12794e03074c2337c7)
Правила вывода:
1. «От
и
заключить
”
2. «От
заключить
”.
Полнота ILM с точки зрения арифметической интерпретации была независимо доказана Алессандро Берардуччи и Владимиром Шавруковым.
Логика ТОЛ
Язык TOL расширяет язык классической логики высказываний, добавляя модальный оператор
которому разрешено принимать любую непустую последовательность аргументов. Арифметическая интерпретация
является "
это толерантная последовательность теорий ».
Аксиомы (с
стоит для любых формул,
для любых последовательностей формул, и
обозначается ⊤):
1. Все классические тавтологии
2. ![Diamond ( vec {r}, p, vec {s}) rightarrow Diamond ( vec {r}, p wedge neg q, vec {s}) vee Diamond ( vec {r }, q, vec {s})](https://wikimedia.org/api/rest_v1/media/math/render/svg/636d62fa1cbf2ecce25c6991886673818e91c463)
3. ![Diamond (p) rightarrow Diamond (p клин neg Diamond (p))](https://wikimedia.org/api/rest_v1/media/math/render/svg/94edb2d602402f12a79aa26a169529b18a60f743)
4. ![Diamond ( vec {r}, p, vec {s}) rightarrow Diamond ( vec {r}, vec {s})](https://wikimedia.org/api/rest_v1/media/math/render/svg/204d8bc1e3ad8310a378285ac3a96d85dd49a49a)
5. ![Diamond ( vec {r}, p, vec {s}) rightarrow Diamond ( vec {r}, p, p, vec {s})](https://wikimedia.org/api/rest_v1/media/math/render/svg/5ad0e0687516c002fb6ecda0ad22c8fafdbf5d26)
6. ![Diamond (p, Diamond ( vec {r})) rightarrow Diamond (p wedge Diamond ( vec {r}))](https://wikimedia.org/api/rest_v1/media/math/render/svg/0e885de7dfcddc85e3f0e1eb605ae1697ccd6ebe)
7. ![Diamond ( vec {r}, Diamond ( vec {s})) rightarrow Diamond ( vec {r}, vec {s})](https://wikimedia.org/api/rest_v1/media/math/render/svg/317a7cd369c083d2b50c2d1adf774a238484e75e)
Правила вывода:
1. «От
и
заключить
”
2. «От
заключить
”.
Полнота ТОЛ относительно его арифметической интерпретации была доказана Георгий Джапаридзе.
использованная литература
- Георгий Джапаридзе и Дик де Йонг, Логика доказуемости. В Справочник по теории доказательств, S. Buss, ed., Elsevier, 1998, стр. 475-546.