証明可能性

命題論理と同様に 証明可能性を定義する。すなわち，${\bf L_g}$ の要素である論理式のうち， 証明可能な論理式(provable formula)を次のように定める:

1. 公理系の各公理の形の論理式は証明可能である。
2. 論理式 $\cal A$ と論理式 ${\cal A} \Rightarrow {\cal B}$ が証明可能なら ば，(推論規則によって，)論理式 $\cal B$ は証明可能である。
3. 論理式 ${\cal A} \Rightarrow {\cal B}(a)$ が証明可能なら ば，(推論規則「全称化」によって，)論理式 ${\cal A} \Rightarrow (\forall a)({\cal B}(a))$ も証明可能である。 ただし$a$は自由変数記号で$\cal A$には現れないものとする。
4. 論理式 ${\cal A}(a) \Rightarrow {\cal B}$ が証明可能なら ば，(推論規則「特称化」によって，)論理式 $(\exists a)({\cal A}(a)) \Rightarrow {\cal B}$ は証明可能である。 ただし$a$は自由変数記号で$\cal B$には現れないものとする。

証明可能な論理式の列を「証明」という。「証明可能性」の定義に従えば

$${\cal A}_1,{\cal A}_2, \cdots,{\cal A}_n$$

が「証明」のとき。各${\cal A}_k$は

1. 公理系の各公理の形の論理式である。
2. 論理式 ${\cal A}_k$ の前に論理式 ${\cal A}_i$と${\cal A}_j$ $(i,j<k)$があり，${\cal A}_j$は ${\cal A}_i \Rightarrow {\cal A}_k$ の 形をしている。
3. 論理式 ${\cal A}_k$ の前に論理式 ${\cal A}_j$ $(j<k)$があり，${\cal A}_j$は
   

   $${\cal A} \Rightarrow {\cal B}(a)$$ (4.1)

   
   
   であり，${\cal A}_k$は
   

   $${\cal A} \Rightarrow (\forall a)({\cal B}(a))$$ (4.2)

   
   
   の形をしている。 ただし$a$は自由変数記号で$\cal A$には現れないものとする。
4. 論理式 ${\cal A}_k$ の前に論理式 ${\cal A}_j$ $(j<k)$があり，${\cal A}_j$は
   

   $${\cal A}(a) \Rightarrow {\cal B}$$ (4.3)

   
   
   であり，${\cal A}_k$は
   

   $$(\exists a)({\cal A}(a)) \Rightarrow {\cal B}$$ (4.4)

   
   
   の形をしている。 ただし$a$は自由変数記号で$\cal B$には現れないものとする。