推論規則

以下の推論規則が用いられます。 横線の上の関係式から下の関係式が導かれることを表わします。

$$(\exists x){\cal P}(x,y)$$

の$y$のように$\forall$や$\exists$が作用していないものは自由変数と呼ばれます。

1. 三段論法
   
   $$\frac{{\cal A} \quad {\cal A} \Rightarrow {\cal B}}{\cal B}$$
   
   

2. 　全称化
   
   $$\frac{{\cal A} \Rightarrow {\cal B}(a)} {{\cal A} \Rightarrow (\forall a)({\cal B}(a))}$$
   
   
   ただし$a$は自由変数記号で$\cal A$には現れないものとします。
3. 　特称化
   
   $$\frac{{\cal A}(a) \Rightarrow {\cal B}}{(\exists a)({\cal A}(a)) \Rightarrow {\cal B}}$$
   
   
   ただし$a$は自由変数記号で$\cal B$には現れないものとすします。

前述の公理自身もそうですが,公理と,上の推論規則を用いて導かれる 関係式を「証明可能な関係式」,あるいは,「定理」, 「命題」などと呼びます。またその導出の過程が「証明」です。

上の推論規則と公理を何回か適用する共通した手順を「推論法則」と呼びます。 これ自身は,公理系を扱うのに必須ではないですが，それを操作する上で便利な手続き をまとめたものです。以下に推論規則の例を述べます。

1. 添加
   
   
   $$\frac{\cal A }{{\cal B} \Rightarrow {\cal A}} \qquad ({\bf 推論法則：添加})$$
   
   

   これは${\cal A}$が証明可能な関係式であるとき,(即ち定理であるとき) ${\cal B} \Rightarrow {\cal A}$も証明可能,即ち定理ですことを表しています。

2. 論理積
   
   
   $$\frac{\cal A,B }{{\cal A} \land {\cal B}} \qquad ({\bf 推論法則：論理積})$$
   
   

   これは ${\cal A},{\cal B}$が証明可能な関係式であるとき, ${\cal A} \land {\cal B}$も証明可能ですことを表しています

   以下,それぞれの規則意味の説明は省略します。

3. 論理積の交換
   
   
   $$\frac{\cal A \land B }{\cal B \land A} \qquad ({\bf 推論法則：交換})$$
   
   

4. 論理和の交換
   
   
   $$\frac{\cal A \lor B }{\cal B \lor A} \qquad ({\bf 推論法則：交換})$$
   
   

5. ２重否定
   

   
   

   $$\frac{\cal A }{\lnot \lnot A},\quad \frac{\lnot \lnot A}{A} ({\bf 推論法則：２重否定})$$
   
   

6. 推移
   
   
   $$\frac{ \cal A \Rightarrow B ,B \Rightarrow C } {\cal A \Rightarrow C}({\bf 推論法則：推移})$$
   
   

7. 複推移
   
   
   $$\frac{ \cal A \Rightarrow (B \Rightarrow C) ,A \Rightarrow B } {\cal A \Rightarrow C}　({\bf 推論法則：復推移})$$
   
   

8. 対偶
   
   
   $$\frac{{\cal A } \Rightarrow {\cal B}} {\lnot {\cal B} \Rightarrow \lnot {\cal A}} \qquad ({\bf 推論法則：添加})$$