Mathematical Logic

Mathematical logic is a formal system consisting of axioms and inference rules: by repeatedly applying the inference rules to the axioms (and to the previously derived theorems), new theorems can be one derived within the system.

For example, the definition of the natural numbers by Peano axioms: zero is a natural number; each natural number has a successor which is also a natural number. Therefore, starting with 0 and repeatedly applying the successor function we can generate a list of natural numbers (the new theorem).

Mathematical logic studies and builds theorems about a system of objects, only the objects it deals with are the theorems themselves and the system of objects is the entire mathematics.

Mathematical logic studies the application of technics of formal logic to math, explores formal systems of deductive reasoning in formal proof systems.

Mathematical logic is closely associated to metamathematics, foundations of mathematics and theoretical computer science.

The aim of logic in CS is to develop formal languages that can model concepts so we can reason about these models by constructing valid arguments, which can be rigorously defended and proved, and, preferably mechanically, checked for correctness.

History of mathematical logic

Logic becomes an important part of math, especially of the foundations of mathematics, the math field that attempts to come up with the first principles from which the entirety of math could be derived.

The interest in the mathematical foundations has arose in the late XIX century with the newly established set theory, which almost immediately was shown to suffer from inconsistencies. This problem, coupled with the previously discovered issue with (Euclidean) geometry, has lead many, but most of all, the highly-influential German mathematician David Hilbert, to come up with the program aimed at proving, once and for all, the consistency of foundational theories of mathematics.

The early XX century was marked with attempts to solve the 25 issues that consituted the Hilbert's program, and/or to solve the overall challenge and prove math to be consistent and sound.

Results of Kurt Gödel, Gerhard Gentzen, and others provided partial resolution to the program, and clarified the issues involved in proving consistency. Work in set theory showed that almost all ordinary mathematics can be formalized in terms of sets, although there were some theorems that could not be proven in a common axiom system for set theory.

Contemporary work in the foundations of mathematics often focuses on establishing which parts of mathematics can be formalized in particular formal systems (as in reverse mathematics) rather than trying to find theories in which the entire math can be developed.

This period was also marked by the significant effort to reduce mathematics to logic, the movement which was called logicism, whose most prominent leaders were Russell and Whitehead that were attempting to derive math from logic in their magnum opus "Principia Mathematica". The work on "Principia" lasted for years and had exhausted both authors so much that they have abandoned completing all the planned volumes. As a famous example to illustrate how difficult this endavour was, it is often mentioned that it took them about 300 pages to show that 1 + 1 = 2, deriving this equation from the first princliples.