Независимость помещения

В теории доказательств и конструктивной математике принцип независимости посылок (IP) гласит, что если φ и ∃ x θ являются предложениями в формальной теории и φ → ∃ x θ доказуемо, то ∃ x (φ → θ) доказуемо. Здесь x не может быть свободной переменной функции φ, а θ может быть зависящим от нее предикатом.

Основное применение этого принципа приходится на изучение интуиционистской логики , где этот принцип вообще недействителен. Его критический эквивалентный частный случай обсуждается ниже.Этот принцип справедлив и в классической логике .

Обсуждение

Как обычно, предполагается, что область дискурса обитаема. То есть часть теории – это хоть какой-то термин. Для обсуждения мы выделяем один такой термин, как . В теории натуральных чисел эту роль может играть число 7 . Ниже φ и ψ обозначают предложения, не зависящие от x , а θ — предикат, который может зависеть от in.

Легко устанавливается следующее:

• Во-первых , если установлено, что φ истинно, то если предположить, что φ → ∃ x θ доказуемо, существует x, удовлетворяющий φ → θ .
• Во-вторых , если установлено, что φ ложно, то в результате взрыва любое предложение вида φ → ψ имеет место. Тогда любой x формально удовлетворяет φ → θ (да и любому предикату этой формы).

В первом сценарии некоторый x , связанный с посылкой, повторно используется в заключении, и, как правило, не априорное значение a подтверждает его. Во втором сценарии значение a, в частности, подтверждает вывод принципа. Итак, в обоих этих двух случаях некоторый x подтверждает вывод.

В-третьих , теперь в отличие от двух пунктов выше рассмотрим случай, когда неизвестно, как доказать или отвергнуть φ. Основной случай - это когда φ является формулой ∃ z θ( z ) , и в этом случае антецедент φ → ∃ x θ становится тривиальным: «Если θ выполнимо, то θ выполнимо». В целях иллюстрации допустим, что θ является разрешимым предикатом в арифметике, то есть для любого заданного числа b утверждение θ( b ) можно легко проверить на предмет его истинностного значения. Более конкретно, θ должно выражать то, что x является индексом формального доказательства некоторой математической гипотезы, доказуемость которой неизвестна. Конечно, здесь один из способов установить ∃ x (φ → θ) — это указать конкретный индекс x, для которого можно показать (затем с помощью предположения, что некоторое значение z удовлетворяет θ), что оно действительно удовлетворяет θ. Однако объяснение такого x невозможно (пока и, возможно, никогда), поскольку такое x в точности кодирует доказательство еще не доказанной или отвергнутой гипотезы.

В интуиционистской логике

Приведенный выше арифметический пример представляет собой так называемый слабый контрпример . Утверждение о существовании ∃ x (φ → θ) не может быть доказано интуиционистскими средствами: возможность проверить x , подтверждающую φ → θ, разрешит гипотезу.

Например, рассмотрим следующий классический аргумент: гипотеза Гольдбаха либо имеет доказательство, либо нет. Если у него нет доказательства, то предполагать, что у него есть доказательство, абсурдно, и из этого следует что угодно — в частности, из этого следует, что оно имеет доказательство. Следовательно, существует некоторый индекс натурального числа x такой, что если предположить, что гипотеза Гольдбаха имеет доказательство, то x является индексом такого доказательства.

К этому вопросу также можно подойти, используя интерпретацию БХК для интуиционистских доказательств, которую следует сравнить с классическим исчислением доказательств. BHK говорит, что доказательство φ → ∃ x θ включает функцию, которая принимает доказательство φ и возвращает доказательство ∃ x θ . Здесь доказательства сами по себе могут выступать в качестве входных данных для функций и, когда это возможно, могут использоваться для построения x . Затем доказательство ∃ x (φ → θ) должно продемонстрировать конкретный x вместе с функцией, которая преобразует доказательство φ в доказательство θ, в котором x имеет это значение. В исчислении доказательств - как и в слабом контрпримере - подходящий x может быть задан только с использованием большего количества входных данных, привязанных к поддающемуся φ.

Действительно, с помощью нарушающих моделей было установлено, что предпосылка φ → ∃ x θ недостаточна для общего доказательства существования, предоставляемого принципом.

Правила

Импликация усиливается, когда антецедент можно ослабить. Здесь интерес представляют посылки в форме отрицательных утверждений φ := ¬η.

Метатеоретически установлено, что если ¬η → ∃ x θ имеет доказательство в арифметике , то ∃ x (¬η → θ) также имеет доказательство.

Неизвестно, применимо ли это также к знакомым теориям множеств .

Для φ без кванторов существования теории интуиционистской логики имеют тенденцию хорошо вести себя по отношению к правилам такого рода.

В классической логике

Как отмечалось, принцип независимости посылки для фиксированного φ и любого θ следует как из доказательства φ, так и из отказа от него. Следовательно, если принять закон дизъюнкции исключенного среднего аксиоматически, принцип справедлив.

Например, здесь ∃ x ((∃ y θ) → θ) всегда выполняется . Более конкретно, рассмотрим предложение:

«Существует такое натуральное число x , что если существует индекс доказательства гипотезы Гольдбаха, то число x является индексом доказательства гипотезы Гольдбаха».

Это классически доказуемо следующим образом: либо индекс для доказательства гипотезы Гольдбаха существует, либо такой индекс не существует. С одной стороны, если он существует, то каким бы ни был этот индекс, он также действует как действительный x в приведенном выше предложении. С другой стороны, если такого индекса не существует, то существование такого индекса противоречит, и тогда из взрыва следует что угодно - и, в частности, из этого следует, что x = 7 является индексом доказательства гипотезы Гольдбаха. В обоих случаях существует некоторый индекс, подтверждающий утверждение.

Конструктивно, необходимо предоставить x такой, чтобы можно было продемонстрировать (затем с помощью φ, предполагаемого действительным, а также ∃ y θ для некоторого y ), что θ выполняется для этого x . Классически достаточно сделать один и тот же интересный вывод, исходя из двух гипотез относительно φ. В последнем подходе утверждается, что некоторый x существует в любом случае, и логика не требует его объяснения.

Пропозициональная логика

Логика Крейзеля-Патнэма

IP и более короткий ∃ x ((∃ y θ) → θ) имеют аналоги в логике высказываний. В интуиционистском исчислении конечная форма

${\big (}\eta \to (\alpha \lor \beta ){\big )}\to {\big (}(\eta \to \alpha )\lor (\eta \to \beta ){\big )}$

можно понимать как выражение этой информации в посылке $\eta$ не требуется устанавливать, какое предложение в паре союзов оно подразумевает. Для $\eta =\alpha \lor \beta$, это сводится к более короткому, но действительно эквивалентному так называемому принципу Дирка Джентли. $(\alpha \to \beta )\lor (\beta \to \alpha )$. Схема подразумевает строго более слабое исключенное среднее для отрицаемых суждений (WLEM) через интуиционистскую форму консеквенции мирабилис .

Логика Крейзеля-Патнэма , полученная путем принятия этой схемы для отрицаемых суждений, т. е. с $\eta =\neg \delta$, все еще обладает свойством дизъюнкции . Соответствующее правило является допустимым правилом .

Ссылки

• Джереми Авигад и Соломон Феферман (1999). Функциональная интерпретация Гёделя («Диалектика») (PDF) . в издании С. Басса, Справочник по теории доказательств, Северная Голландия. стр. 337–405.