Независимость помещения - Independence of premise

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

Принцип справедлив в классической логике. Его основное применение - изучение интуиционистской логики, где принцип не всегда верен.

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

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

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

Принцип независимости посылок обычно не действует в интуиционистской логике (Avigad and Feferman 1999). Это можно проиллюстрировать Толкование BHK, в котором говорится, что для доказательства φ → ∃ Икс θ интуиционистски нужно создать функцию, которая принимает доказательство φ и возвращает доказательство ∃ Икс θ. Здесь само доказательство является входом в функцию и может использоваться для построения Икс. С другой стороны, доказательство ∃ Икс (φ → θ) должен сначала продемонстрировать конкретный Икс, а затем предоставить функцию, которая превращает доказательство φ в доказательство θ, в котором Икс имеет эту особую ценность.

Как слабый контрпример, предположим θ (Икс) - некоторый разрешимый предикат натурального числа такой, что неизвестно, есть ли Икс удовлетворяет θ. Например, θ может сказать, что Икс является формальным доказательством некоторой математической гипотезы, доказуемость которой неизвестна. Пусть φ формула ∃ z θ (z). потом φ → ∃ Икс θ тривиально доказуемо. Однако чтобы доказать ∃ Икс (φ → θ), необходимо продемонстрировать особую ценность Икс так что, если любое значение Икс удовлетворяет θ, то тот, который был выбран, удовлетворяет θ. Это невозможно сделать, не зная, ∃ Икс θ имеет место, и таким образом ∃ Икс (φ → θ) не доказуемо интуитивно в этой ситуации.

Рекомендации

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