No label defined (Q4247300)

Author's opening statement: ``After millennia of mathematics we have reached a level of understanding that can be represented physically. Humankind has managed to disentangle the intricate mixture of language, metalanguage and interpretation, isolating a body of formal, abstract mathematics that can be completely verified by machines.'' The paper proceeds with reflections on connected concepts from philosophy of mathematics. Constructivity, for example, is developed with reference to the author's Automath-language: ``A constructivist uses constructions in the language, talks about them in the metalanguage, but should not extend the language by internalizing pieces of metalanguage. \dots{} Automath tried to be as weak as possible, and therefore as constructive as possible. \dots{} Nevertheless, Automath has a feature that was built in mainly for efficiency reasons, the so called type inclusion \dots{}'' To understand constructivity, proof, formalization, mathematics, language, one has to go beyond the domains of constructivity, proof, etc., but is bound to remain in language (as long as the understandings are to be communicable). Linguistic introspectivity is thus central. The author somewhat connects to such a systemic understanding of proof in discussing the recently suggested computerized proof of the four-colour theorem. In discussing mathematics and the real world, the author refers to Wigner's famous statement about the incredible and undeserved success of mathematics in explaining the real world. The author sharpens the issue: ``A pure mathematician might find it even more remarkable that it holds in spite of the fact that a large part of that successful mathematics was always immature, incomplete, unfinished and partially incorrect.'' In the reviewer's opinion, ``Wigner's surprise'' may be tempered by the insight that ``the real world'', for its very conceivability, has to be thought of as fragmentable in a deep linguistic sense -- and that the same holds for communicable mathematics (irrespective of its eventual perfection into truth). Here we must not mistake ``linguistic'' (``language'') for a classical syntax-fragment. That would be an illegitimate fragmentation, yet still frequently occurring in mathematics (intensifying ``Wigner's surprise''). In the fundamental context at hand, language is to be complementaristically conceived and a classical semiotic fragmentability rejected. For the entire collection see [Zbl 0899.00026].