**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](https://mathoverflow.net/questions/71201/are-there-examples-of-statements-that-have-been-proven-whose-consistency-proofs) 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.)



Notable examples of syntactic proofs whose existence is guaranteed by completeness, but having been found later than a semantic proof?
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.


