判断
判断(judgment)
型理論の判断について
「判断」は以下のような構文で書かれているものが判断になる
文脈 ⊢ 結論
$ \Gamma \vdash \text{conclusion}
いろいろ見てうまく処理できなかったけれど、単に構文(syntax)の一つとして考えるのが良さそう。哲学的部分？はおいおい調べる
どんなものが判断か
「Aは真である」
「Aは論理式である」
Martin-Löf型理論だと以下のようなもの？$ ^{(1)}
A is a set (Aは集合)
A1 and A2 are equal sets (A1とA2は等しい集合である)
a is an element in the set A (aは集合Aの要素である)
a1 and a2 are equal elements in the set A (a1とa2は集合Aにおいて等しい要素である)
$ \Gamma \vdash \text{conclusion}
$ \Gamma : 文脈
$ x_1 : A_1,...,x_n :A_n \vdash t:A
$ x_1,...,x_n : 変数
$ A_1,...A_n 、$ A : 型
項$ t
読み方の例: 変数$ x_1 から$ x_n が型$ A_1 から$ A_n であると仮定すると、項$ t は型$ A を持つ
確認用
Q. 判断
関連
シーケント計算
参考
(1) Nördstrom, B., Petersson, K. “Programming in Martin-Löf ’s type theory”. Handbook of Logic in Computer Science: Volume 5. Algebraic and Logical Structures. Oxford University Press, 2001, ISBN978-0-19-853781-6. , (参照 2025-01-01).
(2) 水上 達夫. 2001-11-01. "数学基礎論特論 (コンピュータ特別講義 I) 講師 龍田 真". http://www.yl.is.s.u-tokyo.ac.jp/~tatsuo/types/types20011101.pdf , (参照 2024-11-03).
P9
『型理論I』龍田 真
MaruLabo . "「同じ」を考える -- 「型の理論」入門". https://drive.google.com/file/d/1D_stE1LAcdTxQl6CAEZ4wrx1DCxXzP0x/view , (参照 2024-11-03)
Univalent foundations and the equivalence principle - Benedikt Ahrens
https://www.youtube.com/watch?v=okx4Uklvwco
メモ
「型の理論」入門 (4) -- 論理的推論（１）判断と論理式
https://www.youtube.com/watch?v=1QnJRWLgOvI&list=PLQIrJ0f9gMcPC8_eEnysTwZm14VRaQWCT
「型の理論」 入門 (5) 論理的推論(2) 推論ルール -- Natural Deduction
judgment in nLab
調査用
Google.icon 判断(日)
Google.icon Justification(英)
Wikipedia.icon
判断 - Wikipedia(日)
判断(検索) - Wikipedia(日)
Wikipedia.icon
Justification - Wikipedia(英)
Justification(検索) - Wikipedia(英)