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.


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