# Is there a standard notion of a “theory of Turing machines”?

Of course, there are more-or-less standard definitions of Turing machines as a certain type of mathematical object formalized in some theory (Say, ZFC), but what I am looking for is a first order theory of Turing machines themselves. Is there a standard notion of such a first order theory of Turing machines in the literature? The basic properties I would be looking for would be the following (or something similar):

The main objects in the language of the theory would be Turing machines, and the only atomic propositions of the theory are of the form $\mathrm{halts}(T,a,t)$ which says intuitively something like "The Turing machine $T$ halts on input $a$ at time $t$ in the execution".

In particular, I am interested in the connections between such a theory and Peano Arithmetic, and wish to find a result in the literature stating that these be equiconsistent theories.

• A few comments: First, if you want to include expressions like $halts(T, a, t)$, then you probably want to include natural numbers as objects as well - otherwise, what sort of thing are "$a$" and "$t$"? Second, you may be interested in partial combinatory algebras. – Noah Schweber Jan 28 '17 at 17:31
• @NoahSchweber Of course those would also have to be specified inside of the theory for the description to work, I did not intend to give a complete specification of what I am looking for in my question, but I will look into partial combinatory algebras. – Nathan BeDell Jan 28 '17 at 17:40