명제 p가 "차불휘는 린 정리 증명기를 다룰 줄 안다."라는 문장을 가리킨다고 가정할게요. 그러면 p → p라는 조건문은 "차불휘가 린 정리 증명기를 다룰 줄 알면, 차불휘는 린 정리 증명기를 다룰 줄 안다."라는 명제를 가리킵니다. 두 명제 p와 p → p의 유형은 모두 Prop이라는 유형 세계예요.
그런데 함수 fun (hp : p) ↦ hp의 유형은 조건문 p → p입니다. 이 함수의 정의역과 공역은 모두 명제 p라는 유형이기 때문이죠. 따라서 이 함수는 p → p라는 명제의 증명이에요.
fun이나 ↦가 어떤 연산자인지를 설명을 해주셨으면 보다 편히 읽을 수 있었겠다고 생각이 듭니다.
그나저나 Typed logic에 기초한 증명 보조기에 대해 양가적인 마음이 듭니다. 불필요한 형이상학적 개입 없이 문장들을 형식화하기 위해 유용한 방법이고, 전산학의 발전 때문인지 지금의 우리에게는 고차 논리학에 대한 ‘은폐된 집합론’이라는 콰인의 회의론에 공감하지 않으면서도 Typed logic을 받아들일 마음가짐이 있는 것 같습니다. 이런 점들은 좋습니다.
그런데 두 측면에서의 회의감도 있습니다. 한편으로는, Typed logic을 (아마도 차불휘님이 의도하시는 듯한) 논리학 학습의 툴로 사용하는 것이 과연 가능할까 싶습니다. 논리학을 가르치거나 배우면서 우리가 느끼는 것은, 일차 논리조차도 쉽게 배우고 가르칠 수 없다는 것입니다. 명제 논리 정도가 직관적으로 받아들일 수 있는 한계인 듯합니다. 조금 더 재능이 있다면 일차 논리를 어느 정도 쉽게 받아들일 수 있고요.
한편 이미 일차 논리에 대해 잘 이해하고 있지 않다면, Typed logic을 배우는 것이 가능할지 의문입니다. 학습자는 이미 연산자의 개념이나 함수의 개념을 이해하고 있어야 Typed logic을 배울 수 있을 것 같은데, 사실상 그런 개념을 이해하기 위해 필요한 것이 일차 논리의 학습입니다. 그래서 논리학에의 입문을 더 어렵게 만드는 것이 아닌가 싶은 회의감을 느낍니다.
다른 쪽에서의 회의감은, 증명 보조기가 철학자들에게 큰 쓸모가 있을지 모르겠다는 것입니다. 많은 철학적 논쟁들은, 실상 어떠한 것이 증명 가능한지가 아니라 어떠한 명제를 어떤 식으로 형식화하는 것이 옳은지에 관한 것처럼 보이곤 합니다. 일단 형식화가 마무리되고 나면, 그 이후의 증명은 크게 어렵지 않은 것이 보통입니다. (차불휘님이 관심갖고 계시는 듯한, 수학 기초론의 영역에서는 이 점이 해당하지 않을 것도 같습니다.)
그렇다면 증명 보조기의 역할은 사실상 전문 철학자들보다는 철학도들에게 더 클 텐데, 철학도들이 증명 보조기를 사용하는 것은 또 과연 유용한가, 의문이 듭니다. 결국 스스로 형식 체계를 이해하고 증명을 구성하는 것이 철학을 배우는 한 과정인 것 같아서요. 형식 체계의 이해를 위해 증명 보조기를 쓸 수 있지 않을까?, 묻는다면 이는 첫째 회의론으로 이행하게 됩니다.
여러모로 하시는 작업이 흥미롭게 보이기는 하는데, 또 한편으로는 잘 모르겠고… 하는 생각이 들어 말씀 남겨보았습니다.
이 설명을 윗글에 넣을 걸 그랬네요. 식 fun (x : α) ↦ f x는 유형 α에 속하는 입력값 x에 대해 f x라는 값을 반환하는 함수를 나타냅니다. 여기서 f x는 x에 대한 식입니다. 이런 꼴의 식을 익명 함수[anonymous function]나 람다 함수(lambda function)라고 부릅니다. 그리고 이런 함수를 만드는 일을 함수 추상화[function abstraction]라고 일컫습니다.
앞에서 말한 식 f x가 유형 β에 속한다면, 함수 fun (x : α) ↦ f x의 유형은 α → β입니다. 다시 말해, 이 함수는 유형 α에서 유형 β로의 함수입니다. 유형 α와 β는 각각 이 함수의 정의역과 공역입니다.
제가 지금 제 멘티들의 퀴즈 답안을 검토해야 돼서, @car_nap 님이 쓴 댓글의 나머지 부분은 이따가 읽고 답하겠습니다.
람다 추상화를 ↦을 통해 의미하는 거군요. 그런데 그렇다면, fun (hp : p) ↦ hp 는 하나의 식이라기보다는 하나의 정의 아닌가요? 즉 fun =def. (𝜆x.x)라는 형태로 표현 가능한 메타언어 문장일 텐데, 이게 어떻게 어떤 조건문의 증명이 되는지가 분명히 다가오지가 않네요. 린에서 “증명”을 어떻게 정의하길래 이런 것이 가능한 것인지...
음, 두 용어 '단순 유형론[simple type theory]'과 '고차 논리[higher-order logic]'는 동의어로 쓰일 때가 있다는 걸 아시나요? 저는 콰인이 왜 "고차 논리가 은폐된 집합론이다."라는 지적을 했는지 잘 모르지만, 왠지 이 말이 맞는 거 같아요. 유형론이 집합론 대신에 수학을 형식화하기 위한 기초론으로서 잘 쓰인다는 점이 그 정황 증거가 되지 않을까요?
유형론을 배우는 일도 논리학을 배우는 일이라는 점을 먼저 얘기하고 싶습니다. 유형론도 논리학의 한 분야로 여겨지니까요. 그저 한국에서는 몇몇 대학의 컴퓨터 공학과 말고는 유형론을 가르치는 수업을 찾기가 어려운 거죠.
논리학을 가르치거나 배우면서 우리가 느끼는 것은, 일차 논리조차도 쉽게 배우고 가르칠 수 없다는 것입니다. 명제 논리 정도가 직관적으로 받아들일 수 있는 한계인 듯합니다. 조금 더 재능이 있다면 일차 논리를 어느 정도 쉽게 받아들일 수 있고요.
학습자가 명제 논리와 일차 논리를 먼저 배우지 않고, 처음부터 유형론을 배우는 일은 당연히 어렵습니다. 그래도 제가 학습자에게 유형론을 일찍 가르치는 시도를 하는 이유는, 그 학습자가 이른바 '컴퓨터 보조 증명'의 혜택을 빨리 누릴 수 있기를 제가 갈망하기 때문이겠죠.
한편 이미 일차 논리에 대해 잘 이해하고 있지 않다면, Typed logic을 배우는 것이 가능할지 의문입니다. 학습자는 이미 연산자의 개념이나 함수의 개념을 이해하고 있어야 Typed logic을 배울 수 있을 것 같은데, 사실상 그런 개념을 이해하기 위해 필요한 것이 일차 논리의 학습입니다. 그래서 논리학에의 입문을 더 어렵게 만드는 것이 아닌가 싶은 회의감을 느낍니다.
아랫글에서 설명하다시피, 함수는 적어도 린의 유형론에서 원시 개념입니다.
Riccardo Brasca said:
There might be a way of doing it, but I think the general principle is to not mess up with things in
core. Note that docs#function.comp is not a special case of composition in a category: functions are a primitive notion in type theory, they are not literally morphisms in the category of sets. (Of course there is category of sets with its hom, but these are denoted with a slightly different arrow⟶.)
그래서 저는 학습자가 일차 논리를 미리 알아야만 '원시 개념으로서의 함수'를 이해할 수 있다고 생각하지 않습니다. 대부분의 연산은 린의 유형론에서 커링(currying)을 이용해 정의할 수 있으니, 학습자가 유형론으로 연산을 정의하는 법을 이해하기 위해 미리 알아야 되는 건 함수 추상화, 함수 유형 그리고 커링이에요.
하지만 @car_nap 님이 제게 진정으로 묻는 바는 "명제 논리와 일차 논리를 배우지 않은 학습자가 자신이 아직 모르는 개념과 마주치지 않으면서 유형론을 학습할 수 있는가?"라는 물음 같습니다. 이 물음은 다음과 같이 일반화할 수 있겠죠.
이론
T를 이해하는 데 충분한 배경지식을 갖추지 않은 임의의 학습자l에 대해, 교재m은 학습자l이 아직 모르는 지식을 설명 없이 도입하지 않으면서 이론T를 학습자l에게 가르칠 수 있는가?
이론 T가 '증명 보조기를 다루기 위한 형식 이론'일 때, 위의 성질을 충족하는 동시에 논리학 입문서로도 쓰일 수 있는 교재 m을 어떻게 만들어야 하냐는 문제로 제가 2013년부터 고민해 왔습니다. 과장을 약간 넣고 말하면 말이죠.
아직 저도 정확한 답은 모르고, 이 답을 찾는 게 제 일생의 핵심 목표라고 단언합니다. 수학, 논리학, 컴퓨터 과학 학습의 '적절한 시작점'을 찾는 일 말이죠. 앞에서 말한 '증명 보조기를 다루기 위한 형식 이론' 중에서 제가 아는 현실적인 후보는 유형론밖에 없으니, 교재 m이 유형론 입문서이기도 할 때만을 고려할게요.
교재 m이 학습자에게 유형론을 다 설명한 뒤에 명제 논리와 일차 논리를 알려 주면 당연히 안 됩니다. 유형론을 설명하는 가운데 명제 논리와 일차 논리를 다뤄야 돼요. 그래서 제가 추측해 보자면, 교재 m은 명제 논리와 일차 논리의 기초 내용을 설명하기 전에 유형론의 어떤 일부를 학습자에게 가르쳐야 할 겁니다. 지금 제가 이와 비슷한 방식으로 멘티분들에게 린의 유형론, 명제 논리, 일차 논리를 설명하고 있어요. 하지만 제가 정말로 원하는 교재는 본 적이 없고, 아직은 제가 직접 만들어 내지도 못했어요.
그나저나 저는 아직 영어보다 한국어로 제 생각을 훨씬 더 잘 풀어 쓰는 거 같네요. 영어 학습도 더 해야죠.
식 λx.x를 린에서는 λ (x : p) => x나 fun (x : p) ↦ x와 같이 나타낸다는 점도 제가 설명할 걸 그랬네요. 저는 오히려 λx.x 꼴의 식이 낯설어요. 아마 린 핵심 개발진은 수학자들이 선호할 만한 표기법을 고른 듯해요. 어쨌든 식 fun (x : p) ↦ x는 메타언어 문장이 아닐 거예요. 이게 그렇다면 식 λx.x도 메타언어 문장입니다.
예전에 제가 쓴 글 '증명 보조기와 유형론 알아보기'를 인용할게요.
저는 어떤 명제나 이론을 어떻게 형식화해야 되는지에 관심이 무진장 많습니다. 예를 들어, 저는 타일러 조지프슨 화학 공학 교수님이 물리학을 잘못 형식화하고 있다고 여러 번 비판했어요.
다만 저는 실제로 구체적인 단계까지 들어가는 형식화를 안 하고 '형식화 스케치'만 하는 사람이 되고 싶지는 않아요. 뛰어난 학자를 제외한 사람들은 얼렁뚱땅 논리를 전개하다가 빈틈을 보이기 마련이니까요. 저도 그런 사람이고요.
일단 형식화가 마무리되고 나면, 그 이후의 증명은 크게 어렵지 않은 것이 보통입니다. (차불휘님이 관심갖고 계시는 듯한, 수학 기초론의 영역에서는 이 점이 해당하지 않을 것도 같습니다.)
음, 증명 보조기로 이론을 형식화하다 보면 종이나 전자 문서에 적힌 이론 전개의 논리적 빈틈이 더 잘 보이는 거 같아요. 그 빈틈을 메꾸는 일이 늘 쉬울지는 의문스럽네요. 학술 분야마다 '논리적 허점 없애기'의 난이도가 다를 수는 있겠죠.
그렇다면 증명 보조기의 역할은 사실상 전문 철학자들보다는 철학도들에게 더 클 텐데, 철학도들이 증명 보조기를 사용하는 것은 또 과연 유용한가, 의문이 듭니다. 결국 스스로 형식 체계를 이해하고 증명을 구성하는 것이 철학을 배우는 한 과정인 것 같아서요. 형식 체계의 이해를 위해 증명 보조기를 쓸 수 있지 않을까?, 묻는다면 이는 첫째 회의론으로 이행하게 됩니다.
증명 보조기를 다루는 일이 스스로 형식 체계를 이해하고 증명을 구성하는 일과 동떨어져 있나요? 저는 그렇게 생각한 적이 없습니다. 증명 보조기를 다루기 위해서는 그 증명 보조기의 기초론을 이해해야 되는데, 이미 그 일 자체가 '스스로 형식 체계를 이해하고 증명을 구성하는 일'을 포함해요. 다시 말해, 증명 보조기의 이용법을 배우는 일은 곧 어느 한 형식 체계를 배우는 일입니다.
첫째 의문점에 대한 제 의견은 이전 댓글에 있습니다.
다른 두 댓글도 잘 읽었습니다만, 제 회의감에 대해 더 토론을 하는 것이 생산적인 일은 아닌 듯해서 아래의 두 부분에 대해서만 남깁니다.
1
어떤 표현을 정의한다는 것은 그것이 그 "표현에" 관한 것이라는 점에서 메타언어적 성격을 갖고 있다는 말씀입니다. 여하간 forall x of type p, fun(x)=x와 같이 썼을 때 (표현력의 손실은 있지만) 큰 문제는 안 생길 것 같기는 하네요.
2
이렇게 임의로 “증명”의 용례를 취하는 데에 큰 문제가 있어 보입니다. 증거를 “증명”이라고 불러버리면, 기존에 “증명”이라고 불러온 개념을 뭐라고 부를지 알 수 없게 되어 버립니다.
그리고 이렇게 보더라도, 과연 fun에 대한 정의가 p → p의 증명이 되는 것인지 분명하지 않습니다. 그 과정을 보여주실 수 있으실까요?
예를 들어, 식 λ (x : Nat) => x 자체보다는 다음 코드의 def f : Nat → Nat := λ (x : Nat) => x라는 첫째 줄이 메타언어적 성격을 띤다고 말하는 편이 훨씬 더 적절하다고 생각해요. 혹시 @car_nap 님이 이 둘을 혼동하시는 건 아닌가요?
def f : Nat → Nat := λ (x : Nat) => x
theorem f_eq_id : f = (λ x => x) := rfl
#eval f 1 -- output: 1
#eval (λ (x : Nat) => x) 1 -- 1
린에서는 --가 주석을 시작합니다.
여하간 forall x of type p, fun(x)=x와 같이 썼을 때 (표현력의 손실은 있지만) 큰 문제는 안 생길 것 같기는 하네요.
우선 fun이라는 린 핵심어는 함수 추상화를 시작하는 역할을 할 뿐, 그 자체가 특정 함수를 가리키는 이름이 아닙니다. 그래서 fun(x) = x라는 식은 이상해 보여요. 이 식에서 fun이 특정 함수를 가리키는 이름으로 쓰였다고 볼 수는 있지만, 그렇다면 fun 말고 다른 이름을 쓰는 편이 덜 헷갈리겠죠. 저는 id1이라는 이름을 쓸게요. id는 항등 함수를 뜻합니다. 린 핵심 라이브러리에는 이미 항등 함수 id가 있으므로 이와 살짝 다른 이름을 골랐어요.
theorem id1 {p : Prop} : p → p := fun (x : p) ↦ x
theorem id2 {p : Prop} (x : p) : p := x
theorem id1_eq_id {_p : Prop} : id1 x = (λ x => x) :=
rfl
theorem id1_eq_id' {p : Prop} : ∀ (x : p), id1 x = x :=
fun (_x : p) ↦ rfl
theorem id1_eq_id2 {p : Prop} : id1 = (id2 : p → p) :=
rfl
∀ (x : p), id1 x = x는 명제입니다. 하지만 함수 fun (x : p) ↦ x는 명제가 아니고, 린 코드 theorem id1 {p : Prop} : p → p := fun (x : p) ↦ x도 명제가 아니죠. 뒤엣것은 린의 유형론 내부가 아니라 외부에 있는 명제라고 말할 수는 있겠네요. 메타진술이라고 말해도 되죠? @car_nap 님의 말씀은 이해가 가지만, 린에서 명제 ∀ (x : p), id1 x = x가 직접 id1이라는 새로운 함수를 선언할 수는 없어요. 이는 웬만한 다른 증명 보조기도 마찬가지일 거예요.
@car_nap 님이 말씀하신 '큰 문제가 안 생길 것 같은' 다른 정의 방식은 위 코드의 두 번째 theorem 핵심어가 나오는 줄 theorem id2 {p : Prop} (x : p) : p := x 같네요. 두 함수 id1과 id2의 정의는 같습니다.
이런 용례는 제가 처음 만든 게 아니라는 점을 강조하고 싶습니다. 제가 쓴 글 '증명 보조기와 유
형론'에서 언급된 "호모토피 유형론: 수학의 한값 기초론"의 18쪽에 다음 문구가 있습니다.
The basic judgment of type theory, analogous to “
Ahas a proof”, is written “a : A” and pronounced as “the termahas typeA”, or more loosely “ais an element ofA” (or, in homotopy type theory, “ais a point ofA”). WhenAis a type representing a proposition, thenamay be called a witness to the provability ofA, or evidence of the truth ofA(or even a proof ofA, but we will try to avoid this confusing terminology).
그런데 "린 4로 하는 정리 증명"의 3장 '명제와 증명'에서는 오히려 저자가 '증거' 말고 '증명'이라는 용어만 씁니다.
"기존에 '증명'이라고 불러온 개념을 뭐라고 부를지 알 수 없게 되어 버립니다."라는 @car_nap 님의 말씀에서, 그 '증명'은 무엇을 가리키나요? 유형론을 거의 모르지만 그 밖의 논리학은 이미 배운 철학 또는 수학 전공자들이 이해하는 개념으로서의 '증명'인가요? "린 4로 하는 정리 증명" 교재에서와 같이 "증명"이라는 용어를 쓴다면, 이 교재에 나온 '증명'이 우리가 이미 알고 있는 개념 '증명'과 그리 다른지 저는 모르겠어요. 호모토피 유형론 교재에서는 '증거'가 어떤 명제의 증명 가능성을 보이는 개념이라고 설명했으니, 이 용어를 '증명'으로 바꿀 때 혼동이 생길 수 있죠.
"린 4로 하는 정리 증명" 3장의 위 인용문과 '커리-하워드 대응' 위키백과 항목이 이해에 도움이 될 거예요.
이 대응 때문에 린의 유형론에서는 theorem 명령이 본질적으로 def 명령의 한 버전에 불과해요.
Note that the
theoremcommand is really a version of thedefcommand: under the propositions and types correspondence, proving the theoremp → q → pis really the same as defining an element of the associated type. To the kernel type checker, there is no difference between the two. (Avigad et al. n.d.)
그래도 의문점이 남는다면 제 능력이 닿는 데까지 커리-하워드 대응을 설명해 드릴게요.
참고 문헌
1
전통적인 증명 개념은 통상 다음을 통해 이해됩니다: 문자열 s=(s1, s2, …, sn)이 p의 증명이다 iff si ∈ s와 추론 규칙 R로부터 p로의 직접적인 도출이 존재한다. 그런데 제시하신 증거 개념을 “증명”을 통해 의미하면, 어떤 a를 전제한 뒤 p를 유한 절차 내에 도출할 수만 있다면 a가 p의 증명이 됩니다. 이것이 다소간 혼동을 주는 용법 같아요. (저자들 자신도 인정하듯.)
2
아하, 이해했습니다. f(x)=y인 f가 가정될 때 x→y가 성립한다고 보는 것이군요. 이 부분에서는 요구되는 엄밀함이 충분히 충족되지 않는 것처럼 보이는데, 이에 대해서는 일단 말을 아끼겠습니다.
이게 무슨 말씀인지 이해가 안 가요. 전제를 왜 할 수 있나요? 린의 언어로 명제 p를 증명하는 일은 유형 p에 속하는 항을 하나 만드는 일이에요.
f(x)=y인 f가 가정될 때 x→y가 성립한다고 보는 것이군요.
"가정될 때"라는 말씀은 왜 하신 건가요?
1
어떤 부분이 혼란스러우신 것인지를 잘 모르겠습니다. 증명의 개념 자체가 그렇습니다. 전제 없이 도출할 수 있는 결론들을 theorem이라고 하기는 하지만, 이 역시도 사실 공리를 전제해 추론 규칙들로부터 결론으로 도출할 수 있는 명제들입니다.
2
함수 fun에 대한 정의가 가정되어 있으니까요.
아, @car_nap 님은 '전제'에 공리까지 포함하신 거군요. 네, 이해했습니다.
@car_nap 님이 "가정"이라는 표현을 쓰시는 게 의아했는데, @car_nap 님이 의도하신 바가 뭔지 점점 알 거 같네요. 제가 한번 위 문장의 의미를 추측해 보겠습니다. 린의 유형론에서 람다 함수 자체는 원시 개념이다 보니, 그게 린 코드 안에서 어떻게 쓰일 수 있는지를 미리 밝힌 규칙들이 있다는 뜻으로 저는 이해했어요. 그 규칙들은 아직 저도 잘 이해하지 못했습니다.
그렇지만 "함수 fun"이라는 표현은 앞에서 제가 설명해 드렸다시피 이상합니다. 핵심어 fun만 단독으로 볼 때, 이거는 함수가 아녜요. 예를 들어, 두 람다 함수 fun (x : Nat) ↦ x와 fun (x : Prop) ↦ x를 모두 함수 fun이라고 부르면 혼동이 생기기 마련입니다. 게다가 이 함수들은 정의역도 공역도 서로 다릅니다.
람다 함수라는 개념 자체는 린의 유형론에 원시 개념으로서 처음부터 도입됐다고 말할 수 있어요. 하지만 함수 f가 가정된다는 표현은 어색합니다. 함수 f는 람다 함수의 하나로 정의될 수 있을 뿐이지 그 개념 자체는 아니니까요.
그리고 f(x) = y라는 식에서의 변수 x, y가 각각 함수 f의 유형 x → y에서의 유형 x, y와 같다고 보신 건가요? 그러면 앞의 식에서 변수 x와 y의 유형은 각각 유형 x와 y가 돼요. 한 기호를 서로 다른 두 대상을 가리키는 데 쓰면 무지 헷갈립니다. 다만 린이 똑똑해서 이런 상황에서도 기호의 의미를 잘 가려내긴 하더군요.
아무튼 저라면 이렇게 말하겠습니다.
두 유형
x와y가 명제일 때, 정의역x에서 공역y로의 함수f를 구성하는 일은 조건문x → y를 증명하는 일과 동등하다.
정의역과 정의역 원소, 공역과 공역 원소를 구별해서 말해야 됩니다. 저나 제 멘티분들이나 말하다 보면 둘을 섞게 되더군요.
안녕하세요. 린 정리 증명기로는 맨날 눈팅만 하다가 글을 남깁니다. 예전에 차불휘님은 린 정리 증명기가 형식 철학 연구에 활용된다고 하셨습니다:
혹시 영향력 있는 형식 철학 연구에서 린 정리 증명기를 사용한 사례가 있을까요? 제가 린 정리 증명기도 모르고 형식 철학도 잘 몰라서 댓글 남깁니다.
이저벨(Isabelle)이나 코크(Coq)가 형식 철학 연구에 쓰인 사례가 현재로서는 더 많아 보여요. 그래도 콰인의 새 기초론[New Foundations]이 무모순적이라는 랜들 홈스(Randall Holmes) 수학 교수님의 증명 중에서 사람이 검토하기 까다로운 부분을 린으로 형식화해서 검증한 사례가 있습니다.
수리 논리학보다는 다른 철학 분야에 관심이 많은 철학 전공자는 린보다는 이저벨을 먼저 살펴보는 편이 낫겠다는 생각이 저도 듭니다. 그런데 아직 제가 다룰 줄 아는 증명 보조기가 린뿐이어서 이걸 홍보했어요. 올해 말이나 이듬해 초에 제가 이저벨을 배울 시간이 나면 좋겠네요.
어... 올려주신 린 관련 링크들에는 커뮤니티 댓글 밖에 없습니다. 혹시 린 정리 증명기를 형식 철학에 사용한 연구가 저널에 등재된 적은 없을까요?
없을걸요. 저 연구 결과는 아직 학술지에 게재되지 않았어요. 린은 현재 주로 수학자들이 쓰는 증명 보조기다 보니, 린을 이용한 철학 논문을 학술지에서 찾기는 어렵죠.
제가 예전에 쓴 글 '형식 철학과 증명 보조기'에서 계산 형이상학 프로젝트를 언급했습니다. 이저벨/HOL을 이용한 이 프로젝트의 누리집에서, 학술지에 게재된 논문들을 찾으실 수 있어요. 다음은 그중 하나입니다.
근데 무슨 증명 보조기를 쓰느냐는 문제는 무슨 프로그래밍 언어를 쓰느냐는 문제와 비슷해요. 자신의 프로젝트에 알맞고, 자신이 선호하는 상호 작용 정리 증명기를 쓰면 됩니다. 린이 형식 철학 연구에 부적합하다고 보기는 어려워요. 그저 린 이용자 중에 철학자가 너무 적은 게 문제일 뿐이죠.