3
$\begingroup$

After reading the relevant chapters of Classical Recursion Theory (freely available from here), I have the following questions concerning Theorem II.1.10 (Normal form theorem) and Theorem IV.1.9 (Enumeration theorem):

  • What arithmetical theory based on first-order logic is able to prove the equivalence claimed in the statement of Theorem II.1.10 (and its counterpart IV.1.9, for $\Sigma^{0}_{n}$ formulas) (Something stronger that Robinson's $\mathbf{Q}$, I guess);
  • What arithmetical theory based on first-order logic is able to prove the universal closure of the equivalence claimed in the statement of Theorem II.1.10 (and its counterpart IV.1.9, for $\Sigma^{0}_{n}$ formulas)?

Even if you don't have precise answers, useful references would be appreciated too.

Improve this question
$\endgroup$
1
  • $\begingroup$ The problem here is not so much with proving things, but defining them. The definition of computability using partial recursive function needs the totality of insanely fast-growing functions so that closure under primitive recursion makes sense. In contrast, if you use a sane definition of computability (i.e., Turing machines), then basic results such as the normal form theorem, s-n-m theorem, etc. can be proved in weak fragments of bounded arithmetic, such as PV (the basic theory of polynomial-time functions). $\endgroup$
    – Emil Jeřábek
    Commented Dec 21, 2023 at 12:17

1 Answer 1

Reset to default
4
$\begingroup$

The usual formal systems in which one can carry out basic recursion-theoretic constructions and theorems such as the ones you are asking about are $\mathrm{I}\Sigma_1$ (a fragment of $\mathrm{PA}$ in which the induction scheme is limited to $\Sigma_1$-formulas) and its counterpart $\mathrm{RCA_0}$ (a subsystem of second order arithmetic). The latter is a conservative extension of the former (i.e., any purely arithmetical statement is provable in the latter iff it provable in the former).

A good reference for the former is Chapter I of the book "Meta-mathematics of First-Order Arithmetic" by Petr Hájek and Pavel Pudlák (a free copy of which can be found here), and for the latter, the standard reference is Stephen Simpson's "Subsystems of Second Order Arithmetic".

A related MO question-and-answer is this one about formalizing Kleene's recursion theorem.

Finally: There are more spartan formal systems for handling the basics of computability/recursion theory, as pointed out by Emil Jeřábek in his comment to the question.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .