God, Church, Christ & the Bishop

A brief heretical history of the foundations of mathematics.

John Conway once recalled that at Princeton there were people called “God, the Church, Christ, and the Bishop.” Conway’s recollection (as recorded by Siobhan Roberts) maps, amusingly, onto four real figures: Kurt Gödel, Alonzo Church, Georg Kreisel and Errett Bishop. The joke is a joke of names—but it is also oddly apt. These four thinkers probe, in distinct ways, what mathematics is: truth, computation, proof and construction. Below I offer a short tract: irreverent in tone, but precise in purpose.

I. Genesis — God

Kurt Gödel’s incompleteness theorems force a sharp distinction between truth and provability. For any consistent, sufficiently expressive formal system there are arithmetical statements the system cannot prove. The formal apparatus—axioms and inference rules—is therefore not a plenary catalogue of mathematical reality. Gödel himself defended a form of mathematical realism: mathematical facts, for him, have an objective character that can outstrip any one formalism. (See Gödel, 1931; and for a recent compendium of Gödel’s ontological writings, cf. Gödel — Ontological Dream (2025 PDF).)

II. The Church — Computation

Alonzo Church articulated a competing boundary: not what can be proved, but what can be carried out by an effective procedure. His λ‑calculus and the Church–Turing thesis formalise the notion of mechanical computation. There are functions and decision problems no algorithm can solve; computation has limits even where mathematics has statements. Thus: God may be vast; the Church sets the rules.

III. Christ — Proof

Georg Kreisel pushed attention from the mere existence of proofs to their content. If a proof establishes ∃x P(x), what information does it encode? Proof theory asks what computational or constructive content can be extracted from non-constructive arguments. Kreisel’s investigations—on the interpretation of non‑finitist proofs and the extraction of constructive data—show that a proof can be more than a certificate: it may carry procedures, bounds and witnesses concealed within classical derivations.

IV. The Bishop — Construction

Errett Bishop’s constructive programme insists that existence must mean construction. Where classical mathematics says “there exists,” Bishop asks “show me.” In Foundations of Constructive Analysis he rebuilt analysis so that assertions correspond to algorithms or explicit constructions. The Bishop’s stance is not mere purism: it is a different ontology, one in which a mathematical claim is meaningful only when accompanied by a method to exhibit the claimed object.

V. The Council

Assemble the four. God asserts that truth can outstrip proof. The Church asks what is mechanisable. Christ asks what the proof contains. The Bishop demands a witness. These are not redundant complaints; they are complementary portraits of mathematical practice: discovery, mechanisation, content, and construction. Together they form a taxonomy of foundational questions—each one illuminating a facet the others miss.

VI. Heresy

Theatrical metaphors are useful when they do work. Here they do. The joke’s names gesture at a theological frame, but the underlying questions are technical: incompleteness (Gödel), computability (Church), proof‑theoretic content (Kreisel), and constructive existence (Bishop). The real heresy, if there is one, is to imagine that mathematics admits a single, final perspective. The subject advances by multiplying viewpoints—and by arguing about which matters most.

VII. A Final Provocation

Which of the four is the heretic? The Platonist will call the constructivist unfaithful to truth; the constructivist will call the Platonist credulous; the formalist will see both as devotees of unnecessary metaphysics; the computability theorist will ask whether any of the disputes are decidable at machine speed. That plurality is mathematics’ strength. The joke survives because the names are funny; it endures because those four ways of thinking remain alive and essential.

References

1. Roberts, Siobhan. Genius at Play: The Curious Mind of John Horton Conway. Bloomsbury, 2015. (Conway's recollection of the names.)
2. Gödel, Kurt. “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.” Monatshefte für Mathematik und Physik 38 (1931): 173–198.
3. Gödel — Ontological Dream (PDF).
4. Church, Alonzo. “An Unsolvable Problem of Elementary Number Theory.” American Journal of Mathematics 58 (1936): 345–363.
5. Kreisel, Georg. Selected work on proof theory and the interpretation of non‑finitist proofs (see Journal of Symbolic Logic, 1950s).
6. Bishop, Errett. Foundations of Constructive Analysis. McGraw‑Hill, 1967.