Decidability problem for one-formula sequent in first order logic

Question

I have a question about first order logic : is the problem of provability of one formula in first order logic decidable?

I know that for a sequent $ A \vdash B $ it's undecidable, because $ A $ can be infinite and therefore contain Peano Arithmetic. But I'm talking about a finite number or formula.

I want to be very clear for this decision problem. So let me formalize it. For all $ n \in \mathbb{N} $, we give us a countable number of relation symbols and of function symbols of arity n. We give us a countable number of variables. We use a classic encoding on the integer (I think it's easy to do, but tell me if you think I'm wrong) to encode a first order formula in this language. And I want to know if there exists a Turing machine that is decidable and that accept a number if and only if it's the encoding of a formula for which $ \vdash A $ is provable.

Ask me if anything seems unclear, I'll be happy to give more details.

Wikipedia is not very clear about that question and I don't find any (accessible or satisfying) reference. Do you have any? or do you have an answer with a proof?

Thank you for reading me, I hope my English in understandable!

Answer 1

This is still undecidable: there are finitely axiomatizable theories to which Godel's theorem still applies. The most dramatic example is probably Robinson's Q on account of its incredible weakness, but there are others including ACA$_0$ (a theory of natural numbers and sets of natural numbers which plays a central role in reverse mathematics) and NBG (a "set theory" which also talks about proper classes and often provides a more natural framework for metamathematical statements than ZFC).

---

ACA$_0$ and NBG have an interesting feature: each is in a sense a finitely axiomatizable version of a better-known non-finitely-axiomatizable theory, namely PA and ZFC respectively. Roughly speaking, ACA$_0$ is a finitely-axiomatizable conservative extension of PA and NBG is a finitely-axiomatizable conservative extension of ZFC, where $T_0$ is a conservative extension of $T_1$ iff

• the language of $T_0$ contains the language of $T_1$, and

• the theorems of $T_0$ in the language of $T_1$ are exactly the theorems of $T_1$ (and as a consequence, $T_0$ is consistent iff $T_1$ is).

• The "roughly" above reflects a minor subtlety in the NBG situation, since there are two ways of presenting NBG and one of them doesn't strictly fit the situation above. But this is a side issue which I'll ignore for now (if anyone's interested, I can address it).

This turns out to be an instance of a general phenomenon - see the discussion at this Mathoverflow question. Roughly speaking, non-finitely-axiomatizable theories "always" have finitely-axiomatizable analogues.

Meanwhile, at least in the case of PA this language expansion is necessary: an alternative proof of Godel's first incompleteness theorem in the specific case of PA, due to Kripke, yields as a corollary (instead of Godel's second incompleteness theorem!) that no consistent extension of PA in the same language is finitely axiomatizable (see also the discussion at this old Mathoverflow question). The key feature of PA here is a reflection property: for each finite subset $S$ of the usual axioms of PA, PA proves the consistency of $S$.

• This narrowly avoids contradiction since "$\forall$" and "$\vdash$" don't commute: just because for each finite $S\subseteq$ PA we have PA $\vdash Con(S)$ doesn't mean we have PA $\vdash \forall S\subseteq_{finite}$ PA$(Con(S))$.)

I believe the same is true of ZF as well, but I don't have a citation to provide immediately (although FWIW I think a Kripke-style argument will still go through there). Certainly it is true that ZF satisfies the same reflection phenomenon as PA (in fact in a stronger form).