Lindenbaum-Tarski代数
メモ
Lindenbaum代数と言う時もある
例
論理関数として$ \to,\botを採用し,残り$ \lor,\land,\lnot,\top,\leftrightarrowは適当に略記として導入する.
もちろん証明能力が等価であることがわかっている別の証明体系で証明可能な論理式の集合でも構わない. 「論理式$ \varphiは古典論理で証明可能である」を$ \vdash_\mathsf{PL} \varphiと表す.
もちろんこれは$ \varphi \in \mathrm{PL}である.
論理式の集合$ \mathrm{Form}を次の同値関係$ \sim_\mathsf{PL}で割ったものを$ \mathrm{Form} / \sim_\mathsf{PL}と書く. $ \varphi \sim_\mathsf{PL} \psi \iff \vdash_\mathsf{PL} \varphi \leftrightarrow \psi
古典命題論理のLindenbaum-Tarski代数$ \mathfrak{A}_\mathsf{PL} \coloneqq \lang \mathrm{Form} / \sim_\mathsf{PL}, +, \times, \cdot^-, 0, 1\rangを以下のように定める. $ \varphiの$ \sim_\mathsf{PL}の同値類を$ \llbracket \varphi \rrbracketと表す. $ \llbracket \varphi \rrbracket + \llbracket \psi \rrbracket = \llbracket \varphi \lor \psi \rrbracket
$ \llbracket \varphi \rrbracket \times \llbracket \psi \rrbracket = \llbracket \varphi \land \psi \rrbracket
$ \llbracket \varphi \rrbracket^- = \llbracket \lnot \varphi \rrbracket
$ 0 = \llbracket \bot \rrbracket
$ 1 = \llbracket \top \rrbracket
Thm:
$ \mathfrak{A}_\mathsf{PL}はBoole代数である.