否定の導入
en: negation introduction
aka. refutation by contradiction
A → ⊥ ⊢ ¬A
矛盾ないし恒偽命題がある体系では、単なる定義
def. A → ⊥ ⊣⊢ ¬A
A → ⊥ ≡ ¬A
戸次『数理論理学』
SK (def. 7.20, p. 157)
HM (def. 7.31, p. 160)
LK, LJ (def. 10.1, p. 215)
最小論理より弱い体系では略記ないし派生形式とは定義できないとか。 SKを除く
論理式 A から恒偽式が導かれる場合には ￢A は必ず真になります。これは否定導入と呼ばれる推論規則です。否定導入は背理法と呼ばれる証明方法の根拠になります。
論理式 A と恒偽式 ⊥ について、A→⊥ が真であるような任意の解釈のもとで ¬A は必ず真になります。これは否定導入と呼ばれる推論規則です。
proof.
LJ で証明する。
code:bussprofs
\begin{prooftree}
\AxiomC{}
\RightLabel{(ID)}
\UnaryInfC{$A \vdash A$}
\AxiomC{}
\RightLabel{$({\bot\vdash})$}
\UnaryInfC{$\bot \vdash$}
\RightLabel{$({\rightarrow\vdash})$}
\BinaryInf$A \rightarrow \bot, A \vdash$
\RightLabel{$({\vdash\neg})$}
\UnaryInfC{$A \rightarrow \bot \vdash \neg A$}
\end{prooftree}
fig. https://pbs.twimg.com/media/GGTqk1gbcAAED9D.png
P → Q ⊢ ¬Q → ¬P
⊢ ((P → Q) ∧ (P → ¬Q)) → ¬P
これが有名なヤツのはず
LJ で証明可能
ID×3, ¬⊢, →⊢×2, C⊢, ⊢¬, ∧⊢, ⊢→
vs 否定の除去
¬A → ⊥ ⊢ A
これのこと
¬¬A ⊢ A
ref.
Rules of inference
Negation