皆様,
東北大学の竹田です.
以下の通りセミナーを開催いたしますのでご案内いたします.
https://sites.google.com/view/sendai-logic/
日時:7月26日(金)15:00〜
場所:東北大学理学研究科合同A棟801号室 (zoom配信あり)
講演者:織田幸弘 (東北大学情報)
題目 帰納的定義付き一階述語論理の循環証明体系におけるカット除去の反例
概要 循環証明体系とは証明図にサイクル(循環)の存在を許容した証明体系である.このような体系は無限降下法の形式化とみなせる場合がある.
そのため,循環証明体系は帰納法を使う証明体系の代替手段として証明探索の観点から注目されている.
その一方で,循環証明体系の証明論的な性質についてはまだわかっていないことが多い.
本講演では帰納的定義付き一階述語論理に対する循環証明体系のカット除去の反例を与える.反例の存在から帰納的定義付き一階述語論理に対する循環証明体系においてはカット除去性という基本的な性質が成り立たないことがわかる.