Decision procedure vs Proof system in Predicate Logic

Question

I recently started reading Logic in Computer Science and in section 2.5 the authors talk about decision procedures. They state in Theorem 2.22, "The decision problem of validity in predicate logic is undecidable: no program exists which, given any $\phi$, decides whether $\models \phi$". But from my understanding $\models \phi \rightarrow \vdash \phi$ by the completeness theorem, and you can show is $\vdash \phi$ is a theorem by using analytic tableaux (a proof procedure not present in this book) which is (in my understanding) an algorithmic procedure. It seems that this is a contradiction! So obviously I'm missing some important piece of information. I'd really appreciate if someone could clear this up.

Answer 1

When you state that $\models\phi\implies\vdash\phi$, this is for propositional logic - that is, without quantifiers. Yes, there is a decision procedure for propositional logic. However, predicate logic involves quantifiers. This type of logic has no decision procedure.

Answer 2

The method of tableaux is a proof procedure that, when applied to a valid formula $X$ (i.e. starting the tableaux with $FX$), produce in a finite number of steps a closed tableaux (i.e. a tableaux showing that $FX$ is unsatisfiable), i.e. a proof of the formula.

But if the formula is not vaid, you can go on forever without closing it. Thus, the proof procedure is not a decision method because we have no way to know in advance (in the general case) if a formula of f-o logic is valid or not (a f-o "version" of truth table may involve an infinite number of cases to be managed).