ABSTRACT
We take for granted in everyday practice that the number systems we use — like the real numbers with + , − , · and / — are reliable and stable. Of course, we sometimes make mistakes adding or dividing numbers, but we know that if 5+7 = 12 today, the same is true tomorrow, and this is why we can correct the person who claims that the sum is 11 . + , − , · and / are functions, and so for any pair of numbers they give a unique value. That is, an application of these operations cannot result in both n and m — what would lead to n = m — if n and m are distinct numbers. Moreover, it is widely believed that no such equations will emerge from calculating with numerical functions; that is, the theory of such functions is consistent. In the case of a formalized theory, such as Peano arithmetic (PA), this property can be formalized as “0 = 1 is not provable” (in PA).1 A similar question may be asked concerning CL: Is there an equation (with =w or even =wζ ) between CL-terms that does not hold? In this chapter, one of the paramount results is that CL is consistent. We give a rigorous proof of this with =w — though we do not aim at formalizing the notion of consistency or the proof in CL itself.
