We present a system of sequent calculus for intuitionistic propositional logic. In later chapters we obtain stronger systems by adding rules to this basic system, and we therefore go through its proof-theoretical properties in detail, in particular the admissibility of structural rules and the basic consequences of cut elimination. Many of these properties can then be verified in a routine fashion for extensions of the system. We begin with a discussion of the significance of constructive reasoning.

CONSTRUCTIVE REASONING

Intuitionistic logic, and intuitionism more generally, used to be philosophically motivated, but today the grounds for using intuitionistic logic can be completely neutral philosophically. Intuitionistic or constructive reasoning, which are the same thing, systematically supports computability: If the initial data in a problem or theorem are computable and if one reasons constructively, logic will never make one committed to an infinite computation. Classical logic, instead, does not make the distinction between the computable and the noncomputable. We illustrate these phenomena by an example:

A mathematical colleague comes with an algorithm for generating a decimal expansion 0.a1a2a3 …, and also gives a proof that if none of the decimals ai is greater than zero, a contradiction follows. Then you are asked to find the first decimal ak such that ak > 0. But you are out of luck in this task, for several hours and days of computation bring forth only 0's …

Given two real numbers a and b, if it happens to be true that they are equal, a and b would have to be computed to infinite precision to verify a = b.