Wiki. “否定” [否定]

在 Heyting 代数中, 定义否定算子为 $$ \neg x = (x\Rightarrow 0). $$ 即 $x$ 的否定等同于说 $x$ 蕴含矛盾. 由 $\Rightarrow$ 的定义, $$ y\leq \neg x\quad \text{iff}\quad y\wedge x = 0. $$ 在完备格中, $\neg x$ 是所有与 $x$ 之相遇 (meet) 为 $0$ 的元素 $y$ 之并.

性质

在任意 Heyting 代数中,

• $x\leq \neg\neg x$;
• 若 $x\leq y$, 则 $\neg y\leq \neg x$; (这说明 $\neg$ 是这个 Heyting 代数到其反范畴的函子.)
• $\neg x = \neg\neg\neg x$;
• $\neg\neg(x\wedge y) = \neg\neg x \wedge \neg\neg y$.

命题. 若 $x$ 有补元素 (即满足 $x\vee a = 1$, $x\wedge a = 0$ 的元素 $a$), 则补元素必为 $\neg x$.