The lambda calculus, developed by Alonzo Church in the 1930s, is a minimal but powerful model of computation based purely on function abstraction and application.

In lambda calculus, everything is a function. The only operations are:

1. Variable reference: x
2. Function creation (abstraction): λx.M
3. Function application: (M N)

Despite (or perhaps because of) this simplicity, the lambda calculus can express all computable functions. It forms the theoretical foundation for functional programming languages and has deep connections to both logic and mathematics through the Curry-Howard correspondence.

Category theory provides a unifying framework for mathematics itself, abstracting away details to reveal deep structural similarities between different mathematical concepts.

A category consists of:

1. Objects
2. Arrows (morphisms) between objects
3. A composition operation for arrows
4. Identity arrows for each object

This simple structure appears everywhere in mathematics:

• Sets with functions
• Groups with homomorphisms
• Topological spaces with continuous maps
• Propositions with logical implications

Through concepts like functors, natural transformations, and adjunctions, category theory reveals connections between seemingly unrelated areas of mathematics. It’s often called “the mathematics of mathematics” because it provides a language for describing mathematical structures and their relationships.

First-order logic (FOL) provides the formal language in which most of mathematics is written. Unlike propositional logic, which deals only with true/false statements, FOL introduces quantifiers and predicates that allow us to express much more complex ideas.

The two fundamental quantifiers in FOL are:

• Universal quantifier (∀): “for all”
• Existential quantifier (∃): “there exists”

These powerful tools allow us to express statements like:

• ∀x ∃y (y > x) - “For every number, there exists a larger number”
• ∀x (x = x) - “Everything is equal to itself”

The precise syntax and semantics of FOL provide the rigor needed for mathematical proofs while remaining intuitive enough to express natural mathematical ideas.

Modal logic extends classical logic by adding operators for necessity (□) and possibility (◇). This powerful framework allows us to reason about not just what is true, but what must be true and what could be true.

The basic axioms of modal logic (in the system K) are:

1. □(p → q) → (□p → □q) [Distribution Axiom]
2. If p is a theorem, then □p is a theorem [Necessitation Rule]

From these simple beginnings, we can develop rich systems for reasoning about:

The Axiom of Choice (AC) is perhaps the most controversial axiom in mathematics. It states that given any collection of non-empty sets, we can select exactly one element from each set to form a new set.

While this seems intuitive for finite collections, its application to infinite collections leads to some surprising and counterintuitive results, such as the Banach-Tarski paradox, which proves that it’s possible to take a solid ball, cut it into a finite number of pieces, and reassemble those pieces to create two identical copies of the original ball!