November 2017
Intermediate to advanced
670 pages
17h 35m
English

In 1936, a German mathematician named Gerhard Gentzen provided proof that first-order arithmetic (addition and multiplication) is consistent using primitive recursive arithmetic. Gentzen used sequent calculus, which is a conditional tautology (a series of true statements) to build arguments according to rules and procedures of inference (https://en.wikipedia.org/wiki/Inference) with zero or more assertions. Note that sequent calculus is very similar to natural deduction, which is composed of one or more assertions.