Доказуема ли эта связь между всем и существованием в интуиционистской логике Coq?

Доказуема ли в Coq следующая теорема? А если нет, есть ли способ доказать, что это недоказуемо?

Theorem not_for_all_is_exists:
    forall (X : Set) (P : X -> Prop), ~(forall x : X, ~ P x) -> (exists x: X, P x).

Я знаю, что это родственное отношение верно:

Theorem forall_is_not_exists : (forall (X : Set) (P : X -> Prop), (forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
  (* This could probably be shortened, but I'm just starting out. *)
  intros X P.
  intros forall_x_not_Px.
  unfold not.
  intros exists_x_Px.
  destruct exists_x_Px as [ witness proof_of_Pwitness].
  pose (not_Pwitness := forall_x_not_Px witness).
  unfold not in not_Pwitness.
  pose (proof_of_False := not_Pwitness proof_of_Pwitness).
  case proof_of_False.
Qed.

Но я не уверен, что это поможет мне без двойного отрицательного исключения. Я также поигрался с доказательством рассматриваемой теоремы, используя разные подходы, но безрезультатно. Я только изучаю Coq, так что, возможно, я просто упускаю что-то очевидное.

N.B. Мне хорошо известно, что это верно для классической логики, поэтому я не ищу доказательства, которые добавляют дополнительные аксиомы к базовой системе.


logic implication coq
person Others    schedule 20.02.2016    source источник

Ответы (2)


arrow_upward
7
arrow_downward

Это не доказуемо, потому что это эквивалентно исключению двойного отрицания (и другим классическим аксиомам).

Мои навыки Coq в настоящее время очень устарели, но я могу быстро проиллюстрировать, почему ваша теорема подразумевает исключение двойного отрицания.

В своей теореме создайте экземпляр X в unit и P в fun _ => X для произвольного X : Prop. Теперь у нас есть ~(unit -> ~ X) -> exists (u : unit), X. Но из-за тривиальности unit это эквивалентно ~ ~ X -> X.

Обратная импликация может быть доказана прямым применением исключения двойного отрицания на ~ ~ (exists x, P x).

Моя Agda намного лучше, поэтому я могу хотя бы показать там доказательства (не знаю, полезно ли это, но это может немного подкрепить мои утверждения):

open import Relation.Nullary
open import Data.Product
open import Data.Unit
open import Data.Empty
open import Function

∀∃ : Set _
∀∃ = (A : Set)(P : A → Set) → ¬ (∀ x → ¬ P x) → ∃ P

Dneg : Set _
Dneg = (A : Set) → ¬ ¬ A → A

to : ∀∃ → Dneg
to ∀∃ A ¬¬A = proj₂ (∀∃ ⊤ (const A) (λ f → ¬¬A (f tt)))

fro : Dneg → ∀∃
fro dneg A P f = dneg (∃ P) (f ∘ curry)
person András Kovács    schedule 20.02.2016

arrow_upward
5
arrow_downward

Ваше not_for_all_is_exists предложение невозможно доказать в Coq. Я рекомендую прочитать начало главы 5 «Логики и структуры» Дирка Ван Далена для более глубокого объяснения.

В интуиционистской логике (и таких системах, как Coq), чтобы доказать exists x, P x, вы должны предоставить метод (или алгоритм), который построит реальный x, так что P x будет выполняться.

Предполагая, что not (forall x, not (P x)) имеет приблизительную интерпретацию «если я предполагаю, что P не выполняется для всех x, тогда я получаю противоречие», но это слабее, чем ваш желаемый вывод, построение модели покажет, что предположение не содержит достаточно информации, чтобы Выберите свидетеля для P.

Однако следует сказать, что этот принцип выполняется в Coq для ограниченных классов P и X, конкретный пример - когда P является разрешимым предикатом, а X - конечным типом.

person ejgallego    schedule 20.02.2016