Direct and indirect proof, syntactical and semantical A first-order sentence is (logically) valid iff it's true in every interpretation. And it's valid iff it can be deduced from the FO axioms alone.
One normal case of showing that a FO sentence is true is deducing it (syntactically).
I guess that indirect proofs have to be interpreted more "semantically": 
"Assume that ~F is true in an interpretation. [Deduction of a contradiction] Thus ~F couldn't have been true. Thus F must be true in every interpretation." (But we are left without a deduction of F from the axioms.)
Is this reading of indirect proofs correct?

Are there also direct proofs that
  work "semantically", i.e. that show
  directly that a sentence is true in
  every interpretation? 

Like truth tables do.
 A: I hope I won't mess this up; been some time since I played around with logics.
A key feature of every sound, consistent logic is that you can not prove $false$. If you add $\neg F$ to the assumptions (what is exactly what you do) and can now prove $false$ (by deriving a contradiction) -- syntactically, i.e. for all interpretations! -- the only reason for that can be that $\neg F$ is not true for any interpretation. This implies that $F$ holds for any interpretation.
Note that if you want to enter this in an interactive theorem prover, you might have to take care that all variables in $F$ are free or bound only in $F$.
A: We can easily turn an indirect proof of a theorem (or proof of a theorem by contradiction) into an ordinary direct syntactic proof.  This is a special case of the Deduction Theorem which tells us that if $\Sigma \cup \{A\} \vdash B$ for some collection of statements $\Sigma$ and specific statements $A$ and $B$, then $\Sigma \vdash A \rightarrow B$.  Specifically, if we let $A$ be $\lnot F$ and $B$ be some contradiction $C \land \lnot C$ derived from $\Sigma \cup \{\lnot F\}$, then the deduction theorem tells us that we have a proof of $\lnot F \rightarrow (C \land \lnot C)$ from $\Sigma$.  But since $F$ is a tautological consequence of this last statement, we can extend such a proof of this $\Sigma$-theorem to a proof of $F$.  This direct syntactic proof of $F$ then gives us a direct semantic proof by Gödel's completeness theorem for first-order logic. 
Note that the Deduction Theorem itself is a metatheorem that can be proven by induction on the length of the proof of $B$ from $\Sigma \cup \{A\}$, and its proof provides us with a constructive way of getting the actual proof of $A \rightarrow B$ from $\Sigma$.  
