Prop - pogi-log

Prop

Prop

命題を表す型

$ P \land Q \rightarrow Q \land P : \text{Prop}

bool ≠ Prop

Propは「証明可能」か「証明不能」

code:lean

#check And -- Prop → Prop → Prop

#check Or -- Prop → Prop → Prop

#check Not -- Prop → Prop

#check Implies -- Prop → Prop → Prop

variable (p q r : Prop)

#check And p q -- Prop

#check Or (And p q) r -- Prop

#check Implies (And p q) (And q p) -- Prop

Bool, Propの違い

Bool と Prop の違い

どちらも言明に対応するため、Bool と似ているようですが以下のような目立つ相違点があります：

1. Prop の項はそれ自身が型であるため、Prop は型宇宙であると言われます。Bool の項は型ではありません。

2. Prop の項は True か False のどちらであるかを判定するアルゴリズムがあるとは限りません。Bool の項は簡約すれば必ず true か false になります。

確認用

Q. Prop