まず、上の方は明らかに勘違いかと、、
自然数論なんだから述語記号は=（と場合によっては不等号<）
しか無いです

あとはSuccesser函数Sとか足し算の記号+とか
掛け算の記号とかquantifierの組み合わせとかを使って
Prov(n,m)は実際に書き下すことが出来ます

ただ実際は膨大な長さになるので手で書き下すのは一寸きついかも