类型论与coq (5-5)

这个时候我们需要做的是证明Πx：A fαlse，就像我们前文所说的，这里我们其实可以固定一个x：A只不过我们没有任何额外的关于x的信息，所以我们可以

move =＞ x.

在然后我们会发现我们现在要的东西变成了P(x) → fαlse，所以我们还可以

move =＞ Px.

这个时候我们看看我们都有什么已知的东西：

nx : ~ (exists x : nat, P x)

x : nat

px : P x

而我们要的是一个False，那我们已有的里面谁的值域是False呢，自然是nx，所以我们使用

apply nx.

这个时候我们要的变成了nx的定义域也就是

exists x0 : nat, P x0

于是我们只需要

exists x.

apply px.

就行了，完整代码如下：

Lemma q2 : ~(exists x, P x) -＞ forall x, ~P x.

Proof.

move =＞ nx x px.

apply nx.

exists x.

apply px.

Qed.

现在我们给出如下公理

Axiom DNE : forall A : Prop, ~(~A) -＞ A.

然后留两个习题

Lemma excluded_middle : forall A:Prop, A \/ ~A.

Lemma drinker_paradox (P : nat -＞ Prop) :

exists x : nat, forall y : nat, P x -＞ P y.

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。