論理学のノーテーション
メモ
今後のためにノーテーションを定める．
論理
論理を指すときは\mathsf{}で囲むことにする．
論理$ \mathsf{\Lambda}とは例えば次のように定める定理の集合と考えることにする．
言語$ \mathscr{L}上の論理式の集まり$ \mathrm{Form}_\mathscr{L}において，
モデル的な方法，証明体系的な方法，あるいは何らかの定義によって集合$ \mathrm{Thm}_\mathscr{L} \sube \mathrm{Form}_\mathscr{L}を定めるとする．
$ \mathrm{Thm}_\mathscr{L}を論理$ \mathsf{\Lambda}の定理とし，$ \mathsf{\Lambda}を特徴づける要素とする．
$ \mathsf{\Lambda}が古典論理であるとき，$ \mathsf{\Lambda}の直観主義論理バージョンであることを明示的に表したいとき，小文字の$ \sf iを先頭に付けることにする． memo:大文字ではないのは例えば解釈可能性論理IL$ \sf ILのように$ \sf Iで始まる論理もあり紛らわしいため． 証明体系一般
論理$ \mathsf{\Lambda}に対してHilbert流演繹体系を$ \mathfrak{H}_\mathsf{\Lambda}と表記する． 紛らわしいので，公理は\mathbf{*}として表す．
一般に推論規則は\mathrm{(*)}で囲むものとする． 例
$ \mathfrak{H}_\mathsf{Prop} = \mathbf{Ł_1} + \mathbf{Ł_2} + \mathbf{Ł_3} + \mathrm{(MP)}である．
$ \mathfrak{H}_\mathsf{K} = \mathfrak{H}_\mathsf{Prop} + \mathbf{K} + \mathrm{(Nec)}である．
$ \mathfrak{H}_\mathsf{GL} = \mathfrak{H}_\mathsf{K} + \mathbf{L}と表す．
$ \mathfrak{H}_\mathsf{GL} = \mathfrak{H}_\mathsf{K4} + \mathrm{(L)}とも表される．
正規様相論理K4$ \mathfrak{H}_\mathsf{K4} = \mathfrak{H}_\mathsf{K} + \mathbf{4}で，$ \mathrm{(L)}はLöb推論規則 $ \mathfrak{H}_\mathsf{N} = \mathfrak{H}_\mathsf{Prop} + \mathrm{(Nec)}
よって
$ \mathfrak{H}_\mathsf{N} = \mathbf{Ł_1} + \mathbf{Ł_2} + \mathbf{Ł_3} + \mathrm{(MP)} + \mathrm{(Nec)}でもある．
$ \mathfrak{H}_\mathsf{K} = \mathbf{Ł_1} + \mathbf{Ł_2} + \mathbf{Ł_3} + \mathbf{K} + \mathrm{(MP)} + \mathrm{(Nec)}であることに注意．すなわち$ \bf Kがない．
$ \frak{S}_\Lambdaにカット規則を追加した体系/カット有りシークエント計算体系を$ \mathfrak{S}^\mathrm{C}_\Lambdaとか$ \mathfrak{S}_\Lambda + \mathrm{(cut)}と表記する． このように表される．
$ \mathfrak{S}^\mathrm{C}_\Lambda \vdash \Gamma \rArr \Delta \implies \mathfrak{S}_\mathrm\Lambda \vdash \Gamma \rArr \Delta