---
title: "A Set of Postulates for the Foundation of Logic"
authors:
  - "Alonzo Church"
year: 1932
venue: "Annals of Mathematics"
arxiv: null
doi: "10.2307/1968337"
source: "https://doi.org/10.2307/1968337"
topics:
  - lambda-calculus
  - church
  - logic-foundations
seed_rank: 512
seed_batch: "foundations-greats-2026-08-13"
reviewed: "2026-08-13"
pool: "maths-foundations"
relevance_score: 9
lineage: foundations-of-computing
cites:
  - title: "A Set of Postulates for the Foundation of Logic (second paper)"
    url: "https://doi.org/10.2307/1968172"
    year: 1933
    arxiv: null
    doi: "10.2307/1968172"
  - title: "A Formulation of the Simple Theory of Types"
    url: "https://doi.org/10.2307/2266170"
    year: 1940
    arxiv: null
    doi: "10.2307/2266170"
  - title: "The Calculi of Lambda-Conversion"
    url: "https://press.princeton.edu/books/paperback/9780691083940/the-calculi-of-lambda-conversion"
    year: 1941
    arxiv: null
    doi: null
  - title: "Grundlagen der kombinatorischen Logik"
    url: "https://doi.org/10.2307/2370619"
    year: 1930
    arxiv: null
    doi: "10.2307/2370619"
see:
  - "513-a-set-of-postulates-for-the-foundation-of-logic-second-paper"
  - "510-a-formulation-of-the-simple-theory-of-types"
  - "511-the-calculi-of-lambda-conversion"
  - "497-grundlagen-der-kombinatorischen-logik"
---

# A Set of Postulates for the Foundation of Logic

## One-sentence takeaway

Church's 1932 postulates introduce free-variable λ-abstraction as a logical foundation—before Kleene–Rosser showed the system inconsistent.

## Why it matters here

Origin story of λ as a language, not yet as a programming calculus. The inconsistency is why typed λ and combinatory logic both exist: Schönfinkel–Curry combinators stay type-free and consistent enough to compute, while Church retreats to simple types in 1940.

## Key ideas

- Attempts to found all of logic on a type-free calculus of functions and abstraction.
- λ appears here as a logical primitive, not yet as a model of computation.
- Kleene and Rosser later derive a paradox from the unrestricted system, forcing the 1940 type hierarchy.
- Companion 1933 paper (card 513) extends the postulates before the collapse.

## Caveats

## Links

- DOI: [10.2307/1968337](https://doi.org/10.2307/1968337)
- JSTOR: https://www.jstor.org/stable/1968337