このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

命題論理の簡易インスティチューション

ついで(?)だから、命題論理も書いてしまえ。

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のことである。これをまじめに示すには、論理式の構成に沿った帰納法を使うことになり意外と面倒だが、難しくはないだろう。

命題論理のインスティチューションは、構造的に、多項式のインスティチューションとほとんど同じである。

  • 不定元 ←→ 命題変数
  • 体K ←→ ブール代数Ω
  • 演算記号 ←→ 論理記号
  • 多項式 ←→ 命題論理式
  • 座標点(レコード) ←→ 真偽値割り当て
  • Kの計算 ←→ Ωの計算
  • 0 ←→ true