The theorem which states that in mathematical logic, if a formula is logically valid, then there is a finite formal proof of the formula based on the axioms of the system—something that a computer could be programmed to do. This is important in its own right but is perhaps even more important as the precursor to Gödel’s Incompleteness Theorems.