全部A的不可证明定理:Prop，~~ A->一种 [英] Unprovable theorem forall A : Prop, ~~A -> A

问题描述

我坚持一个定理，我认为这是不可证明的.

I am stuck with a theorem and I think that it's unprovable.

Theorem double_negation : forall A : Prop, ~~A -> A.  

您能证明它还是解释它为什么不可证明?

Can you prove it or explain why it is unprovable?

是因为哥德尔的不完全性定理吗?

Is it due to Gödel's incompleteness theorems?

推荐答案

双重否定消除是卡住了:

Double negation elimination is not provable in constructive logic which underpins Coq. Attempting to prove it we quickly get stuck:

Theorem double_negation_elim : forall A : Prop, ~~A -> A.
Proof.
  unfold not.
  intros A H.
  (* stuck because no way to reach A with H : (A -> False) -> False *)
Abort.

我们可以显示，如果可以消除双重否定则排除中间定律将成立，即(forall (A : Prop) , (~~A -> A)) -> forall A : Prop, A \/ ~A.

We can show that if double negation elimination was provable then Law of Excluded Middle would hold, that is, (forall (A : Prop) , (~~A -> A)) -> forall A : Prop, A \/ ~A.

首先，我们证明中间结果∼∼(A ∨ ∼A):

Lemma not_not_lem: forall A: Prop, ~ ~(A \/ ~A).
Proof.
  intros A H.
  unfold not in H.
  apply H.
  right.
  intro a.
  destruct H.
  left.
  apply a.
Qed.

因此

Theorem not_not_lem_implies_lem: 
  (forall (A : Prop) , (~~A -> A)) -> forall A : Prop, A \/ ~A.
Proof.
  intros H A.
  apply H.
  apply not_not_lem.
Qed.

但这是一个矛盾，因为LEM在构造逻辑中不成立.

But this is a contradiction as LEM does not hold in constructive logic.

这篇关于全部A的不可证明定理:Prop，~~ A->一种的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！