Has something like the Turing Machine that halts if ZFC is inconsistent been done for other axiom systems?

93 Views Asked by At

The current best result (as far as I could find) is that there exists a $748$-state Turing Machine that halts iff ZFC contains a contradiction. Are there any similar results for other axiom systems, e.g. Peano Arithmetic? The linked source mentions this only as "an excellent [potential] project".