9月2日～6日の5日間、Hokkaido Summer Institute 2024文学部・文学院開講科目のひとつであるPhilosophy (Lecture): Topics in Mathematical Logic 2024 (1)/(2) 哲学特殊講義：数理論理学の諸相 2024 (1)/(2)が開講されました。哲学倫理学研究室の佐野勝彦教授と、ドイツのフリードリヒ・アレクサンダー大学エアランゲン・ニュルンベルクからお迎えしたTadeusz LITAK（タデウシュ リタク）上級講師が協働し、対面で授業を行いました。
本科目では、論理学の初歩的な知識と一定の熟練度を前提として、定理証明支援系の使用に精通したLitak上級講師と、本学佐野教授の指導のもと、一階および高階の古典論理、直観主義論理における定理証明のために、定理証明支援系 Coq をいかに使用するかを学びます。
論理学や数学では、人がペンで紙の上に書いた証明にギャップがあって間違っていた、とか、場合分けが多すぎて証明が正しいかどうかの検証が大変だ、ということがあります。定理証明支援系とは数学の定理証明を支援するソフトウェアのことで、数多くの場合分けを含む数学の証明に間違いがないことを保証したり、ソフトウェアの安全性を保障したりするためにも使用されています。授業で主に扱った定理証明支援系 Coq は、「いかなる地図も隣接する領域が異なるように色を塗るには四つの色があれば十分である」という四色定理の証明（複雑な場合分けがありました）が正しいことを検証するためにも使用されました。
初回の講義は講師と受講生の自己紹介から始まり、各々のテーマや興味・関心について共有しました。主な受講生は、論理学を学ぶ博士後期課程または修士課程の大学院生です。
講義は、Coqと定理証明支援系の紹介、Curry-Howard対応、論理学と型理論の比較などから始まり、Litak上級講師の講義と演習を織り交ぜながら進みます。佐野教授も、学生と机を並べて演習に取り組みつつ、Litak上級講師とともに学生の記述内容（コード）を確認してまわりました。
Litak上級講師は長期の日本滞在経験があり、時折日本語が飛び出すユーモアあふれる講義を展開しました。受講生らは、少人数でじっくりと指導を受けられる恵まれた環境で、カリー・ハワード対応、依存型理論、証明をプログラミングとして捉えること、定理証明支援系の適切な使用を段階的に学んだ5日間となりました。
Litak上級講師によると、今回の内容を一足飛びにマスターすることは至難の業で、学んだことを時間をかけて少しずつ自分のものにしていくことが重要だそうです。
