Comment by strbean

> any logical framework which can express Peano arithmetic

(with a finite list of axioms)