Толкование диалектики - Dialectica interpretation

В теории доказательств , то толкование Диалектика является интерпретацией доказательства интуиционистского арифметической ( гейтинговых арифметики ) на конечное расширение типа из примитивно рекурсивной арифметики , так называемая система T . Он был разработан Куртом Гёделем, чтобы обеспечить непротиворечивость арифметических операций. Название интерпретации взято из журнала Dialectica , где статья Гёделя была опубликована в специальном выпуске 1958 года, посвященном Полу Бернейсу в день его 70-летия.

Мотивация

Посредством отрицательного перевода Геделя – Генцена последовательность классической арифметики Пеано уже была сведена к последовательности интуиционистской арифметики Гейтинга . Мотивацией Гёделя к развитию интерпретации диалектики было получение доказательства относительной непротиворечивости арифметики Гейтинга (и, следовательно, арифметики Пеано).

Диалектическая интерпретация интуиционистской логики

Интерпретация состоит из двух компонентов: перевод формулы и перевод корректуры. Преобразование формулы описывает, как каждая формула арифметики Гейтинга отображается в бескванторную формулу системы T, где и являются кортежами новых переменных (не появляющихся в свободном виде ). Интуитивно интерпретируется как . Перевод доказательства показывает, как доказательство имеет достаточно информации, чтобы засвидетельствовать интерпретацию , то есть доказательство может быть преобразовано в закрытый термин и доказательство в системе T. ${\ displaystyle A}$${\ Displaystyle A_ {D} (х; у)}$${\ displaystyle x}$${\ displaystyle y}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle \ существует x \ forall yA_ {D} (x; y)}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle A}$${\ displaystyle t}$${\ Displaystyle A_ {D} (т; у)}$

Перевод формул

Бескванторная формула определяется индуктивно на логической структуре следующим образом, где - атомарная формула: ${\ Displaystyle A_ {D} (х; у)}$${\ displaystyle A}$${\ displaystyle P}$

${\ Displaystyle {\ begin {array} {lcl} (P) _ {D} & \ Equiv & P \\ (A \ wedge B) _ {D} (x, v; y, w) & \ Equiv & A_ {D } (x; y) \ wedge B_ {D} (v; w) \\ (A \ vee B) _ {D} (x, v, z; y, w) & \ Equiv & (z = 0 \ rightarrow A_ {D} (x; y)) \ клин (z \ neq 0 \ to B_ {D} (v; w)) \\ (A \ rightarrow B) _ {D} (f, g; x, w) & \ Equiv & A_ {D} (x; fxw) \ rightarrow B_ {D} (gx; w) \\ (\ exists zA) _ {D} (x, z; y) & \ Equiv & A_ {D} (x ; y) \\ (\ forall zA) _ {D} (f; y, z) & \ Equiv & A_ {D} (fz; y) \ end {array}}}$

Подтвержденный перевод (правильность)

Интерпретация формулы такова, что всякий раз, когда она доказуема в арифметике Гейтинга, существует такая последовательность замкнутых членов , которая доказуема в системе T. Последовательность терминов и доказательство строятся на основе данного доказательства в арифметике Гейтинга. Конструкция довольно проста, за исключением аксиомы сжатия, которая требует предположения о разрешимости бескванторных формул. ${\ displaystyle A}$${\ displaystyle t}$${\ Displaystyle A_ {D} (т; у)}$${\ displaystyle t}$${\ Displaystyle A_ {D} (т; у)}$${\ displaystyle A}$${\ displaystyle t}$${\ Displaystyle A \ rightarrow A \ клин A}$

Принципы характеризации

Также было показано, что арифметика Гейтинга расширилась за счет следующих принципов:

• Аксиома выбора
• Принцип Маркова
• Независимость посылки для универсальных формул

необходимо и достаточно для характеристики формул HA, интерпретируемых диалектической интерпретацией.

Расширения базовой интерпретации

Базовая диалектическая интерпретация интуиционистской логики была распространена на различные более сильные системы. Интуитивно диалектическая интерпретация может быть применена к более сильной системе, если диалектическая интерпретация дополнительного принципа может быть засвидетельствована терминами в системе T (или расширении системы T).

Индукция

Учитывая теорему Гёделя о неполноте (из которой следует, что непротиворечивость PA не может быть доказана конечными средствами), разумно ожидать, что система T должна содержать нефинитистические конструкции. Это действительно так. Нефинитистические конструкции проявляются в интерпретации математической индукции . Чтобы дать диалектическую интерпретацию индукции, Гёдель использует то, что сейчас называется примитивно-рекурсивными функционалами Гёделя , которые представляют собой функции высшего порядка с примитивно рекурсивными описаниями.

Классическая логика

Формулы и доказательства в классической арифметике также могут получить диалектическую интерпретацию посредством первоначального вложения в арифметику Гейтинга с последующей интерпретацией диалектики арифметики Гейтинга. Шенфилд в своей книге объединяет негативный перевод и интерпретацию диалектики в единую интерпретацию классической арифметики.

Понимание

В 1962 году Спектор расширил интерпретацию арифметики «Диалектика» Гёделя до полного математического анализа, показав, как схеме исчисляемого выбора можно придать интерпретацию «Диалектика» путем расширения системы T с помощью линейной рекурсии .

Диалектическая интерпретация линейной логики

Интерпретация Диалектики использовалась для построения модели утонченной Жираром интуиционистской логики, известной как линейная логика , через так называемые пространства Диалектики . Поскольку линейная логика является уточнением интуиционистской логики, диалектическая интерпретация линейной логики также может рассматриваться как уточнение диалектической интерпретации интуиционистской логики.

Хотя линейная интерпретация в работе Ширахаты подтверждает правило ослабления (на самом деле это интерпретация аффинной логики ), интерпретация диалектических пространств де Пайвы не подтверждает ослабление для произвольных формул.

Варианты интерпретации диалектики

С тех пор было предложено несколько вариантов интерпретации Диалектики. В частности, вариант Диллера-Нама (чтобы избежать проблемы сжатия) и монотонные интерпретации Коленбаха и ограниченные интерпретации Феррейры-Оливы (для интерпретации слабой леммы Кенига ). Подробное описание интерпретации можно найти на сайтах, и.

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