I’m not familiar with your textbook, so I’ll refer to the exposition of tableaux method contained in R.Smullyan, First-Order Logic (1968, Dover reprint, 1995).
A preliminary comment is needed : unfortunately, mathematical logic uses “completeness” in two different contexts (which ones, it will be clear - I hope - in a moment).
A) Let us start with the simple case of sentential logic. Here we have the notion of tautology and the method of truth-tables. Truth-tables are an (inefficient but effective) device to test for “tautologuesness”.
When we set-up a proof system for sentential logic, we choose (zero or more) axioms and some (at least one) rules of inference; with an Hilbert-style proof system, typically we have modus ponens.
We call theorems of the proof system all the formulae that are deducible, i.e. “produced” starting from the axioms with a finite number of applications of the rules of inference.
There are a lots of different way to set up a proof system; but the basic properties we are requesting to it are the following :
1) it must be sound : assuming that all the axioms are tautologies, we want that all the theorems must be tautologies (i.e. rules of inference must preserve the property of being a tautology);
2) it must be adequate : we want that all the tautologies must be deducible from the axioms (this second properties is usually called completeness of the proof system).
With a sound and adequate proof system, the property of being a theorem is decidable : test a formula $A$ with truth-tables; if it is a tautology, then it is a theorem (and some proof of the "completeness" of sentential logic give an effective method to build the deduction of the theorem in the proof system).
As you said, the refutation tree method (or the tablaux method ) for sentential logic is complete (I say adequate), in the sense that if applied to a tautology, all the paths of the tree will close after a finite number of step.
If the tree is finished (and in sentential logic this will always happen after a finite number of steps) with some path that is not closed, the formula is satisfiable (and its negation isn’t a tautology).
You must take into account two features of sentential logic :
a) the refutation tree will always finish after a finite number of steps (because at each step the “complexity” of the formulae – in terms of occurrences of connectives - will decrease)
b) the truth-table device allows us to check in advance if a formula $A$ is a tautology or not.
P.S. Please, note that, is not true that for every formula $A$, $A$ is a tautology or $\lnot A$ is a tautology. There are formulae, like $p \rightarrow q$, which are not tautologies, and whose contradictory (i.e. $\lnot (p \rightarrow q)$ ) are not tautologies either.
B) If now we move to first-order logic, most of the above concepts are still applicable. Instead of tautology, we have the notion of (logical) validity. I assume that we are familiar with the basic semantic notion for f-o logic : interpretation, model, validity (i.e.true in every interpretation) and logical consequence.
We must note the first difference compared to sentential logic: in f-o logic the device of truth-tables will not work any more; in general, the number of combination to be tested is infinite.
Adding suitable axioms for quantifiers, we will have a proof system for f-o logic that is sound and adequate with respect to validity. Again, the refutation tree method (or the tablaux method ) for f-o logic is complete (I say adequate), in the sense that if applied to a valid formula, all the paths of the tree will close after a finite number of step.
But now, applying the method to a formula $A$ that is not valid (i.e. such that $\lnot A$ is satisfiable) we have that either the tree is finite and a path is open or there is a path that continues to infinity.
Again, you must remember that there are sentences (i.e.closed formulae) like $\exists x \exists y ( \lnot x = y)$ that are not valid (because not satisfiable in an interpretation with only one object in the domain) and whose negation $\forall x \forall y (x = y)$ is not valid either (because not satisfiable in an interpretation with more than one object in the domain).
Taking into account that we cannot check in advance if $A$ or $\lnot A$ are valid or not, if we run the refutation method with a couple of formulae like the above, and if after a finite number of steps neither of the two trees is finished, we are not licensed to conclude anything.
This is the reason why the refutation method does not violate the (meta-)theorem about the undecidability of f-o logic.
Last comment about first-order logic. We said that the proof system is adequate when : if $A$ is valid, then $A$ is deducible (i.e. if $\vDash A$, then $\vdash A$) : this result is called Godel’s Completeness Theorem.
It can be stated in a more general form saying that : if $\Gamma \vDash A$, then $\Gamma \vdash A$. All the logical consequences of a set of assumptions are deducible within the proof system.
C) About completeness of a formalized theory
We say that a formalized theory $T$ (e.g.formal arithmetic, based on the f-o proof system with the first-order version of Peano’s axioms) is
negation complete if, for every sentence $\phi$ expressible in the language of the theory, either $T \vdash \phi$ or $T \vdash \lnot \phi$, i.e. either $\phi$ or $\lnot \phi$ is deducible in $T$’s proof system (see Peter Smith, An Introduction to Godel’s Theorems, 1st ed, 2007 : pag.2).
We are interested to know if a theory like formal arithmetic is negation complete or not, because with a
complete theory of arithmetic we could in principle use the theory to prove the truth or falsity of any claim about addition and/or multiplication (or at least, any claim we can state using quantifiers like "for all", connectives like "if" and "not", and identity). And if that’s right, truth in arithmetic could just be equated with provability in this complete theory (P.Smith, loc.cit., pag.2).
Godel’s (first) Incompleteness Theorem says that if $T$ has a decidable set of axioms (like f-o Peano’s axioms) and is expressive enough (in a specifiable sense) and is consistent , then there is a sentence $\sigma$ that is true in the intended model but it is not deducible from the axioms, i.e.is unprovable in $T$. Formal arithmetic is NOT complete.
But using the more general form of G’s Completeness Th for f-o logic, we have that the proof system of $T$ is complete (i.e.adequate). How we reconcile this with G’s Incompleteness Th for $T$ ?
The reason is that the unprovability of $\sigma$ proves that it is not a logical consequence of f-o Peano’s axioms. Because the proof of Godel’s Incompleteness shows us (with insight) that $\sigma$ must be true in our “intuitive” domain of natural numbers, from it follows also that there are some models (different from the intended one) where $\sigma$ is false.
I hope it can help you.
