■
授業第十五回目の今回は、論理結合子の意味について、証明論的意味論の立場からさらに考察を加えたいと思います。具体的には、
- 結合子の導入規則がその意味を定めるというゲンツェンの意見を紹介
- 「導入規則さえ与えれば、どんな結合子も『論理結合子』として認められるのか?」という疑問
- プライアーによる反例 tonk の紹介
- 論理結合子が満たしているべき条件としてベルナップによる「保存拡大性」概念を導入
- 結論:ある結合子が論理結合子として認められるべきかどうかは、言語に含まれる他の結合子との関係で定まる
なお、保存拡大性の説明の箇所で使用する証明図の書き換えの技法を可能にする性質は、inversion principleと呼ばれ、今後、証明の正規化などの箇所で重要になります。