Mathematical logic

Content sourced from Wikipedia, licensed under CC BY-SA 3.0.

Mathematical logic studies the formal rules for reasoning used in mathematics. It uses precise languages and axioms to understand what can be proved, how powerful those proofs are, and how mathematical theories relate to one another. The main areas are model theory, proof theory, set theory, and recursion (computability) theory, but many other logical ideas and techniques are connected to them.

Main areas
- Model theory: studies mathematical structures that satisfy given logical theories.
- Proof theory: analyzes how proofs are built and what they can show.
- Set theory: investigates sets as the basic objects of mathematics and serves as a foundation for most other theories.
- Recursion (computability) theory: looks at what can be computed by algorithms and how difficult problems are.

A brief history in plain terms
- In the 19th century, mathematicians started to axiomatize geometry, arithmetic, and analysis to remove inconsistencies.
- In the early 20th century, Hilbert sought to prove the consistency of these foundations.
- Gödel showed limits to this program: any strong enough system has true statements it cannot prove, and it cannot prove its own consistency.
- Set theory grew to formalize most of mathematics, but some questions (like the continuum hypothesis) cannot be settled using standard axioms alone.
- Over time, the field shifted toward understanding which parts of math can be formalized in specific systems and how different areas interact.

Key ideas and theorems (brief)
- Completeness: in first-order logic, every statement true in all models of a theory has a proof from the theory.
- Compactness: if every finite subset of a set of sentences has a model, then the whole set has a model.
- Löwenheim–Skolem: if a theory has an infinite model, it has models of many infinite sizes; first-order logic cannot pin down the size of infinite structures.
- Gödel’s incompleteness theorems: strong, consistent theories of arithmetic have true statements they cannot prove; such theories cannot prove their own consistency.
- Forcing and independence: some statements cannot be proved or disproved from standard axioms, using techniques from set theory.

What it’s used for
- In computer science: giving formal semantics to programming languages, proving properties about algorithms, and building automated theorem provers.
- In mathematics: providing a foundation for other areas, analyzing what can be derived from given axioms, and exploring connections to algebra, geometry, and beyond.
- In philosophy and logic: clarifying the nature of proof, truth, and mathematical justification.

A note on foundations
- Some logics extend beyond first-order logic (like higher-order or infinitary logics) and can express more ideas, but they often lose some of the convenient features (like completeness) that make first-order logic so powerful for mathematical work.
- Different foundational programs (such as constructive or predicative approaches) emphasize how we know something rather than only whether it can be proven, leading to rich ongoing research.

In short, mathematical logic asks how we formalize, prove, and understand the basic rules of mathematical reasoning, with a broad range of methods and applications across mathematics and computer science.