증명언어 agda로 (직관적, 명제 논리 버전의) 자연연역을 형식화 하고, 정규화(normalization), 일관성(consistency), 배중률의 증명 불가능성 등을 증명해봤습니다.
핵심이 되는 정규화 증명은 Frank Pfenning 교수님의 Constructive Logic 강의노트와 Hereditary Substitutions for Simple Types, Formalized를 참고했습니다. 단, FP 교수님의 강의노트에서는 겐첸의 방법과 같이 sequent calculus의 cut-elimination을 통해서 증명을 했지만 저는 sequent calculus를 정의하지 않았기 때문에 완전히 같은 방식은 아닙니다. 증명의 핵심은 hereditary substitution의 정의로, cut-free sequent calculus에서 cut의 admissibility를 보이는 것에 대응됩니다.
아그다(Agda) 증명 보조기로 구성주의 자연 연역을 형식화하신 것을 축하합니다.
아그다도 줄립(Zulip) 서버를 운영하더군요. #newcomers 스트림에서 자기소개를 간단히 하고 @damhiya 님의 아그다 코드를 공유하셔도 좋을 듯합니다.
증명언어 커뮤니티도 은근 많아서 사실 이미 여러곳에 가입되어 있어요. 개인적으로는 한국어권에서 이런 관심이 커졌으면 해서 그런 커뮤니티들에는 몇번 공유했구요.
영어권 커뮤니티에는 이 코드를 공유한적이 없긴 한데, 특별한 이유가 있는건 아니고 워낙 많이 알려졌고 형식화도 많이 된 증명이라 안올려봤네요.
저는 증명 보조기를 소개할 만한 한국어 커뮤니티는 서강올빼미랑 긱뉴스(GeekNews)밖에 생각이 안 나네요. 증명 보조기를 이용하는 한국인을 온라인으로 찾기 쉽지 않은데, 이를 해내더라도 각자가 주로 이용하는 증명 보조기도 다르고 세부 관심 분야도 다르더군요.
제가 혼자서 증명 보조기 입문용 콘텐츠를 기획하고 있는데, 본격적인 활동을 언제 시작할지는 아직 확정이 안 됐어요.