直観主義論理
排中律 p ∨ ¬ p {\displaystyle p\vee \neg p} だけでなくパースの法則 ( ( p → q ) → p ) → p {\displaystyle ((p\to q)\to p)\to p} や二重否定除去 ¬ ¬ p → p {\displaystyle \neg \neg p\to p} などがその例である。古典論理において二重否定導入 p → ¬ ¬ p {\displaystyle p\to \neg \neg p} と二重否定除去 はともに定理である。直観主義論理においては前者のみが定理である。すなわち二重否定を導入することはできるが、除去することはできない。ただし三重否定除去 ¬ ¬ ¬ p → ¬ p {\displaystyle \neg \neg \neg p\to \neg p} は定理である。排中律 p ∨ ¬ p {\displaystyle p\vee \neg p} の拒絶は古典論理に親しい者には奇妙に思われるが、直観主義論理で命題論理式を証明するには、全ての可能な命題論理式に対して真または偽の証明が要求され、これは様々な理由によって不可能である。
多くの古典論理で妥当な恒真式は直観主義論理では定理でないが、全ての直観主義論理で妥当な定理は古典論理に於いても妥当であるから、直観主義論理は古典論理を弱めたものであるという見方ができる。ただし直観主義論理は古典論理にはない良い性質を多く持っている。
否定
もし否定を表す結合子 ¬ {\displaystyle \lnot } を φ → ⊥ {\displaystyle \phi \to \bot } なる省略形の代わりに導入したいならば、次を公理に加えれば十分である:
NOT-1': ( φ → ⊥ ) → ¬ φ {\displaystyle (\phi \to \bot )\to \lnot \phi }
NOT-2': ¬ φ → ( φ → ⊥ ) {\displaystyle \lnot \phi \to (\phi \to \bot )}
否定を導入した代わりに偽を表す命題定数 ⊥ {\displaystyle \bot } を落としたいならば次のようにする。まず FALSE, NOT-1', NOT-2' を次の公理に置き換える:
NOT-1: ( φ → χ ) → ( ( φ → ¬ χ ) → ¬ φ ) {\displaystyle (\phi \to \chi )\to ((\phi \to \lnot \chi )\to \lnot \phi )}
NOT-2: φ → ( ¬ φ → χ ) {\displaystyle \phi \to (\lnot \phi \to \chi )}
NOT-1の代替としては ( φ → ¬ χ ) → ( χ → ¬ φ ) {\displaystyle (\phi \to \lnot \chi )\to (\chi \to \lnot \phi )} または ( φ → ¬ φ ) → ¬ φ {\displaystyle (\phi \to \lnot \phi )\to \lnot \phi } などがある。