The Discovery of E.W. Beth's Semantics
for Intuitionistic Logic

A.S. Troelstra and P. van Ulsen

Faculteit WINS
University of Amsterdam
Plantage Muidergracht 24
1018 TV Amsterdam
The Netherlands


One of van Benthem's predecessors, and the first in line of the Dutch logicians, was Evert Willem Beth. During the last decade of his life he worked on a truly constructive semantics for intuitionistic logic, with a corresponding completeness theorem. The result is known as ``Beth models''. We try to describe his intents and efforts, but it is not possible to give a clear story line: the data are too scarce. However, we attempt a reconstruction. For this we not only used published records, but as much as possible also quotes from correspondence. Beth semantics combine trees, tableaus, choice sequences and fans. Intuitionistically acceptable completeness required Beth to avoid certain classical notions, in particular König's Lemma. Instead, Beth used Brouwer's fan theorem.

Bibtex Entry