型と論理

型と論理(Types and Logic)

$ \begin{array}{c|c} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) \\ \hline A & \text{命題}P \\ a: A & \text{証明}p : P & \\ B(x) & \text{述語}P(x) \\ b(x) : B(x) & \mathrm{条件付き証明} \\ \bm{0} & \bot \\ \bm{1} & \top \\ A + B & A \lor B \\ A \times B & A \land B \\ A \to B & A \implies B\\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) \\ \prod_{(x:A)}B(x) & \forall_{x:A} B(x) \\ \mathrm{Id}_A & 等号\ = \end{array}

型Aと、命題P

型Aの項aと、命題Pの証明p

依存型B(x)と、述語P(x)

依存型理論のレベルでは、直観主義述語論理と依存型理論

確認用

Q. 型と論理

参考

メモ

調査用

Wikipedia.icon

Wikipedia.icon