Analogous to the model of True Arithmetic, the model of "True Computation" is defined to be the set of all true first-order statements about Turing machines i.e. answers to elementary questions like how many states does it have, what will it do at state $X$ when looking at symbol $Y,\ldots$ as well as undecidable questions like if it will halt on input $Z$ or not and what will it output?

**Motivation**: It is known that some theories can "reason about Turing machines" (if Turing machine $X$ halts on input Y and outputs $Z$ then the theory proves that statement and not any statements that intuitively contradicts it, like "the Turing machine also outputs $W$ at the same time"), be consistent and yet prove some wrong statements about Turing machines i.e. proves that one halts when it doesn't actually halt. My intuition is that Turing machines can be used as a baseline to gauge the semantic correctness of a (consistent) theory, if we (somehow) have access to all true statements about Turing machines.

I have several questions.

- Is this definition well-defined?
- Could this definition be internally self-contradictory? Do we even know?
- What is the relationship to True Arithmetic? Can it be in some sense stronger or are they unrelated?
- If we have some kind of oracular access to this model, can we decide if the axioms of some theory are actually semantically correct Platonian-style, for example the axioms of Peano arithmetic, ZFC or ZFC + Continuum Hypothesis?