見当違いのことを言ってたら訂正をお願いします。

私が理解できないのは、
1. 形式的体系PAの各記号を自然数に一対一対応させる。
2. PAの記号からなる有限列(項や論理式)を、ある自然数に一対一対応させる。(エンコードの方法は、素因数分解を利用した関数とする。)
3. PAの記号からなる有限列(項や論理式)の有限列(証明のこと)を、上と同じ方法で自然数に一対一に対応させる。

4. 以上の考えをベースにして、形式的体系に関する概念を、算術上の述語として表現する。

5. 述語 IsTerm (x)「xは形式的体系PAの項である。」
⇔ x=/0/
または ヨn<x (IsTerm(n)かつx=/S/*par(n))
または ヨm<x ヨn<x ［IsTerm(m)かつIsTerm(n)かつ(x=par(m)*/+/*par(n)または x=par(m)*/・/*par(n) )］

このように考えた上で、私がわからないのは、
・5の定義は正しいのか
・正しいとしたら、5におけるIsTerm の特性関数はどのようになものになるのか
の二点です。
どうか教えてください。