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.[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.
New to topics? Read the docs here!