I think it is helpful to think along the following lines (which are developed more fully -- with lots of nice tree diagrams which I can't reproduce here! -- in my Intro. to Formal Logic, which you might find helpful).
Think of trees (tableaux) as coming in three flavours. First, we set out to -- as it were -- do a truth table backwards. Instead of evaluating an argument $\varphi_1, \varphi_2, \ldots \varphi_n \therefore \psi$ by hacking through a truth table to see if there is a valuation which makes the premisses true and conclusion false, we go the other way about. We start by assuming that $\varphi_i$ is true, $\varphi_2$ is true, $\ldots$, $\varphi_n$ is true and $\psi$ is false, and then try to see whether we can work backwards to find a valuation which yields these assignments to the $\varphi_i$ and $\psi$. We may have to consider branching possibilities (e.g., from $P \lor Q$ is true, we can only infer that either $P$ is true or $Q$ is true). This sort of doing-a-truth-table-backwards, sometimes having to split our reasoning to consider alternative paths, is naturally set out using signed trees where the nodes on the tree are decorated by expressions of the kind "$\varphi \Rightarrow T$" or "$\psi \Rightarrow F$" (where "$\Rightarrow T/F$" means "is assigned the value $T/F$"). These signed trees are evidently introduced as a way of setting our metalogical semantic reasoning, to establish whether the semantic entailment $\varphi_1, \varphi_2, \ldots \varphi_n \vDash \psi$ holds.
Second, instead of having some wffs assigned $T$ and others assigned $F$, why not just rewrite trees so that every wff appearing on them is assigned $T$? Whenever you are tempted to write "$\varphi \Rightarrow F$" write instead "$\neg\varphi \Rightarrow T$". You'll end up with uniformly signed trees, with every wff decorated the same way.
Third, since in the second version all the wffs are decorated the same way, you can just drop the assignments of values to get unsigned trees. Now, the original motivation for these signed trees remains semantic, so the natural way of reading them, as they are first introduced, is still as shorthand for semantic reasoning to establish semantic entailment.
However, we can now think of these unsigned trees a different way -- as formal proof objects involving no mention of truth (we've dropped the assignments of truth-value remember). And we can define a corresponing notion of syntactic entailment where $\varphi_1, \varphi_2, \ldots \varphi_n \vdash_T \psi$ [that's subscript $T$-for-trees] just when there is a closed tree whose trunk starts $\varphi_1, \varphi_2, \ldots \varphi_n, \neg\psi$. A closed tree can then be regarded as exhibiting a syntactic entailment in this sense. (We then need a proof that trees in any flavour work as advertised, and in particular we will want it to be the case that $\varphi_1, \varphi_2, \ldots \varphi_n \vdash_T \psi$ iff $\varphi_1, \varphi_2, \ldots \varphi_n \vDash \psi$.)
Best Answer
Keep in mind that proofs are "easily-recognizable finite strings of symbols" - precisely, we can effectively enumerate all proofs from a given theory. So we can always find a formal proof of $F$ from $T$ - if one exists - effectively by simply checking each $T$-proof in order until we find one which is a proof of $F$. This is unsatisfying, but is perfectly precise and effective.