Abstract. Our goal is to formalize the famous Church-Turing thesis.
Specifically, the notion of an “effective model of computation” over an
arbitrary countable first-order structure is axiomatized. This is accomplished
by modifying Gurevich’s “Abstract State Machine” postulates.
Then a proof is provided that effective models are of equivalent computational
power to Turing Machines, using a quasi-ordering on computational
models that captures comparative extensional power.