ロッサーのからくり
formula_1が十分な算術を含むなら、すべての論理式formula_9に対し、formula_54はformula_55を含意することを証明可能であることが、定義から直ちに従う。なぜならば、もしそうでなければ、2つの数formula_56が存在し、それぞれformula_9とformula_18の証明のコードであり、formula_59とformula_60の両方を満たすからである (実はformula_1に必要なのはそのような状況がいかなる2数に対しても起き得ないことの証明と、いくばくかの一階述語論理のみである)。