本記事では,ペアノ算術の加法交換法則の証明図をかいていきたいと思います.
ペアノ算術の各種法則の証明は,等式変形をやっていけばそれほど難しいものではないですが,
せっかく基礎まで立ち返って証明をやっているのにそれではもったいないので,1段階ずつ推論規則を追って加法交換法則を証明し,証明図にしていこうと思います.
なお,本記事は参考文献にあげた資料および筆者が数年前に受けた記号論理学の講義の記憶をもとに構成されています.
独自の定義を含む可能性がありますので,レポートなどのためにこの記事を見つけられた方はご注意ください.
証明の前にまず必要事項の定義をまとめていきます.
まずは記号の定義です.
ここを厳密に構成するのは筆者の手に余るので自然言語的な説明でお許しください.
古典一階述語論理の推論規則です.
本項は文献[1-4]を元に,(ちょいちょい表記がブレるので)筆者が構成したものです.
~
「
のようにどこの推論に対応する仮定なのかわかるようマークをつけたりします.
排中律(
「数」を扱うのに必要な等号「
ここで,公理として「
変数
「自然数」における演算を以下の公理系で定義します.(参考:[4,6])
記号
公理系(PA)
ここまでに定義した推論規則・公理を使って
を証明します.
全称量化が2つあるので,2重の数学的帰納法で証明していきます.
適宜用いた推論規則や公理を()で付記します.
(I)
(I-i)
(I-ii)
(II)
この証明を証明図にするとこのようになります.
証明図-全体
いくらなんでも見づらすぎるので前半部分を分割すると,以下のようになります.
証明図-分割
bussproofs パッケージを用いてLaTeXで描画しています.
すぐ紙幅をはみ出すので調整が大変です.
以上です.
今後,機会があれば他の法則の証明もやってみようと思います.
間違いなどありましたらコメントで教えていただけると幸いです.
面倒がってマクロを濫用した汚いコードですが,参考に置いておきます.
※マークダウン記法と干渉しておかしな表示になってるのでソースコードを参照してください.
\documentclass[a4paper,8pt]{jsarticle}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{bussproofs}
%\usepackage{proof}
\newcommand{\CAA}{(反射律)}
\newcommand{\CAB}{(対称律)}
\newcommand{\CAC}{(推移律)}
\newcommand{\CAD}{ (代入律(関数))}
\newcommand{\CAE}{(代入律(述語))}
\newcommand{\PAA}{$(\mathrm{PA1})\; \forall n. \lnot(sn=0)$}
\newcommand{\PAB}{$(\mathrm{PA2})\;\forall m. \forall n. (sm=sn\to m=n)$}
\newcommand{\PAC}{$(\mathrm{PA3})\; \forall n. (n+0=n)$}
\newcommand{\PAD}{$(\mathrm{PA}4)\; \forall m. \forall n. (m+sn=s(m+n))$}
\newcommand{\MI}{(数学的帰納法)}
\let\A\AxiomC
%\let\R\RightLabel
\newcommand{\R}[1]{\RightLabel{{\footnotesize #1}}}
\let\U\UnaryInfC
\let\B\BinaryInfC
\let\T\TrinaryInfC
\newcommand{\paren}[1]{\left( #1 \right)}
\newcommand{\bracket}[1]{\left[ #1 \right]}
\newcommand{\To}{\vdash}
\begin{document}
\rotatebox{270}{
\scalebox{0.3}{
\parbox{2.7\linewidth}{
\begin{prooftree}
%
\A{}
\R{\CAA}
\U{$0+0=0+0$}%(1)
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. 0+sn=s(0+n)$}
\R{$\forall E$}
\U{$0+sk = s(0+k)$}%(2)
%
\A{$\bracket{0+k=k+0}^A$}
\R{\CAD}
\U{$s(0+k)=s(k+0)$}%(3)
\R{\CAC}
\B{$0+sk=s(k+0)$}%(5)
%
\A{\PAC}
\R{$\forall E$}
\U{$k+0=k$}
\R{\CAD}
\U{$s(k+0)=sk$}%(4)
\R{\CAC}
\B{$0+sk=sk$}%(6)
%
\A{\PAC}
\R{$\forall E$}
\U{$sk+0=sk$}
\R{\CAB}
\U{$sk=sk+0$}%(7)
\R{\CAC}
\B{$0+sk=sk+0$}%(8)
\R{$\to I^A$}
\U{$(0+k=k+0\to 0+sk=sk+0)$}
\R{$\forall I$}
\U{$\forall k.(0+k=k+0\to 0+sk=sk+0)$}%(9)
\R{\MI}
\B{$\forall y. (0+y=y+0)$}
%
\A{}
\R{\CAA}
\U{$0+0=0+0$}%(1)
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. 0+sn=s(0+n)$}
\R{$\forall E$}
\U{$0+sk = s(0+k)$}%(2)
%
\A{$\bracket{0+k=k+0}^A$}
\R{\CAD}
\U{$s(0+k)=s(k+0)$}%(3)
\R{\CAC}
\B{$0+sk=s(k+0)$}%(5)
%
\A{\PAC}
\R{$\forall E$}
\U{$k+0=k$}
\R{\CAD}
\U{$s(k+0)=sk$}%(4)
\R{\CAC}
\B{$0+sk=sk$}%(6)
%
\A{\PAC}
\R{$\forall E$}
\U{$sk+0=sk$}
\R{\CAB}
\U{$sk=sk+0$}%(7)
\R{\CAC}
\B{$0+sk=sk+0$}%(8)
\R{$\to I^A$}
\U{$(0+k=k+0\to 0+sk=sk+0)$}
\R{$\forall I$}
\U{$\forall k.(0+k=k+0\to 0+sk=sk+0)$}%(9)
\R{\MI}
\B{$\forall y. (0+y=y+0)$}
\R{$\forall E$}
\U{$0+sl=sl+0$}
\R{\CAB}
\U{$sl+0=0+sl$}%(25
%
\A{\PAD}
\R{$\forall E$}
\U{$sl+sn=s(sl+n)$}
\R{$\forall E$}
\U{$sl*sk=s(sl+k)$}%(11)
%
\A{$\bracket{sl+k=k+sl}^B$}
\R{\CAD}
\U{$s(sl+k)=s(k+sl)$}%(12)
\R{\CAC}
\B{$sl+sk=s(k+sl)$}%(13)
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. k+sn=s(k+n)$}
\R{$\forall E$}
\U{$k+sl=s(k+l)$}
\R{\CAD}
\U{$s(k+sl)=ss(k+l)$}%(14)
\R{\CAC}
\B{$sl+sk=ss(k+l)$}%(15
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. sk+sn=s(sk+n)s$}
\R{$\forall E$}
\U{$sk+sl=s(sk+l)$}%(16
%
\A{$\bracket{\forall y. l+y=y+l}^C$}
\R{$\forall E$}
\U{$l+sk=sk+l$}
\R{\CAB}
\U{$sk+l=l+sk$}
\R{\CAD}
\U{$s(sk+l)=s(l+sk)$}%(17
\R{\CAC}
\B{$sk+sl=s(l+sk)$}%(18
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. l+sn=s(l+n)$}
\R{$\forall E$}
\U{$l+sk=s(l+k)$}
\R{\CAD}
\U{$s(l+sk)=ss(l+k)$}%(19
\R{\CAC}
\B{$sk+sl=ss(l+k)$}%(20
%
\A{$\bracket{\forall y. l+y=y+l}^C$}
\R{$\forall E$}
\U{$l+k=k+l$}
\R{\CAD}
\U{$ss(l+k)=ss(k+l)$}%(21
\R{\CAC}
\B{$sk+sl=ss(k+l)$}
\R{\CAB}
\U{$ss(k+l)=sk+sl$}%(22
\R{\CAC}
\B{$sl+sk=sk+sl$}%(23
\R{$\to I^B$}
\U{$(sl+k=k+sl)\to(sl+sk=sk+sl)$}
\R{$\forall I$}
\U{$\forall k. (sl+k=k+sl)\to(sl+sk=sk+sl)$}%(24
\R{\MI}
\B{$\forall y. sl+y = y+sl$}%(25
\R{$\to I$}
\U{$(\forall y.l+y=y+l)\to(\forall y. sl+y=y+sl)$}
\R{$\forall I$}
\U{$\forall l. (\forall y.l+y=y+l)\to(\forall y. sl+y=y+sl)$}%(27
\R{\MI}
\B{$\forall x. \forall y.x+y=y+x$}
\end{prooftree}}}}
\newpage
\scalebox{0.4}{少し見やすいver.}
\fbox{
\scalebox{0.4}{
\parbox{1.4\linewidth}{
\begin{prooftree}
\A{}
\R{\CAA}
\U{$0+0=0+0$}%(1)
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. 0+sn=s(0+n)$}
\R{$\forall E$}
\U{$0+sk = s(0+k)$}%(2)
%
\A{$\bracket{0+k=k+0}^A$}
\R{\CAD}
\U{$s(0+k)=s(k+0)$}%(3)
\R{\CAC}
\B{$0+sk=s(k+0)$}%(5)
%
\A{\PAC}
\R{$\forall E$}
\U{$k+0=k$}
\R{\CAD}
\U{$s(k+0)=sk$}%(4)
\R{\CAC}
\B{$0+sk=sk$}%(6)
%
\A{\PAC}
\R{$\forall E$}
\U{$sk+0=sk$}
\R{\CAB}
\U{$sk=sk+0$}%(7)
\R{\CAC}
\B{$0+sk=sk+0$}%(8)
\R{$\to I^A$}
\U{$(0+k=k+0\to 0+sk=sk+0)$}
\R{$\forall I$}
\U{$\forall k.(0+k=k+0\to 0+sk=sk+0)$}%(9)
\R{\MI}
\B{$\forall y. (0+y=y+0)$}
\end{prooftree}
}
}
}\scalebox{0.4}{$\quad\cdots\cdots\quad$\fbox{$\phantom{X}A\phantom{\frac{X}{Y}}$}}
\scalebox{0.4}{
\parbox{2.7\linewidth}{
\begin{prooftree}
%
\A{\fbox{$\phantom{X}A\phantom{\frac{X}{Y}}$}}
%
\A{\fbox{$\phantom{X}A\phantom{\frac{X}{Y}}$}}
\R{$\forall E$}
\U{$0+sl=sl+0$}
\R{\CAB}
\U{$sl+0=0+sl$}%(25
%
\A{\PAD}
\R{$\forall E$}
\U{$sl+sn=s(sl+n)$}
\R{$\forall E$}
\U{$sl*sk=s(sl+k)$}%(11)
%
\A{$\bracket{sl+k=k+sl}^B$}
\R{\CAD}
\U{$s(sl+k)=s(k+sl)$}%(12)
\R{\CAC}
\B{$sl+sk=s(k+sl)$}%(13)
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. k+sn=s(k+n)$}
\R{$\forall E$}
\U{$k+sl=s(k+l)$}
\R{\CAD}
\U{$s(k+sl)=ss(k+l)$}%(14)
\R{\CAC}
\B{$sl+sk=ss(k+l)$}%(15
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. sk+sn=s(sk+n)s$}
\R{$\forall E$}
\U{$sk+sl=s(sk+l)$}%(16
%
\A{$\bracket{\forall y. l+y=y+l}^C$}
\R{$\forall E$}
\U{$l+sk=sk+l$}
\R{\CAB}
\U{$sk+l=l+sk$}
\R{\CAD}
\U{$s(sk+l)=s(l+sk)$}%(17
\R{\CAC}
\B{$sk+sl=s(l+sk)$}%(18
%
\A{\PAD}
\R{$\forall E$}
\U{$\forall n. l+sn=s(l+n)$}
\R{$\forall E$}
\U{$l+sk=s(l+k)$}
\R{\CAD}
\U{$s(l+sk)=ss(l+k)$}%(19
\R{\CAC}
\B{$sk+sl=ss(l+k)$}%(20
%
\A{$\bracket{\forall y. l+y=y+l}^C$}
\R{$\forall E$}
\U{$l+k=k+l$}
\R{\CAD}
\U{$ss(l+k)=ss(k+l)$}%(21
\R{\CAC}
\B{$sk+sl=ss(k+l)$}
\R{\CAB}
\U{$ss(k+l)=sk+sl$}%(22
\R{\CAC}
\B{$sl+sk=sk+sl$}%(23
\R{$\to I^B$}
\U{$(sl+k=k+sl)\to(sl+sk=sk+sl)$}
\R{$\forall I$}
\U{$\forall k. (sl+k=k+sl)\to(sl+sk=sk+sl)$}%(24
\R{\MI}
\B{$\forall y. sl+y = y+sl$}
\R{$\to I$}
\U{$(\forall y.l+y=y+l)\to(\forall y. sl+y=y+sl)$}
\R{$\forall I$}
\U{$\forall l. (\forall y.l+y=y+l)\to(\forall y. sl+y=y+sl)$}
\R{\MI}
\B{$\forall x. \forall y.x+y=y+x$}
\end{prooftree}
}}
\end{document}