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