Reference for a "recursive" fragment of infinitary logic?

Question

Does anyone know of any texts or papers out there concerning properties of the fragment of $ \mathcal{L}_{\omega_1, \omega} $ in which the only admissable infinite conjunctions are those which are recursive, when infinite conjunctions are considered as functions $ \omega \to \omega $ for some appropriate encoding of the language?

Answer 1

Yes, these are called computable infinitary formulas. I recommend the following references (as a matter of taste I prefer them to Barwise...don't remember why...possibly just it's more canonical in my field):

Computable Structures and the Hyperarithmetical Hierarchy by Ash and Knight

To a lesser extent

Forcing and Reducibilities. II. Forcing in Fragments of Analysis by Odifreddi

---

But if you understand Kleene's ordinal notations it's a pretty trivial definition (modulo a few mostly irrelevant technical details).

Basically you introduce the notion of an infinite computable disjunction of formulas. That being a c.e. set of codes for infinite computable sentences.

Since you can take infinite disjunctions (and negations) there is no longer any need for $\exists$ and $\forall$ as they get absorbed into the infinite versions. If you want to say there is some number $x$ satisfying $\phi$ you just write the computable $\Sigma_1$ sentence that is a disjunction of $\phi(n)$ for each $n$ (assuming you working in a countable structure...I don't know if this makes sense in uncountable structures see the Ash and Knight book). This makes things a little simpler.

Thus the computable infinitary formulas are just those formulas built up in this fashion and obviously go up all the way to $w_1^{CK}$.

There are only two annoying technical details. The first is how to assign codes to the formulas. One wants to take a bit of care here about whether to include the rank (ordinal notation) the formula appears at in it's code. I believe you want to avoid this given the difficulties posed by incompatible notations and computability problems it brings. The downside is that you have to be a bit clever to recover the rank from formula but this is done in the textbook once and glossed over subsequently.

The only other minor problem is how do you define $\Sigma_\lambda$ at limit levels. There are two competing standards. One just takes it to be the collections of all formulas at levels below the other takes it to be computable disjunctions of those formulas.