Up 7.1.3 式変形システム／推論システム  

  1. Gの上の文変形システム

    U＝( S， D)， S＝( G,σ, R)

    は，以下のようになる：

    1. G＝( NＶ, TＶ, Ｐ, SEN)：

      1. NＶは，述語論理の NＶに
          NUM，Ｎ：数項シェマ記号の生成に関する
          NVR：数変項シェマ記号の生成に関する

        を追加したもの。

      2. TＶは，TＶと述語論理のTＶの合併に
          num： 原初数項シェマ記号
          nvr： 原初数変項シェマ記号

        を追加したもの。

      3. Ｐは，述語論理のＰに，以下を追加したもの(註):

          TRM → NUM
          NUM → NVR
          NUM → NUM′
          NUM → NVR
          NUM → １
          NUM → Ｎ
          Ｎ → Ｎ1
          Ｎ → num
          NVR → NVR1
          NVR → nvr


    2. σは，述語論理のσに

        NUM → NUM
        NVR → NVR

      を追加したもの。

    3. R，Dは，述語論理のものと同じ。


  2. U＝(S,D) については，Uの変更に対応する変更を行なうことの他に，つぎの“自然数の公理”を追加する：

      (N0) num＝num1 → num′＝num1′
      (N1) ε→ ¬(num′＝1)
      (N2) num′＝num1′→ num＝num1
      (N3) sen[nvr↓1]∧(sen⊃sen[nvr↓nvr']) → sen

ここでの (N1),(N2),(N3) が，“ペアノの公理”と呼ばれているところのものである。


（註） このとき，
num，num1，num11，････
nvr，nvr1，nvr11，････

が数項シェマ記号，数変項シェマ記号の全て。