scientific article; zbMATH DE number 1289305
adjunction between syntax and semanticscategory theoryfoundations of mathematicslatticesposetsstructural recursionsyntactic category of a theorytextbook
Mathematics in general (00A05) Methodology of mathematics (00A35) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to ordered structures (06-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to category theory (18-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01)
In 1971, \textit{Carl E. Linderholm} published a book entitled: ``Mathematics made difficult (Wolfe Publishing Ltd., London) (1971; Zbl 0217.00102), in which he attempted to satirize the way in which (as he saw it) `abstract nonsense' was taking over the foundations of mathematics and making them incomprehensible. Nearly 30 years later, Paul Taylor has finally written the book of which ``Mathematics made difficult was a parody. That is not intended as a criticism of ``Practical foundations of mathematics; the reviewer has little sympathy with Linderholm's rather heavy-handed `humour', and is of the opinion that Taylor has written a splendid and highly enjoyable book. But the parallel between the two books is inescapable. Taylor's book is both didactic and descriptive: it attempts to explain how mathematicians and informaticians (the latter being the author's appealing term for theoretical computer scientists) should view the foundations on which their work is based, but at the same time it attempts to tease out the logical structure underpinning the informal way in which mathematicians actually argue -- both today and in previous eras of history. It is this latter feature which makes it very different from most books on the foundations of mathematics, but at the same time brings it closer to Linderholm's satire. (To take two examples, the detailed description of the history of the algorithm for solving the general cubic equation, and its presentation as a program in the semi-formal language developed by the author (p.~198), remind one irresistibly of the tribulations of M.~Boulangiaire in chapter 3 of ``Mathematics made difficult. And the author's concern for Bo Peep's difficulties in counting her sheep, evidenced by Exercise 1.1 on p.~60, might have been lifted straight from Linderholm's discussion of whether one can use the same number-system for adding and for counting.) Mention of exercises is a reminder that this book is, at least partly, intended as a textbook. What sort of students could benefit from courses based on it? The author's own suggestion is that `the first three chapters should be accessible to final year undergraduates in mathematics and informatics'; this is probably true, provided the mathematics undergraduates have rather more familiarity with programming languages (and the informaticians have more familiarity with non-discrete mathematics) than is usual. (And both groups would find the exercises pretty hard going.) It is, above all, beginning graduate students in both disciplines who will find this book most useful; it will prompt them to think seriously about the foundations of their subjects, and the relations between them, in a way that no other existing book (known to the reviewer) can achieve. Indeed, if it succeeds in becoming widely used and quoted (as it deserves to do), then it may bring about an altogether new level of understanding, by each of the two groups, of the way in which the other group thinks about the subject it studies. At the heart of the book, not surprisingly, is category theory. It is therefore a little unexpected not to find a chapter headed `Introduction to Categories' or something of the sort; Chapter III on posets and lattices is immediately followed by a chapter entitled `Cartesian Closed Categories'. However, readers who are newcomers to category theory should not despair: Chapter IV does largely consist of an introduction to category theory (albeit a rather more condensed one than that found in most textbooks on category theory), and this together with Chapter V on `Limits and Colimits' will serve to introduce such readers to all the important concepts of the subject (except, rather oddly, for adjunctions, which are held back until Chapter VII, although adjoint functors between posets have been treated in Chapter III). The author's other main theme is structural recursion, which forms the title of Chapter VI but which, like the categorical notion of adjoint functor, actually pervades the whole book. Chapter VI itself is a tour of various aspects of recursive definitions: free algebras, the general recursion theorem (formulated, in the style of Gerhard Osius, as a theorem about well-founded coalgebras), tail recursion, and Kuratowski-finiteness. But the thing which links all of these to each other, and to the categorical ideas which are omnipresent in the foundations of mathematics, is the notion of the syntactic category of a theory and the syntax/semantics adjunction. These topics are covered more fully in the last two chapters, which introduce the notions of dependent types, fibrations and the categorical notion of quantification. Although, in these later chapters, the going inevitably gets tougher (as befits the subject-matter), the author's style remains user-friendly without becoming imprecise: a student who works through to the end of the book will (rightly) feel a real sense of achievement, but there is no reason why he shouldn't get there if he perseveres. The book's collection of references is splendidly eclectic; Taylor is extremely good at pointing out the (sometimes surprising) sources of ideas that most of us take for granted, and at finding apposite quotations to support his argument. Indeed, the reviewer suspects that many readers will gain more enjoyment from reading the footnotes than they do from the text of this book. (The reviewer's favourite footnote, a rare unattributed example, is on page 192.) Taylor's insistence on spelling out the forenames of cited authors, whenever he knows them, may at first seem irritating to a reader brought up on the tradition of initials-plus-surname, but one soon gets used to it. Indeed, by the time one reaches the Bibliography, one is tempted to wonder what crimes Godfrey Harold Hardy can have committed in Taylor's eyes, to cause him to be reduced to `G. H.'. In this respect, if in no other, Taylor's book is inferior to Linderholm's!
- A new framework for declarative programming
- Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
- Darboux calculus
- Distributivity of categories of coalgebras
- Computational adequacy for recursive types in models of intuitionistic set theory
- What is a finitely related object, categorically?
- Localization, monoid sets and \(K\)-theory
- A categorical framework for learning generalised tree automata
- M-shaped and other exotic solitons generated by cubic-quintic saturable nonlinearities in a nonlinear electrical transmission network with higher-order dispersion effects
- Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies
- Relative full completeness for bicategorical Cartesian closed structure
- Symmetric Heyting relation algebras with applications to hypergraphs
- Map composition generalized to coherent collections of maps.
- Kernels, in a nutshell
- Ordinals in Frobenius monads
- Recursive coalgebras from comonads
- Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness
- Understanding one another: making out meanings with Boolean equations
- Type-theoretic approaches to ordinals
- Filter pairs and natural extensions of logics
- Logic of negation-complete interactive proofs (formal theory of epistemic deciders)
- Quantum logic in dagger kernel categories
- Generic tools via general refinement
- Relations on hypergraphs
- The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
- Two-dimensional models of type theory
- The Dedekind reals in abstract Stone duality
- Recursive coalgebras of finitary functors
- scientific article; zbMATH DE number 5306929 (Why is no real title available?)
- Parameterised notions of computation
- Quotient completion for the foundation of constructive mathematics
- scientific article; zbMATH DE number 6981655 (Why is no real title available?)
- Bicategories in univalent foundations
- Bicategories in univalent foundations
- Cubical syntax for reflection-free extensional equality
- A cubical language for Bishop sets
- Identity types and weak factorization systems in Cauchy complete categories
- Pick two points in a tree
- Logic of intuitionistic interactive proofs (formal theory of perfect knowledge transfer)
- Well-founded coalgebras, revisited
- General refinement. II: Flexible refinement
- Contexts, refinement and determinism
- Extending conceptualisation modes for generalised formal concept analysis
- Intuitionistic sets and ordinals
- The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
- Semantic analysis of normalisation by evaluation for typed lambda calculus
- Proof theory in the abstract
- Semi-abelian categories
- A Categorical Aspect of the Analogy Between Quantifiers and Modalities
- Bicategorical type theory: semantics and syntax
- Constructing initial algebras using inflationary iteration
- GATlab: modeling and programming with generalized algebraic theories
- Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
- Congruence filter pairs, equational filter pairs and adjoints
- Continuous and algebraic domains in univalent foundations
- Initial algebras unchained -- a novel initial algebra construction formalized in Agda
- Algebraic presentations of type dependency
- Categories for collection monads
- Strict universes for Grothendieck topoi
- Trees in coalgebra from generalized reachability ((co)algebraic pearl)
- A 2-categorical approach to the semantics of dependent type theory with computation axioms
- Duality for clans: an extension of Gabriel-Ulmer duality
- Free doubly-infinitary distributive categories are Cartesian closed
- The identity type weak factorisation system
- CPO semantics of timed interactive actor networks
- Kleisli morphisms and randomized congruences for the Giry monad
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4243759)