ロッサーのからくり
T {\displaystyle T} が無矛盾であるという仮定のもとでは、各論理式 φ {\displaystyle \phi } ごとに、論理式 Pvbl T R  ( # φ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )} が成り立つことと Pvbl T  ( # φ ) {\displaystyle \operatorname {Pvbl} _{T}(\#\phi )} が成り立つことは同値である。なぜならば、もし φ {\displaystyle \phi } の証明のコードが存在するならば、( T {\displaystyle T} の無矛盾性の仮定に従い) ¬ φ {\displaystyle \neg \phi } の証明のコードは存在しないからである。しかしながら、 Pvbl T  ( # φ ) {\displaystyle \operatorname {Pvbl} _{T}(\#\phi )} と Pvbl T R  ( # φ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )} は T {\displaystyle T} における証明可能性の観点からは異なる性質を持つ。
T {\displaystyle T} が十分な算術を含むなら、すべての論理式 φ {\displaystyle \phi } に対し、 Pvbl T R  ( φ ) {\displaystyle \operatorname {Pvbl} _{T}^{R}(\phi )} は ¬ Pvbl T R  ( neg ( φ ) ) {\displaystyle \neg \operatorname {Pvbl} _{T}^{R}({\text{neg}}(\phi ))} を含意することを証明可能であることが、定義から直ちに従う。