Given a first-order logic theory $T$ and and a formula $F$, suppose I have semantically proved that $T\vdash F$. That is, I have proved that any model $M$ of $T$ satisfies $F$ and I conclude by Gödel's completeness theorem.
Do I have a general algorithm to extract from the above a syntactic proof of $T\vdash F$, i.e. a finite sequence of formulas that respects inference rules, uses $T$ and finishes at $F$ ?
If no such algorithm exists, then did I really prove $T\vdash F$ ? The completeness theorem was just an example of how to indirectly prove that there exists a proof of $T\vdash F$, without explicitly giving this latter proof. What if my indirect proof uses an inaccessible cardinal, do I have to mention the awkward $$ (\text{ZFC + Inaccessible cardinal})\; \vdash\; (T \vdash F) $$ And then this proof can also be indirect, so I might continue stacking theories to the left and it becomes a nightmare. Don't semantic or other indirect formal proofs somewhat defeat the purpose of formal logic, that we should be absolutely certain that the formal proofs exist and are correct?