[strbean]

> any logical framework which can express Peano arithmetic

(with a finite list of axioms)

[jrvidal]

I think the precise pre-condition is that the theory should be recursive, which means either a finite list of axioms _or_ a computable check to determine whether a given formula is an axiom.