Is there a way to state the (in)completeness theorem for an arbitrary deductive system?

Is there a way to state the content of completeness theorems "in general" that a) treats logics like FOL and SOL and theories like arithmetic the same way and b) does not make explicit reference to a syntactic consequence relation / proof calculus like $\vdash_{LK}$?

I'm trying to understand the meaning (but not yet the proofs) of various completeness theorems. As a first step, I'm trying to understand whether each (in)completeness theorem is special and has its own bespoke set of definitions or whether there's a way to talk about the content of a completeness theorem for an arbitrary deductive system, whether it has nonlogical axioms or not.

For first-order logic, the completeness theorem, as far as I know, consists of picking a sound and complete deductive system (such as the sequent calculus LK) and proving that $\models$ and $\vdash_{LK}$ are coextensive. The consequence relation $\vdash_{LK}$ is also computable as a function $\mathrm{Set[Wff]} \times \mathrm{Wff} \to 2$, i.e. $\vdash_{LK}$ is recursively enumerable. Since $\vdash_{LK}$ and $\models$ are coextensive this means that $\models$ is recursively enumerable too. I have a sneaking suspicion that this is wrong. Intuitively, I know that I can computably verify a proof in FOL, but I can't computably produce one. I don't know how to talk about a proof though in a way that isn't intimately tied to the specifics of FOL.

For second order logic, I think there's an incompleteness theorem that shows that there is no analogue to $\vdash_{LK}$. I think this is equivalent to saying that $\models_{\mathrm{SOL}}$ is not recursively enumerable. I think.

For the theory of arithmetic, I'm honestly not sure what the story is. I intuitively think of the incompleteness theorem for arithmetic as meaning that if there's a set of axioms $A$ that when combined with $\vdash_{\mathsf{FOL}}$ axiomatizes true arithmetic, then $A$ must not be recursively enumerable. I don't think this is completely right though, since I'm baking the completeness of FOL into my statement and talking separately about logical and nonlogical axioms/inference rules.

Solution 1:

Yes, this can be done in various ways. Here's a gloss on one particular approach I quite like:

The (first) incompleteness theorem can be phrased as an undefinability theorem:

No completion of $\mathsf{PA}$ is simply definable in $\mathfrak{N}=(\mathbb{N};+,\times)$.

Of course "simply" is a huge weasel-word here; many completions of $\mathsf{PA}$ are $\mathfrak{N}$-definable after all. We want a stronger notion of definability which lines up with computability. One such definition was observed by Kreisel and further analyzed by Moschovakis and others (see Krei63, Mosc69 if you're interested). I'll butcher it a bit, but the essence is the following:

Given a structure $\mathfrak{A}$ and a first-order theory $T$ satisfied by $\mathfrak{A}$, say that a first-order formula $\varphi(x_1,...,x_n)$ in the language of $\mathfrak{A}$ is invariant on $\mathfrak{A}$ given $T$ iff for every $\mathfrak{B}\models T$ and every embedding $h:\mathfrak{A}\rightarrow\mathfrak{B}$ we have $\varphi^\mathfrak{B}\cap\mathfrak{A}^n=\varphi^\mathfrak{A}$. A relation $R$ on $\mathfrak{A}$ is invariantly definable on $\mathfrak{A}$ given $T$ if there is some formula $\varphi$ which is invariant on $\mathfrak{A}$ given $T$ and has $\varphi^\mathfrak{A}=R$.

There are two key observations here:

• First, invariant definability as presented above lives in the context of first-order logic. We could also whip up an analogous notion of (say) second-order invariant definability: just let $T$ range over second-order theories and $\varphi$ range over second-order formulas.

• Second, unlike mere first-order definability, invariant definability is a very strong condition. For example, take $T$ to be the theory of groups. The center of a group is defined by the formula $\zeta(x)\equiv\forall y(x*y=y*x)$. Since every group embeds into a group with trivial center (exercise), the formula $\zeta$ is not invariant on $\mathfrak{A}$ given $T$ for any group $\mathfrak{A}$ with non-trivial center. (Of course $\zeta$ is "half-invariant" - if $\mathfrak{A}\models\neg\zeta(a)$ and $h:\mathfrak{A}\rightarrow\mathfrak{B}$ is an embedding of groups then $\mathfrak{B}\models\neg\zeta(a)$ - but I'm really just briefly treating the notion of invariance here, so let's ignore this sort of nuance.)

Putting these together, what the idea of invariance really gives us is a way of carving out "concrete" fragments of a "big" logic. This puts us in Godel territory! The connection between (classical) computability and invariant definability (on $\mathfrak{N}$ given some mild theory of arithmetic) is that the following are equivalent:

• $R$ is invariantly definable on $\mathfrak{N}$ given $T$, for some c.e. theory $T\subseteq Th(\mathfrak{N})$.

• $R$ is invariantly definable on $\mathfrak{N}$ given Robinson's arithmetic $\mathsf{Q}$ in particular (so no need to go to a complicated theory in the above bulletpoint!).

• $R$ is computable.

This is really just a quick tweak on the more common result that the computable relations are exactly those which are representable in $\mathsf{Q}$. Think of invariant definability as generalizing representability.

It turns out that the first incompleteness theorem can be phrased as follows:

$(*)\quad$ If $T\subseteq Th(\mathfrak{N})$, no consistent completion of $T$ is invariantly definable on $\mathfrak{N}$ given $T$.

Proof sketch: Suppose $S$ is a consistent completion of $T$ and $\varphi$ invariantly defines $S$ in $\mathfrak{N}$ given $T$. Let $\mathfrak{M}\models S$. Then in particular, $\mathfrak{M}\models T$ and $S=Th(\mathfrak{M})\supseteq T$. By invariance-given-$T$ of $\varphi$ we have that $Th(\mathfrak{M})$ is the standard part of a parameter-freely-definable subset of $\mathfrak{M}$, namely $\varphi^\mathfrak{M}$, but this contradicts Tarski's undefinability theorem. $\quad\Box$

Note that there's no restriction here to computable theories $T$! In particular, if we take $T=Th(\mathfrak{N})$ itself we just recover Tarski's undefinability theorem (of course we used Tarski in the proof above so this doesn't actually give a new proof of Tarski, but it is a useful "reality check"). Admittedly I'm conflating theories and sets of Godel numbers here, but meh for now.

The formulation $(*)$ generalizes immediately to all logics and "reasonable" Godelization functions (we just need the map from formulas to numbers to satisfy a couple mild definability conditions). Even $\mathfrak{N}$ can be varied here: there is a general notion of a structure be "sufficient" for representing a given logic, and as long as $\mathfrak{A}$ is sufficient for $\mathcal{L}$ we get a Godel-type theorem for $\mathfrak{A},\mathcal{L}$. If you're interested, I'll add more details.