현대 수리기초론은 같은 현상을 표현하는 여러 가지 방법으로 이루어져 있다고 할 수 있다. (Curry–Howard–Lambek correspondence를 고려하면) 이 사실은 인류가 오랜 시간 발전시켜 온 여러 직관들이 보편적인 논리적 구조를 갖추고 있다는 사실을 의미한다.
| First-Order Logic | Set Theory | Type Theory | Category Theory |
|---|---|---|---|
| (meta-theory) Provability of a proposition | Set Membership | Type & Membership | (meta-theory) Collection and Collection Membership |
| Proposition | Set | Type | Object |
| Logical Implication | Function | Lambda Function | Morphism |
| Hypothetical Syllogism | Function Composition | Lambda Function Composition | Morphism Composition |
| Deductive System | - | Type Universe | Category |
| - | Power Set | Higher Type Universe | Category of Category & Functor Category |
| Conjunction | Cartesian Intersection | Product Type | Product Category |
| Disjunction | Disjoint Union | Sum Type | Coproduct Category |
| Universal Quantifier | Indexed Set Intersection | Dependent Product Type | Right Adjoint |
| Existential Quantifier | Indexed Set Union | Dependent Sum Type | Left Adjoint |
독서목록
- Seven Sketches in Compositionality (117p)
- 인간관계론 (42%; 105p)
- 서양철학사 3부(32%; 946p)
- Understand Machine Learning (16%; 72p)
- Dune (44%)