Abstract: The Introduction explains the issues raised by constructive logic for different traditions; principally, for mainstream constructive mathematics treated here, and for the foundational tradition, the subject of Part II. The material is arranged under the following headings. 1. Flashy metatheorems and some neglected implications. For example, classical proofs of Π02 theorems are essentially no harder to unwind than corresponding constructive, more precisely, intuitionistic proofs. In short, intuitionistic restrictions tend to be too weak in practice, incidentally despite the (little known) elegance of their metatheory documented in a digression. 2. Weakness of the constructive meaning of Π03 → Π03. This is illustrated by reference to various elementary implications of this form between familiar finiteness theorems in arithmetic. A proviso is formulated which corrects that weakness, and is often satisfied in practice. 3. Metamathematics of classical systems: modern variants of Hubert's program without detour via constructive logic. For example, some recalcitrant proofs of Π02 theorems have in fact been unwound by suitable functional interpretations such as the n.c.i.; cut elimination is generally less efficient. 4. Applying the n.c.i.: reassurances (about additional skills needed for successful applications, beyond knowing the metatheory of the n.c.i.). Attention is drawn to proof strategies used in ordinary mathematics, of comparable generality to logical metatheorems, where similar additional skills are needed, and have proved to be available. Much the same applies to successful applications of model theory which, contrary to superficial impressions, are shown to involve operations on proof's, and not only on the theorem proved. 5. Algebraization: reminders and surprises (principal section). By reference mainly to recent literature, the potential of algebraization and a couple of other general mathematical strategies in the sense of 4. above is documented, and contrasted with logical contributions to the constructive tradition in mathematics. Remarkably many significant and general points are illustrated by work on sums of squares and by the Appendix. The latter supplements section 2. by reference to the most sophisticated implication between finiteness theorems in the number-theoretic literature. Particular attention is given to realizing the 'proviso' mentioned in 2., or, equivalently, to making a proper choice between various meanings of the popular phrase: from a counterexample to the conclusion we get one to the premise. - The Appendix can be read independently of the main text.
Publication Year: 1982
Publication Date: 1982-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 59
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot