14 ERRETT A. BISHOP If we let "A" be any such result, with the constructive interpretation, then the constructive version of the corresponding classical result will be (for instance) "LPO + A, as we have seen. My feeling is that is likely to be worth whatever extra effort it takes to prove "A" rather than "LPO + A. " The linguistic developments I have outlined could be taken as the basis for a formalization of constructive (and therefore of classical) mathematics. So as not to create the wrong impression, I wish to emphasize again certain points that have already been made. Formalism The devil is very neat. It is his pride To keep his house in order. Every bit Of trivia has its place. He takes great pains To see that nothing ever does not fit. And yet his guests are queasy. All their food, Served with a flair and pleasant to the eye, Goes through like sawdust. Pity the perfect host! The devil thinks and thinks and he cannot cry. Constructivism Computation is the heart Of everything we prove. Not for us the velvet wisdom Of a softer love. If Aphrodite spends the night. Let Pallas spend the day. When the sun dispels the stars Put your dreams away. There are at least two reasons for developing formal systems for con- structive mathematics. First, it is good to state a s concisely and system- atically as we are able some of the objects, constructions, terminology, and methods of proof. The development of formal systems that catch these aspects of constructive practice should help to sharpen our understanding of how best to organize and communicate the subject. Second and more important, in- formal mathematics is the appropriate language for communicating with people, but formal mathematics is more appropriate for communicating with machines. Modern computer languages (see the report [30], for example). while rich in facilities, seem to be lacking in philosophical scope. It might be worthwhile to investigate the possibility that constructive mathematics would
Previous Page Next Page