What are examples (preferably documented and explicitly commented on from this perspective in the literature, preferably in an article dedicated to this aspect alone) of the following well-known aspect of the usual completeness theorem for first-order logic (summarizing it here slightly flippantly, for brevity)?

If $\mathbb{T}$ is a theory in first-order logic (with $=$) over a language $L$, and if $\sigma$ is any $L$-sentence, and if $\vDash$ denotes entailment w.r.t. a given semantics for $L$, and if $\vdash$ denotes existence of a finite proof w.r.t. a given usual proof system, and if you prove $\mathbb{T}\vDash\sigma$ with no holds barred, then you know the existence-statement $\mathbb{T}\vdash\sigma$ to be true.


  • Motivation for the question is partly expository writing, partly my working on an open problem about triangle-free graphs whose statement is one first-order sentence in a relational language.

  • It seems especially interesting, in particular for expository purposes, to have notable examples of a first-order syntactic proof having to exist by the completeness theorem but not yet having been found so far (and researchers in the field being aware of that and deploring it), and there being some hope that the shortest syntactic proof is short enough to be found in future (and possible even appreciably simple).

  • Even though my research-motivation is about a statement which does not even use function-symbols, my exposition does not make any such restriction to purely relational languages, and I would also appreciate examples involving first-order statements which do use function symbols.

  • In expositions (I will not give examples here since such mentionings would be rather negativistic, to the effect of "Look, Author A does not give an example.") of the usual completeness theorem for first-order logic, one sometimes encounters a discussion pointing out the above consequence of the completeness theorem, but I have not seen any notable example being given in such expositions. It is easy to devise very artificial examples.

  • The metaphor "with no holds barred" in the above refers to any mathematical theory or logic being allowed to prove that each model of $\mathbb{T}$ is a model of $\sigma$.

  • This MO thread is similar in spirit, but technically quite different.

  • All famous examples (that I can think of, that is) of ("elementary" here in an informal sense) elementary statements first being proved by non-elementary methods and later being given an elementary proof do not qualify as examples, for one technical reason or the other. (For example, it would be too much of a stretch to pass off e.g. the elementary proofs given by P. Erdős and A. Selbert of the theorem on the distribution of the primes as an example. The statement each Robbins algebra is a Boolean algebra fits the logical bill, but there the first-proved-by-semantic-non-elementary-methods-bit is totally lacking: the first proof found for this was syntactic. Some other examples I tried do not fit for similar reasons.)


3 Answers 3


There's a good reason that concrete examples are going to be rare. Existence of a first-order proof (at least in a countable language) is a $\Sigma_1$ property in the language of arithmetic, and it's a general metamathematical principle that proofs of $\Sigma_1$ statements should be constructive.

More precisely, if you have a proof that such a proof exists via the completeness theorem, one should be able to formalize this proof in some strong enough theory of arithmetic and then extract a syntactic proof (for instance, using the functional (or "Dialectica") interpretation). That doesn't mean there can't be such examples---the process of extracting a syntactic proof could be tedious, or simply not done yet---but it's unusual and unlikely to last for long if there's interest in obtaining a syntactic proof.

  • $\begingroup$ And do you agree that if the statement involves function symbols, then it is not completely clear that "existence of a first-order proof" is $\Sigma_1$-definable? Not that this would be my main concern (my main concern is indeed a language similar to the language of set-theory, which is purely relational), I am just trying to work out a few technicalities. And I am aware, that function symbols are usually defined in terms of the purely-relational language of set-theory, I am just trying to go through how this is done. $\endgroup$ Jul 20, 2017 at 5:32
  • $\begingroup$ Many thanks. This is nicely explanatory and general contribution. A few questions: what do you consider a usual reference for a first-order proof itself being $\Pi_0$ in the Lévy hierarchy? It is sort-of evident that it is, at least with some coding (like coding implications as inclusions), but, without getting into too much issues here, I would like to check a few technical things against a reference. $\endgroup$ Jul 20, 2017 at 9:18
  • 1
    $\begingroup$ This is just as clear when the language includes function symbols. The set of results needed is usually called the "Arithmetization of Syntax". Because it's a basic result, I don't know any modern expositions outside of textbooks which don't complicate it by proving something fancier, but I'm fond of the exposition in Enderton's A Mathematical Introduction to Logic. $\endgroup$ Jul 20, 2017 at 17:15

If you are willing to consider completeness of fragments of first-order logic, one example that would follow under your scheme is the conservativity of classical logic over its fragment of coherent logic. Before the proof of Barr's theorem (1974), which settles this conservativity result, the way to see it was via Deligne's completeness theorem from SGA IV (1972) stating that a coherent topos has enough points. This is essentially a completeness theorem for coherent logic with respect to (set-valued) models. Therefore, if there is a proof in classical logic of a coherent sequent $\sigma$ from a set of coherent axioms $\mathbb{T}$, by soundness it is true in all set models, and therefore the completeness of coherent logic implies that it must be provable already in the coherent fragment.

However explicit transformations of classical proofs of the coherent sequent from coherent axioms into proofs in the coherent fragment were not obtained until later. One of them is given in Palmgren, E.: "An intuitionistic axiomatisation of real closed fields" (2002) by using the Dragalin-Friedman translation. Another is in Sara Negri's "Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem" (2003) where the transformation follows from cut elimination. (Negri uses the word "geometric" to mean "coherent").


George Boolos has a nice example in "A Curious Inference", where $\mathbb{T}\vDash\sigma$ is obvious from second-order or semantic considerations, but $\mathbb{T}\vdash\sigma$ is of Ackermann difficulty in first-order logic, so that anyone would come across the first proof first.

More tangentially from my other answers: Jeremy Avigad surveys this for $\mathbb{T}\vDash\{\sigma\in S\}$ and $\mathbb{T}\vdash\{\sigma\in S\}$; Harvey Friedman has an example for $\mathbb{T}\nvDash\sigma$ and an elemetary proof of $\mathbb{T}\nvdash\sigma$.

  • $\begingroup$ Many thanks. Looking into that closely will take some time. A cursory reading makes it seem as if Boolos is using the function symbols primarily to ensure the "difficulty". But as I said, I will have to look into this more closely. $\endgroup$ Jul 20, 2017 at 5:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.