30 ERRETT A. BISHOP done, we should increasingly turn our attention to questions of the efficiency of our algorithms, and bridge the gap between constructive mathematics on the one hand and numerical analysis and the theory of computation on the other. Since constructive mathematics is the study of what is theoretically comput- able, it should afford a sound philosophical basis for the theory of computa- tion. Our terminology and technical devices need constant re-examination as to whether they are the most appropriate tools for extracting the full meaning from our material. It seems to me that the meaning of implication, in partic- ular, should be thoroughly studied, and other possible candidates investi- gated. Such statements as "(A + B) + C" have a rather tenuous meaning, and in many instances of proofs of such statements, something more is actually being proved. Work of Gadel [17] raises some interesting possibilities about possible re-definitions of implication, which seem to be very difficult to imple- ment in usable generality, and which also seem to run counter to natural modes of thought. There seems to be no reason in principle that we should not be able to develop a viable terminology that incorporates more than one meaning for some or all of the quantifiers and connectives. More important than any of these technical problems is the broader problem of involving ourselves more deeply with the meaning of mathematics at all levels. This is the simplest and most general statement of the con- structivist program, and the technical developments are intended as a means to that end.

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.