Является ли эта связь между фоллом и существует доказуемой в 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, поэтому, возможно, я просто упускаю что-то очевидное.

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

Источник

2 ответа

Решение

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

Мои навыки 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)
Источник

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

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

Если предположить, not (forall x, not (P x)) имеет примерно интерпретацию "если я предполагаю, что P не выполняется для всех х, тогда я получаю противоречие ", но это слабее, чем вы хотите, построение модели покажет, что предположение не содержит достаточно информации, чтобы выбрать свидетеля для P,

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

Источник
Другие вопросы по тегам