1910년 『Principia Mathematica』에서 람다 계산·참조 투명성·타입의 선구적 개념을 읽다

실제로 이 기획의 중심에는 나중에 괴델이 밝혀낸 큰 논리적 문제가 있음. 다만 저자들이 독자를 골리려고 심어 둔 오류는 아니지.

학부 논리학 수업에서 필독서였고, 집합론 선택 과목에서도 사실상 필독이었음. 수학사나 수리철학 수업에서도 흔히 다루더라.

작년에는 Principia를 Lean으로 형식화한 Show HN이 있었고, Principia Rewrite는 원문 증명 개요를 기준으로 명제논리 1-5절의 정리 189개를 Coq로 검증했음.

이 책에 바로 들어가기 전에는 러셀의 Introduction to Mathematical Philosophy가 더 읽기 쉬운 입문서임. 읽기 편한 PDF도 공개돼 있음.

나는 Frege의 Begriffsschrift 쪽 표기를 더 좋아함. 표기가 정말 창의적이었는데, 러셀이 그 프로젝트를 평가절하한 뒤 역사에서 밀려난 점은 아쉬움.

러셀과 화이트헤드에 매달리기보다 HoTT Book을 읽는 편을 권함. 종속 타입도 재미있지만 고차 귀납 타입은 훨씬 더 충격적이고, 함수형 언어와의 연결도 더 직접적임.

결국 괴델의 불완전성 정리가 무너뜨린 수학의 기초화 시도가 TypeScript 프로그래머에게도 도움이 될 수 있다는 얘기인가 보네. 오늘 하나 배움.