0
$\begingroup$

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.

  1. Is this definition well-defined?
  2. Could this definition be internally self-contradictory? Do we even know?
  3. What is the relationship to True Arithmetic? Can it be in some sense stronger or are they unrelated?
  4. 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?
Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ Which kinds of statements are considered "first-order statements about Turing machines"? (E.g. are statements of the form "Turing machine X halts on all inputs" considered? Are statements of the form "Turing machine X halts for sufficiently large inputs X" considered?) $\endgroup$
    – C7X
    Commented Oct 1, 2023 at 6:17
  • $\begingroup$ @C7X Good point. It seems that this set of statements will have to contain TA in some way for many statements about halting to be well-defined. Honestly I'm not picky about how to define the set, as long as the Motivation is fulfilled. $\endgroup$
    – symmetrickittens
    Commented Oct 1, 2023 at 7:01
  • 9
    $\begingroup$ Since statements about Turing machines can be coded in arithmetic and vice versa, I see no significant difference between "true computation" and "true arithmetic". I think any difference would have to be created by imposing some (artificial) restrictions on the expressive power of one of the two theories. (This might have been the reason for @C7X's Comment, asking about the expressive power.) $\endgroup$
    – Andreas Blass
    Commented Oct 1, 2023 at 13:17

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .