![hbhb bbk](/uploads/mathdown/20201126194008.jpg)






&&&def imp
$$
imp(a\ b:Prop):=a\rightarrow b\ .
$$
&&&


&&&def total
$$
total\ U\ R:=\forall x\ y:U,R\ x\ y\lor R\ y\ x\ .
$$
&&&



&&&def em
$$
em \ a:=a\lor \lnot a\ .
$$
&&&




&&&exc 
$$
(\forall a,em\ a)\rightarrow total\ imp\ .
$$
&&&


```
Require Import Utf8.

Set Implicit Arguments.

Definition imp(a b:Prop):=a → b.

Definition total U R:=∀x y:U,R x y∨R y x.

Definition em a:=a∨¬a.

Goal (∀a,em a) → total imp.
Proof. Abort.
```

ダメットの法則

この記事を高評価した人

この記事に送られたバッジ

投稿者

コメント

他の人のコメント