Add section on \Sigma_1 completeness to the chapter on representability in Q

[beastaugh]

This fills out the chapter on representability in Q by showing that the various lemmas used in proving that computable functions are representable in Q can be extended to the entire class of Sigma_1 sentences.

[rzach]

This is great. I'm going to put it in but place it after the undecidability section if that's ok?

There are some things I'd probably change if I had time. E.g., I'm not sure we define what a "Boolean" connective is, I don't like "implication" for $\to$, probably should tokenize "correct" (I might want to call it "true in N") etc. Time for that later.

One question before I merge this though: you say that a generalized $\Sigma_1$ is built up from ... using conditional and unbounded existentials. But if an unbounded existential is in the antecedent then the whole is not equivalent to a $\Sigma_1$ formula. Mistake or do you not intent extended $\Sigma_1$ formulas to be equivalent to $\Sigma_1$ formulas?

The second half of the last paragraph probably comes too early and should instead come after incompleteness (Prf etc not yet defined). In the long run I think we should grow this into a chapter where we define the formula classes more precisely, show $\Sigma_1$ completeness, define $\Delta_1$ formulas, show that the formulas representing p.r. and partial recursive functions are $\Delta_1$--and so get the result that the computable functions are exactly the $\Delta_0$-definable ones.

[beastaugh]

I'm going to put it in but place it after the undecidability section if that's ok?

I wasn't sure where was best, before or after the undecidability section. So moving it is fine by me.

There are some things I'd probably change if I had time. E.g., I'm not sure we define what a "Boolean" connective is, I don't like "implication" for → , probably should tokenize "correct" (I might want to call it "true in N") etc. Time for that later.

I've pushed a new commit that tidies things up somewhat, including replacing "correct" with "true in N" and "Boolean" with "propositional" (I think in the rest of the text they're just called connectives, with connectives plus quantifiers being referred to as 'operators', but this is less ambiguous).

One question before I merge this though: you say that a generalized Σ 1 is built up from ... using conditional and unbounded existentials. But if an unbounded existential is in the antecedent then the whole is not equivalent to a Σ 1 formula. Mistake or do you not intent extended Σ 1 formulas to be equivalent to Σ 1 formulas?

I think I probably put this in with the intention of generalising some of the results, but ended up not doing it. For now I've just removed the relevant parts of the definitions. If we want to add more material later we can always add a correct version back in.

The second half of the last paragraph probably comes too early and should instead come after incompleteness (Prf etc not yet defined).

For now I've just removed the whole paragraph—I don't think it does much work without the second half.

In the long run I think we should grow this into a chapter where we define the formula classes more precisely, show Σ 1 completeness, define Δ 1 formulas, show that the formulas representing p.r. and partial recursive functions are Δ 1 --and so get the result that the computable functions are exactly the Δ 0 -definable ones.

Yes, in the longer term I'd like to do that. This would lay the groundwork for adding more computability theory material, like Post's theorem.