- Title: Kalish/Montague and Ja´skowski Natural Deduction
- Authors: Mohammad M. Ajallooeian, Francis Jeffry Pelletier
- Pages: 9p
- URL: https://mirror.las.iastate.edu/tex-archive/macros/latex/contrib/natded/extended_doc.pdf
$`\newcommand{\mrm}[1]{\mathrm{#1}}
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\letsShow}{\Keyword{lets show } }
\newcommand{\conclude}{\Keyword{conclude } }
\newcommand{\par}{\Keyword{par } }
\newcommand{\endBlock}{\Keyword{end } }
\newcommand{\case}{\Keyword{case } }
\newcommand{\assume}{\Keyword{assume } }
\newcommand{\consider}{\Keyword{consider } }
\newcommand{\suchThat}{\Keyword{such that } }
\newcommand{\curs}{ \textcolor{orange}{\blacksquare} }
\newcommand{\Imp}{ \Rightarrow }`$
ヤシコフスキ〈Stanisław Jaśkowski〉／カリシュ〈Donald Kalish〉／モンタギュー〈Richard Montague〉〈JKM〉形式の証明：
$`\letsShow ( (p \Imp q) \land (\lnot r \Imp \lnot q) )\Imp (p \Imp r)\\
\bullet (p \Imp q) \land (\lnot r \Imp \lnot q) \text{ を仮定して、 } (p \Imp r) \text{ を導く}\\
\quad \assume (p \Imp q) \land (\lnot r \Imp \lnot q) \:\cdots \text{(1)}\\
\qquad \letsShow p \Imp r\\
\qquad \bullet p \text{ を仮定して }r \text{ を導く}\\
\qquad\quad \assume p \:\cdots \text{(2)}\\
\qquad\qquad \downarrow \text{上の仮定を再掲}\\
\qquad\qquad (p \Imp q) \land (\lnot r \Imp \lnot q) \:\cdots \text{(3)}\\
\qquad\qquad \downarrow \text{すぐ上の連言の左側}\\
\qquad\qquad (p \Imp q) \:\cdots \text{(4)}\\
\qquad\qquad \downarrow \text{モーダスポネンスを適用}\\
\qquad\qquad q \:\cdots \text{(5)}\\
\qquad\qquad \downarrow \text{上の連言の右側}\\
\qquad\qquad \lnot r \Imp \lnot q \:\cdots \text{(6)}\\
\qquad\qquad \letsShow r\\
\qquad\qquad \bullet \text{背理法を使う}\\
\qquad\qquad\quad \assume \lnot r \:\cdots \text{(7)}\\
\qquad\qquad\qquad \downarrow\text{先の命題を再掲}\\
\qquad\qquad\qquad \lnot r \Imp \lnot q \:\cdots \text{(8)}\\
\qquad\qquad\qquad \downarrow \text{モーダスポネンスを適用}\\
\qquad\qquad\qquad \lnot q \:\cdots \text{(9)}\\
\qquad\qquad\qquad \downarrow\text{先に得られた命題を再掲}\\
\qquad\qquad\qquad q \:\cdots \text{(10)}\\
\qquad\qquad\qquad \downarrow\text{矛盾が生じる}\\
\qquad\qquad\qquad \bot\\
\qquad\qquad\quad \endBlock\\
\qquad\qquad \conclude r\\
\qquad\quad \endBlock\\
\qquad \conclude p \Imp r\\
\quad \endBlock\\
\conclude ( (p \Imp q) \land (\lnot r \Imp \lnot q) )\Imp (p \Imp r)
`$
インデントガイドラインがあったほうがよい。
※ カリシュ／モンタギューの教科書は "Logic: Techniques of Formal Reasoning"
