{c}

<Jocelyn Quaintance> coauthored mathematical expositions on computation with <Jean Gallier>. Their <Introduction to the Theory of Computation: Computability, Complexity, and the Lambda Calculus by Jean Gallier and Jocelyn Quaintance (2020)> develops links among formal computation, <lambda calculus> and arithmetic.<Introduction to the Theory of Computation: Computability, Complexity, and the Lambda Calculus by Jean Gallier and Jocelyn Quaintance (2020)>[Title page and chapters 4 and 6]{ref}

The arithmetic chapter distinguishes the finite axioms of <Robinson arithmetic> from the <mathematical induction> schema used in <Peano arithmetic>. This matters computationally: a formal language can express arithmetic operations while different axiom systems prove different claims about them. The exposition connects symbolic rules with limits on what algorithms and formal proofs can establish.


 Jocelyn Quaintance (source code)