I am confused about the relationship between the quantifier complexity of formulae in the language of arithmetic and the computational classification of the sets those formulae define.
Specifically, my question can be boiled down to asking whether or not adding the minimization operator $μ$ to a primitive recursive formula always produces a $Δ^0_1$, total computable function. If this is the case, what is the proof, what guarantees the minimization always returns a value? If this is not the case, how does this not violate Post’s theorem?
What is confusing to me is that the minimization operator seems to perfectly correspond to an unbounded existential quantifier in my mind, i.e. they both are recursively enumerable but not recursive. If the number we’re looking for exists, an unbounded search will find it after a finite time. But if the number doesn’t exist, we will search forever. The minimization operator is often introduced in the context of loops. $Δ^0_1$ formulae have bounded quantifiers so they are clearly analogous to for loops, while the minimization operator is analogous to a while loop. But while loops are not guaranteed to halt (“while false, loop”), so how does fixing a minimization operator to a primitive recursive formula always produce a $Δ^0_1$ formula? If it doesn’t always, then the general recursive functions are not closed under minimization, which I thought was the point of the formalism, and we have general recursive functions which are $Σ^0_1$ which contradicts both my understanding of what Post’s theorem says and the definition of general recursive.
My only idea of how this could be solved is that, given Kleene’s normal form theorem, we know that we only need one use of minimization, which means we can always make the formula the minimization is attached to primitive recursive, and that somehow guarantees that the value the minimization is searching for will exist so it won’t loop forever, but I don’t know why that would be true if it is true. I guess the other option is that I do not understand Post’s theorem, or “general recursive/computable”. I always thought “general recursive/computable” meant the total functions closed under the primitive recursive functions and minimization, not the (non total) partial functions. As in, I thought the general recursive functions were the functions which are recursively enumerable and their complements are recursively enumerable, but not the functions which are recursively enumerable but whose complements are not recursively enumerable.
I know that I’m wrong about something, probably multiple things, but I cannot find an explicit answer to these questions in any textbook I have access to. What am I missing?