이 멘토링이 철학과 무슨 상관이 있는지가 궁금하실 수 있는데, 상호 작용 정리 증명기(증명 보조기)는 형식 철학을 연구하는 데 활용할 수 있습니다.
형식 철학과 증명 보조기
형식 철학
전통적인 철학 문제를 연구하고자 수학의 엄밀한 도구에 의지하는 연구 전통. (Dolgorukov and Shumilina 2021, 235)
논리학, 수학, 컴퓨터 과학, 언어학, 물리학, 생물학, 경제학, 게임 이론, 정치론, 심리학 등의 연구 방법을 활용함.
형식 철학의 주제
논리학: 비단조 논리, 양상 논리 등
형식 인식론: 인식 논리, 신념 변화, 베이즈 인식론 등
계산 형이상학: Computational Metaphysics
추상적 대상 이론: GitHub - ekpyron/AOT: Embedding of The Theory of Abstract Objects in Isabelle/HOL
과학 철학: 과학 이론 발전에 대한 모형, 일반 상대성 이론이 허용하는 가능 세계의 성질 (Hansson and Hendricks 2018, chap. 26)
가치론과 도덕 철학: 가치론, 선호와 선택, 선호 변화, 규범 논리
결정 이론과 사회 철학…
제 멘토링을 통해 린 정리 증명기의 이용법을 배우신 멘티 가운데 철학의 형식화에 관심 있는 분들은 컨트리뷰션 아카데미가 끝난 뒤에 저와 함께 형식 철학 학습 모임을 가지셔도 좋을 듯합니다. 제가 예전에 구상한 증명 보조기 학습 모임을 진행할 수도 있고, 아래의 참고 문헌 목록에 있는 형식 철학 입문서를 함께 읽을 수도 있어요.
증명 보조기 학습 모임에 대한 구상
증명 보조기를 이용해 수학·논리학·이론 컴퓨터 과학·철학을 비롯한 여러 분야의 이론을 배우거나 형식화하고 싶은 분들을 위해 나중에 학습 모임을 운영하고자 합니다. 가능하면 추가로 교육 영상도 제작하고 인터넷 방송도 하고 싶어요.
아쉽게도 현재로서는 고교·대학 수준의 논리학을 모르는 초보자가 증명 보조기와 논리학을 동시에 배울 수 있는 학습 자료가 없는 듯해요. 간단히 말해, 쉬운 교재가 없습니다.
제가 구상한 학습 모임은 다음과 같습니다. 아래의 내용은 나중에 바뀔 수 있으며, 아직 참가자를 모집하는 것이 아닙니다. 본격적으로 학습 모임을 시작하기 전에 음성 및 영상 편집을 더 배우고 싶어요.
호모토피 유형론 배우기
이용할 증명 보조기와 라이브러리
코크(Coq) 증명 보조기
Coq-HoTT : 호모토피 유형론[HoTT]을 위한 코크 라이브러리
읽을 자료
소프트웨어 기초론 1권: 논리적 기초
호모토피 유형론: 수학의 한값[一價, unival…
참고 문헌