量化子をつけた推論ってどうやるのかな？で、調べてみたら量化子の除去規則で量化子を消して単項命題にして推論をするみたい。A(x)を述語とみたらA(x)は命題ではないので推論の対象にならないが、A(x)をxに任意の項を代入した単項命題とみなしたときは推論してもいいらしい。じっさいの証明でも「∀xA(x)」は「任意のｘについてA(x)」としてA(x)について推論していくから、じっさいの推論と量化子除去＆単項命題の推論は整合している。
\[
\newcommand\sp[1]{\hspace #1em}
\newcommand\sub{\lower 1em}
\]
\[
\displaylines{
\underline{\forall x A(x)}\rlap{\sub{\forall 消去}} \\
\underline{[A(x)]} \\
\underline{\sp{1} \vdots \sp{1}} \\
\underline{\sp{2} B(x)\sp{2}}\rlap{\sub{\to 導入}} \\
\underline{\sp{1} A(x) \to B(x)\sp{1}}\rlap{\sub{\forall 導入}} \\
\forall x (A(x)\to B(x)) \\
}
\]
が、単項命題とかたんなる言い訳で結局、述語A(x)で推論してるやんというのが正直な感想。色々考えてみたが、A(x)はA(1),A(2),......という具体的な命題を列挙したものの省略表記と解釈するのが一番納得がいくような気がする
\[
\displaylines{
\underline{\sp{6}\forall x A(x)\sp{6}}\rlap{\sub{\forall 消去}} \\
\underline{[A(1)]\sp{4}[A(2)]\sp{4}[A(3)]} \\
\underline{\sp{1}\vdots\sp{6}\vdots\sp{6}\vdots\sp{1}} \\
\underline{\sp{2}B(1)\sp{4}B(2)\sp{4}B(3)\sp{2}}\rlap{\sub{\to 導入}} \\
\underline{A(1) \to B(1)\sp{1}A(2) \to B(2)\sp{1}A(3) \to B(3)}\rlap{\sub{\forall 導入}}\\
\forall x (A(x)\to B(x)) \\
}
\]
抽象思考できない具体例の列挙でしかものごとを納得できないあんこ脳なので、こういう解釈をするしかない。
(参考）
１階述語論理の自然演繹
論理学入門
論理学入門」講義ノート