Hilbert algebra の性質の証明

ちょっと気になってやってみたのをどこかにメモしたくなったので書いた。関数解析じゃなくて論理の方の Hilbert algebra です。

Hilbert algebra の公理

 (A, \rightarrow, 1) が Hilbert algebra とは

  •  \rightarrow: A^2 \rightarrow A
  •  1 \in A
  •  a \rightarrow b \rightarrow a = 1
  •  (a \rightarrow b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow (a \rightarrow c) = 1
  • if  (a \rightarrow b) =  (b \rightarrow a) = 1 then  a = b

性質

  •  1 \rightarrow a = a
  •  a \rightarrow 1 = 1
  •  a \rightarrow a = 1
  •  a \rightarrow b \rightarrow c = b \rightarrow a \rightarrow c
  •  a \le b \iff a \rightarrow b = 1 で順序が入り,1 が最大元

などが成り立つ。証明は下に書くけど自分で考えると楽しいかも。

証明

補題:  a \rightarrow b = 1 かつ  a = 1 なら  b = 1

証明: 最後の公理があるので  b \rightarrow 1 = 1 \rightarrow b = 1 がいえればよいが,
 \begin{array}{rll} b \rightarrow 1 & = & b \rightarrow (a \rightarrow b) & (仮定\ a \rightarrow b = 1)
\\ & = & 1 & (\text{公理}) \end{array}
 \begin{array}{rll} 1 \rightarrow b & = & a \rightarrow b & (仮定\ a = 1) \\ & = & 1 & (仮定)\end{array}

定理: 直観主義論理の implicational fragment で  \vdash \varphi なら, A \models \varphi = 1

証明: Hilbert style system での証明に関する帰納法。Modus ponens のときは上の補題を使う。

系: 直観主義論理の implicational fragment で  \vdash \varphi \rightarrow \psi かつ  \vdash \psi \rightarrow \varphi なら, A \models \varphi = \psi

上に書いた主張はこの定理と系から全部出てくる。