The formal system described above is sound for any interpretation of the type discussed earlier. This implies consistency as well. It is also complete. The easiest way to prove this is by giving an algorithm for converting a closed tableau into a proof in the natural deduction system. We’ve already seen how to find, in finite time, a closed tableau for any valid statement so every valid statement has a proof. If you like complete systems you should take a moment to enjoy this fact before reading further. This is the last complete system we will see.