>>535
>述語論理は考えるためのルールではない。
>「論理」と書いてあるからきっと思考法にかかわるなにかだとおもってるんやろ

いわゆる論理と、論理式が充足可能か否か判定する手続きは、厳然と区別されるべきである

その上で
一階述語論理では、論理式が充足不能であるとき、その根拠が得られる手続きが存在する
（上記の根拠は、当該論理式の否定の、背理法による証明となるもの）
しかし、これは充足可能性の判定手続きではない
なぜなら充足可能な場合には、手続きが終了しないからである

それでも一階述語論理はまだましな状況である

二階論理の場合、論理式が充足不能である場合に必ずその根拠が得られるような手続きすら存在しない

つまり、充足不能の根拠が得られる場合に必ず停止するような、いかなる手続きにおいても
その手続きでは充足不能の根拠が得られないような充足不能論理式が存在する

したがって二階論理上の算術のモデルは（同型を除いて）一意とかいってみても
二階算術の任意の論理式の真偽判定には全くつながらないので無駄ってことである