Nisan comments on Formulas of arithmetic that behave like decision agents

[Nisan]

Yep, this sounds about right. I think one do has to prove “#a > #b if a > b”, or rather

)