命題論理の簡易インスティチューション
ついで(?)だから、命題論理も書いてしまえ。
Bを有限集合と単射の圏だとする、これが指標圏。X∈|B|のとき、Xは命題変数の集合だとみなす。Ω={true, false}を2値のブール代数として、多項式インスティチューションと同じようにして簡易インスティチューションを作る。
M(X) = ΩXとする。M(X)は命題変数への真偽値割り当ての全体になる。a∈M(X)は、ブール値のレコード{x1:v1, ..., vn:vn}の形で書いてもよい(多項式のときと同じ)。それで、S(X)は、Xに含まれる命題変数を含む命題論理式の全体とする。
a∈M(X)、p∈S(X)に対して、a |= p とは、論理式pにaによる真偽値割り当てを実行(代入)して、ブール値として評価した結果を【p[a]】だとして、【p[a]】= true のことだと定義する。
充足条件は、σ:X→Yが単射(指標射ですね)だとして
- b∈M(Y), p∈S(X)に対して、M(σ)(b) |= p ⇔ b |= S(σ)(p)
となる。これは、命題論理式pと割り当てaに関して次を示せばよい。
- 【p[bσ]】 = 【pσ[b]】
ここで、bσ = b・σ(写像の合成)であり、pσは、σによって命題変数を置き換えたpのことである。これをまじめに示すには、論理式の構成に沿った帰納法を使うことになり意外と面倒だが、難しくはないだろう。
命題論理のインスティチューションは、構造的に、多項式のインスティチューションとほとんど同じである。