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.

The Curry-Howard correspondence, also known as the proofs-as-programs correspondence, reveals a deep connection between computer programs and mathematical proofs.

This remarkable isomorphism shows that:

• Types correspond to propositions
• Programs correspond to proofs
• Program execution corresponds to proof normalization

For example:

• The type A → B corresponds to the logical implication A ⊃ B
• Product types (A × B) correspond to logical conjunction (A ∧ B)
• Sum types (A + B) correspond to logical disjunction (A ∨ B)

This correspondence has profound implications for both computer science and mathematics, suggesting that programming and mathematical proof are fundamentally the same activity viewed through different lenses.

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:

Boolean algebra, developed by George Boole in the 19th century, provides the mathematical foundation for digital computing and logical reasoning.

The fundamental operations in Boolean algebra are:

• AND (conjunction)
• OR (disjunction)
• NOT (negation)

These simple operations, combined with the values True and False, form a complete system for logical reasoning. This system is not just theoretically interesting - it’s the basis for all digital computer operations, from simple calculations to complex decision-making algorithms.