---
title: "A Set of Postulates for the Foundation of Logic (second paper)"
authors:
  - "Alonzo Church"
year: 1933
venue: "Annals of Mathematics"
arxiv: null
doi: "10.2307/1968172"
source: "https://doi.org/10.2307/1968172"
topics:
  - lambda-calculus
  - church
  - logic-foundations
seed_rank: 513
seed_batch: "foundations-greats-2026-08-13"
reviewed: "2026-08-13"
pool: "maths-foundations"
relevance_score: 8
lineage: foundations-of-computing
cites:
  - title: "A Set of Postulates for the Foundation of Logic"
    url: "https://doi.org/10.2307/1968337"
    year: 1932
    arxiv: null
    doi: "10.2307/1968337"
  - 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: "λ-definability and recursiveness"
    url: "https://doi.org/10.1215/S0012-7094-36-00227-2"
    year: 1936
    arxiv: null
    doi: "10.1215/S0012-7094-36-00227-2"
see:
  - "512-a-set-of-postulates-for-the-foundation-of-logic"
  - "510-a-formulation-of-the-simple-theory-of-types"
  - "526-lambda-definability-and-recursiveness"
---

# A Set of Postulates for the Foundation of Logic (second paper)

## One-sentence takeaway

Church's 1933 sequel extends the untyped logical λ-system that Kleene–Rosser would shortly prove inconsistent.

## Why it matters here

Completes the 1932–33 foundation attempt. After the paradox, the same abstraction apparatus is reused as a theory of computation (1936) and then as simple type theory (1940)—the fork ano still lives on.

## Key ideas

- Continues the 1932 postulates with further rules for the type-free calculus.
- Still treats λ as a foundation for logic rather than as a programming notation.
- Historical path: once the system is known inconsistent, conversion and definability survive as the computational remnant.

## Caveats

## Links

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