형식 철학과 증명 보조기

[chabulhwi]

형식 철학과 증명 보조기

형식 철학

• 전통적인 철학 문제를 연구하고자 수학의 엄밀한 도구에 의지하는 연구 전통. (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)
• 가치론과 도덕 철학: 가치론, 선호와 선택, 선호 변화, 규범 논리
• 결정 이론과 사회 철학: 동적 결정 이론, 인과 결정 이론, 사회 선택 이론

증명 보조기를 철학 연구에 활용할 수 있는가

이저벨 증명 보조기의 활용 사례

Logic/Philosophical aspects

이저벨(Isabelle) 증명 보조기로 다음 이론이 형식화됐습니다.

• 신 존재 증명
• 추상적 대상 이론
• 포괄적 일관성 원리
• 아리스토텔레스의 주장적 삼단 논법
• 부분 전체론
• 조지 불로스(George Boolos)의 기묘한 추론
• 조건부 규범 추리

'기존 철학'을 연구하는 데 활용할 수 있는가

@sophisten

시간이 괜찮으시다면, <증명보조기>가 정확히 무엇이고 또 어떤 방식으로 굴러가는지, 대표적인 보조기가 무엇이고 또 그것이 기존 철학에 기여할 수 있는 것이 무엇인지 한번 글을 통해 듣고 싶습니다.
딴죽을 거는게 아니라, 저는 글쓴이 님이 올리시는 글들을 보기 전에 <증명보조기>라는게 있는지도 모르고 살았습니다. 저 뿐만 아니라 일반적인 방식으로 철학을 쭉 공부하신 분들에겐 생소한 것이라는 생각이 듭니다. 한번 얘기를 들어보고 싶습니다.

"증명 보조기가 기존 철학의 연구에 활용될 수 있는가?"라는 물음의 답은 어디부터 어디까지가 '기존 철학'의 범위에 들어가는지에 따라 달라질 듯합니다. 하지만 세계에 널리 알려진 중요한 철학 이론 중에서 많은 것이 형식화하기 어려워 보인다고 저는 생각합니다. 형식화하기 어려운 이론은 증명 보조기로 재서술하기도 어렵습니다.

제가 보건대, 그런 철학 이론에서 영감을 받아 새로운 형식 철학 이론을 만드는 편이 차라리 더 쉬울 듯해요. 물론 이것도 그리 쉬운 일이 절대 아닙니다. 해당 철학 분야를 잘 이해해야 할 뿐만 아니라 증명 보조기를 잘 다룰 수 있어야 하니까요. 저는 "린 4로 하는 정리 증명"과 린 라이브러리의 몇몇 코드를 읽는 데 대략 373시간을 들였어요. 제가 원래 학습 속도가 느린 편이긴 하지만요.

참고 문헌

• Dolgorukov, Vitaly V., and Vera A. Shumilina. 2021. “What Is Formal Philosophy?” Epistemology & Philosophy of Science 58, no. 1. https://www.pdcnet.org/eps/content/eps_2021_0058_0001_0235_0241.
• Hansson, Sven Ove, and Vincent F. Hendricks, ed. 2018. Introduction to formal philosophy. New York: Springer. https://doi.org/10.1007/978-3-319-77434-3.

[Ruby]

글 잘 읽어보았습니다. 저도 철학적 물음을 해결하기 위해 수학이나 컴퓨터를 도구로서 활용하는 것에 관심이 있는데요. 제가 알기로는 증명 보조기는 연역 논증의 타당성을 검증하는 데 도움을 주는 것으로 알고 있습니다. 그렇다면,

(1) 귀납 논증을 중점적으로 활용하는 철학에서 증명 보조기가 그 힘을 발휘할 수 있을까요?
(2) 연역 논증을 검증하기 위해 증명 보조기를 활용한다면, 굳이 증명 보조기가 없어도 사람의 이성만으로 그 타당성을 보일 수 있지 않을까요? 증명 보조기를 활용하기 위해서는 쉽지 않은 코드 작성이 필요한데, 이것이 사람이 직접 검증하는 것에 비해 수고를 더 들여도 가치 있을만한 활동인지 의문이 드네요.

[chabulhwi]

@Ruby

(1) 귀납 논증을 중점적으로 활용하는 철학에서 증명 보조기가 그 힘을 발휘할 수 있을까요?

"형식 철학 입문" 학부 교과서의 5장 '귀납'을 보니, 귀납 논증에 관한 이론은 증명 보조기로 서술할 수 있을 듯합니다. (Hansson and Hendricks 2018, chap. 5)

(2) 연역 논증을 검증하기 위해 증명 보조기를 활용한다면, 굳이 증명 보조기가 없어도 사람의 이성만으로 그 타당성을 보일 수 있지 않을까요?

사람의 이성만으로 그 논증의 타당성을 보일 수는 있습니다. 그런데 사람의 착오가 문제입니다. 사람은 정의를 잘못 내리고, 정리를 잘못 진술하고, 정리를 증명하면서 오류를 범합니다. 증명 보조기를 활용하면 증명 안의 오류를 제거할 수 있습니다. 가끔 증명 보조기의 신뢰성 문제가 생기기는 하지만, 증명 보조기는 사람보다 더 믿을 만합니다.

증명 보조기를 활용하기 위해서는 쉽지 않은 코드 작성이 필요한데, 이것이 사람이 직접 검증하는 것에 비해 수고를 더 들여도 가치 있을만한 활동인지 의문이 드네요.

저는 증명 보조기를 쓸 줄 알기 전에도 자꾸 수학 증명을 형식적으로 쓰려고 해서 고생했습니다. 이런 경우에는 증명 보조기를 쓰는 편이 고생을 훨씬 덜어 줍니다. 현재 대부분의 수학 전공자는 지나치게 엄밀하게 수학 증명을 작성하지 말라고 조언하겠지만요. 저는 형식 증명을 읽고 쓸 때 이론을 더 잘 이해한다고 느꼈습니다.

어떤 이론을 만든 사람이 증명 보조기로 그 이론을 이미 검증하면, 그 사람을 뺀 나머지 모두는 고생을 덜 하게 됩니다. 그 이론을 검토하고 싶은 사람들은 정의와 정리 진술이 올바른지만 확인해도 되니까요. 증명 보조기가 검증한 증명이 실제로 틀릴 가능성은 작습니다.

어떻게 해야 증명 검증기를 신뢰할 수 있는지는 마리오 카네이로 박사 후 연구원님이 자신의 박사 논문 도입부에서 설명하셨습니다.

증명 보조기를 활용해 자신의 이론을 아주 엄밀하게 검증하다 보면 새로운 깨달음을 얻기도 합니다. 예를 들어, 저는 린 표준 라이브러리의 문자열 정리 String.splitOn_of_valid를 증명하려고 여러 보조 정리를 만들다가 String.splitOn 함수를 정의하는 새로운 방법을 생각해 냈어요. 제가 만든 보조 정리가 사실상 제게 새 정의를 알려 준 셈이었습니다.