Our natural deduction system for first order logic is sound, in the sense that the axioms are true in any of the interpretations considered earlier and it’s not possible to derive a false statement true statements in any of those interpretations using any of our rules of inference. In fact there are no axioms, so that part, at least is easy. Of course if you look closely the statement of soundness above you’ll see a few quantifiers appearing explicitly, like “in any of those interpretations” and a few more which are implicit. So any system in which we might hope to prove the soundness of first order logic will have to include first order logic in its foundations, so a formal proof doesn’t really accomplish anything. It’s still possible to give informal proofs though. If you stare at the rules of inference you should be able to convince yourself that they are all reasonable. Of course people have convinced themselves of the reasonableness of unsound rules of inference in the past so there’s a limit to how far you should trust your intuition in these matters.
Consistency will follow from completeness, so we don’t need to consider it separately.
The system can be proved complete by roughly the same method as was used previously for zeroeth order logic. Either we can find a tableau which closes or we can’t. If we can then there is an algorithm for converting that tableau into a formal proof, and so the statement is a theorem of the system. Unfortunately though the tableau method doesn’t need to terminate, even when presented with a valid statement.
One important property of zeroth order tableaux, that every statement is shorter than the statement it was derived from, no longer holds. We might get stuck performing tableau operations forever without ever completing the tableau. We can still think of the infinite tableau that would result from this procedure though, even though we can’t produce it in finite time. A further complication comes from the variety of choices we have to make at each step. If we choose particularly badly we could continue forever even though other choices might cause the tableau to close. This is a solvable problem though. The idea, roughly, is to view the tableau method as a non-deterministic computation and use one of the hybrid traversal methods to ensure that if some set of choices has a desired property, like causing the tableau to close, then we will eventually find it. With a bit more care we can also ensure that in the case where it doesn’t close the open branches, which may be infinite, contain enough information to generate a counter-example, i.e. an interpretation which makes the statement we started with false. In that case the statement must be invalid.
The above arguments show that every statement is a theorem or is invalid. Equivalently, every valid statement is a theorem, which is completeness.