Lindenbaum-Tarski代数

メモ

各々の論理の代数的意味論を考えるとき，その論理の代数のことを特別にLindenbaum-Tarski代数という．

Lindenbaum代数と言う時もある

例

論理関数として$ \to,\botを採用し，残り$ \lor,\land,\lnot,\top,\leftrightarrowは適当に略記として導入する．

$ \mathrm{PL}はŁukasiewiczの3公理図式によるHilbert流演繹体系で閉じた論理式の集合とする．

もちろん証明能力が等価であることがわかっている別の証明体系で証明可能な論理式の集合でも構わない．

「論理式$ \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代数である．