Mathematical logic

Mathematical logic is a discipline within mathematics, studying formal systems in relation to the way they encode intuitive concepts of proof and computation as part of the foundations of mathematics.

Some fundamental results

Some important results are:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

• The set of valid first-order formulas is recursively enumerable. This follows from Gödel's completeness theorem (which establishes the equivalence of validity and provability), because the set of proofs for first-order logic formulas is recursively enumerable ("semi-decidable"). Therefore, there is a procedure that behaves as follows: Given a first-order formula as its input, the procedure eventually halts if the formula is valid, and runs forever otherwise. Some first-order theorem provers have this completeness property.
• The set of valid first-order formulas is not recursive, i.e., there is no algorithm for checking for universal validity. This follows from Gödel's incompleteness theorem.
• The set of all universally valid second-order formulas is not even recursively enumerable. This is also a consequence of Gödel's incompleteness theorem.
• The Löwenheim-Skolem theorem.
• Cut-elimination in sequent calculus.
• The independence of the continuum hypothesis, proved by Paul Cohen in 1963.