Notable examples of syntactic proofs whose existence is guaranteed by completeness, but having been found later than a semantic proof?

Question

Question.

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.

Remark.

• 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.)

Answer 1

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.

Answer 2

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").

Answer 3

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$.