Доказательство (~ A -> ~ B) -> (~ A -> B) -> A в Coq - PullRequest
Новая
       12

Доказательство (~ A -> ~ B) -> (~ A -> B) -> A в Coq

3 голосов
/ 19 марта 2019

Я пытался доказать следующую тавтологию в Coq. 

Theorem Axiom3: forall A B: Prop, (~A -> ~B)-> ((~A -> B) -> A).

Мой план состоял в следующем 

Theorem Axiom3: forall A B: Prop, (~A -> ~B)-> ((~A -> B) -> A).
Proof.
  intros A B.
  unfold not.
  intros nA_implies_nB.
  intros nA_implies_B.
  pose (proof_of_False := nA_implies_nB nA_implies_B).
  case proof_of_False.
Qed.

Тем не менее, вот где мои проблемы. 

 pose (proof_of_False := nA_implies_nB nA_implies_B).

Я не могу просто составить следующее, чтобы получить доказательство ложности. 

nA_implies_nB : (A -> False) -> B -> False
nA_implies_B : (A -> False) -> B

Может ли мое доказательство быть адаптировано для создания или исправления или есть простой способ доказать эту теорему?

1 Ответ

2 голосов
/ 19 марта 2019

Это утверждение эквивалентно принципу исключенного среднего , который гласит, что A \/ ~A выполняется для любого предложения A. Исключенная середина печально известна своим отсутствием в Coq и других системах, основанных на конструктивной математике. Чтобы доказать утверждение в Coq, вы должны явно объявить, что вы хотите принять неконструктивные рассуждения. 

Require Import Coq.Logic.Classical.

Theorem Axiom3: forall A B: Prop, (~A -> ~B)-> ((~A -> B) -> A).
Proof. intros A B. tauto. Qed.

Если вы закомментируете первую строку, вы увидите, что доказательство не удалось, потому что Coq не будет пытаться использовать исключенную середину в доказательстве.

Если вам интересно, вот более явное доказательство того, как Axiom3 подразумевает исключенную середину: 

Axiom Axiom3: forall A B: Prop, (~A -> ~B)-> ((~A -> B) -> A).

Lemma classical : forall A : Prop, A \/ ~ A.
Proof.
intros A.
apply (Axiom3 (A \/ ~A) (A \/ ~A)).
- trivial.
- intros H. exfalso.
  assert (H' : ~ ~ A).
  { intros HA. apply H. right. trivial. }
  apply H'. intros HA. apply H. left. trivial.
Qed.
...