10 ERRETT A. BISHOP Brouwer. (See references [1] , [6], 1151, 1201 , and [21] for a more com- plete exposition that we are able to give here. ) Brouwer remarked that the meanings customarily assigned to the terms "and, " "or, " "not, " "implies, " "there exists, and "for all" are not entirely appropriate to the constructive point of view, and he introduced more appropriate meanings as necessary. The connective "and" causes no trouble. To prove "A and B, " we must prove A and also prove B, as in classical mathematics. To prove "A or B" we must give a finite, purely routine method which after a finite number of steps either leads to a proof of A or to a proof of B. This is very different from the classical use of "or" for example, LPO is true classically, but we are not entitled to assert it constructively because of the constructive meaning of "or. " The connective "implies" is defined classically by taking "A impliesBfl to mean "not A or B. " This definition would not be of much value construc- tively. Brouwer therefore defined "A implies B" to mean that there exists an argument which shows how to convert an arbitrary proof of A into a proof of B. To take an example, it is clear that " ((A implies B) and (B implies C)] implies (A implies C)" is always true constructively the argument that con- verts arbitrary proofs of "A implies B" and "B implies C" into a proof of "A implies C" is the following: given any proof of A, convert it into a proof of C by first converting it into a proof of B and then converting that proof into a proof of C. We define "not A" to mean that A is contradictory. By this we mean that it is inconceivable that a proof of A will ever be given. For example, "not 0 = 1" is a true statement. The statement "0 = 1" means that when the numbers "0" and "1" are expressed in decimal form, a mechanical compari- son of the usual sort checks that they are the same. since they are already in decimal form, and the comparison in question shows they are not the same, it is impossible by correct methods to prove that they are the same. Any such proof would be defective, either technically or conceptually. As another ex- ample, "not (A and not A)" is always a true statement, because if we prove not A it is impossible to prove A -- therefore, it is impossible to prove both. Having changed the meaning of the connectives, we should not be sur- prised to find that certain classically accepted modes of inference are no long- er correct. The most important of these is the principle of the excluded

Purchased from American Mathematical Society for the exclusive use of nofirst nolast (email unknown) Copyright 1985 American Mathematical Society. Duplication prohibited. Please report unauthorized use to cust-serv@ams.org. Thank You! Your purchase supports the AMS' mission, programs, and services for the mathematical community.