Principia Mathematica Уайтхеда и Рассела вышла в 1910 году, но читается как современный текст по языкам программирования. В ней уже обсуждаются экстенсиональность и интенсиональность, референциальная прозрачность, типы, domain и alpha-renaming. «Неполные символы» предвосхищают продолжения и операторы управления. Авторы замечают, что свободные и связанные переменные, подстановка, абстракция и аппликация пришли из лингвистики. Похоже, Principia уже содержит lambda-calculus, а различение «any» и «all» предвосхищает интуиционизм.
Книга знаменита тем, что на тысяче страниц доказывает 1+1=2. Доказательства намеренно излишне детальны, чтобы исключить неявные посылки. Цель — показать, что базовых понятий достаточно для всей математики. Если бы книга выходила сегодня, доказательства ушли бы в приложение или в theorem prover, а главным остались бы базовые понятия.
На странице 8 — первое упоминание интенсий и экстенсий и референциальной прозрачности: если p≡q, то f(p)≡f(q). В современной записи C[p]≡C[q]. Тут же пример непрозрачного контекста «A believes p». Математика, по мнению авторов, всегда имеет дело с экстенсиями.
На странице 12 определения названы типографическими удобствами, но важными, так как показывают намерения.
Страница 15 вводит пропозициональные функции — фактически lambda-terms. «x is hurt» не утверждение, пока x не определён; «x-hat is hurt» — функция. Различаются свободные и связанные переменные, подстановка, alpha-equivalence. Страница 17 вводит «apparent variable» (связанная) и «real variable» (свободная), с аналогией с определённым интегралом.
Страницы 18–19 различают «any» и «all»: ⊢ x = x относится к любому значению, ⊢ (x).x = x — ко всем. Авторы хотят сохранить различие, хотя в их логике это эквивалентно. Здесь же ∀-введение, а на странице 20 — ∀-удаление.
На странице 20 после ∃-введения сказано, что единственный способ доказать существование — найти конкретный свидетель. Это конструктивный взгляд, опубликованный в 1910 году. Брауэр писал в то же время, но его работы были трудны; спор начался с Германа Вейля. Каретт добавил, что некоторые аспекты конструктивизма восходят к Кронекеру на 30 лет раньше.
На странице 21 впервые использовано слово «type» в современном смысле. На странице 26 — символ принадлежности это греческая эпсилон, первая буква ἐστί («быть»).
На странице 33 — первое современное определение функции через бинарное отношение: R'y — единственный x с xRy. Такие descriptive functions перекликаются с теорией дескрипций Рассела 1905 года. Каретт заметил: Principia предвосхитила различие между definite description и explicit function — аналитическое продолжение функционально, но не функция, так как включает выбор.