■

授業第二十五回目、本日は推件計算と部分構造論理の話をします。
まず、前回紹介した「仮定を使用した演繹」の一種として、直観主義論理の推件計算(sequent calculus)を導入します。論理結合子の右導入則が自然演繹における導入則、左導入則が除去規則に対応します。次に構造規則（縮約規則・交換規則・割増規則）について説明します。最後に、構造規則に制限を加えた部分構造論理について紹介します。
また、部分構造論理の土台となる、ランベック計算（FL）について補足します。FLは、本来言語学における「範疇文法」を形式化するために導入されたもので、論理結合子の左右の導入規則のみを持ち、一切構造規則を持たないのが特徴です（範疇文法との関係については来週説明します）。