0

ダメットの法則

8
0
$$$$

hbhb bbk hbhb bbk

imp

$$ imp(a\ b:Prop):=a\rightarrow b\ . $$

total

$$ total\ U\ R:=\forall x\ y:U,R\ x\ y\lor R\ y\ x\ . $$

em

$$ em \ a:=a\lor \lnot a\ . $$

$$ (\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.
    
投稿日:20201126

この記事を高評価した人

高評価したユーザはいません

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

バッジはありません。

投稿者

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中