■

後期授業第二回目の今回は、「論理結合子の条件」について、証明論的意味論の立場から考えてみたいと思います。
具体的には、意味の理論IIの素朴な解釈である素朴な推論主義「論理結合子の意味は導入規則と除去規則によって完全に定められる」が正しいかどうかを検討します。言い換えると「導入規則さえ与えれば、どんな結合子も『論理結合子』として認められるのか？」という疑問についてです。
この疑問に関し、プライアーによる tonk の例をあげ、素朴な推論主義が成立しないことを示し、ベルナップによる「保存拡大性」概念を導入します。
なお、保存拡大性の説明の箇所で使用する証明図の書き換えの技法は、今後、証明の正規化などの箇所で重要になります。

授業内容

1. 前回の復習
   1. モデル論的意味論
   2. 証明論的意味論
2. 論理結合子の条件
3. 保存拡大性

本日の授業資料

授業要約・宿題

こちらから

授業スライド

こちらから

参考文献

授業で紹介したPrior の tonk の初出はこちら。
Prior, Arthur. "The runabout inference ticket." Analysis, 21, pp38-39, 1960-61.(link: http://www.jstor.org/pss/3326699)

またベルナップの tonk の初出文献は以下の通りです。
Tonk, Plonk and Plink. Nuel D. Belnap. Analysis, Vol. 22, No. 6. (Jun., 1962), pp. 130-134. (link: http://www.jstor.org/pss/3326862)