Formalism, Formalization, Intuition and Understanding in Mathematics: From Informal Practice to Formal Systems and Back Again

本项目研究了非正式数学理论及其形式化之间的相互作用，并认为这种动态产生了三种不同形式的理解：(1)不同类型的形式化以不同的方式确定了概念之间的边界和概念依赖性，从而有助于我们对非正式数学理论内容的理解。我们认为，对非正式理论的这种形式的理解是通过将其重新塑造为正式理论来实现的，即通过改变其表达手段。（二）一旦有了形式理论，它就成为理解的对象。对这种理解的一个重要贡献是，我们认识到所讨论的理论是一种特定的非正式数学语料库的形式化。这种形式的理解将通过研究单一的预期模型和揭示不同数学领域中对象之间潜在概念共性的模型类别来澄清。（III）第三个层面涉及对同一数学领域的不同形式化的研究如何导致这些领域内容的转变，以及非正式数学本身的地理变化。在研究这些形式的数学理解时，该项目将利用数学实践历史中案例研究的哲学和逻辑分析，以构建形式化与非正式数学实践关系的令人信服的新图景。这项研究的主要结果之一将是表明，获得数学理解的过程远比当前哲学观点允许我们解释的要复杂得多。虽然形式化通常被认为对数学实践的影响可以忽略，但我们将捍卫这样一种观点，即形式化是一种认知工具，它不仅对实践中研究的问题施加了限制，而且还产生了新的推理模式，可以增强数学不同领域的标准证明方法。反思非正式数学理论与其形式化之间的相互作用意味着反思数学实践，思考是什么让数学变得严谨，以及这种活力如何产生不同形式的理解。因此，我们也旨在研究上述三个层次的理解与数学中的严谨性概念之间的联系。形式严谨性的概念（在证明理论意义上）已经在哲学和逻辑中得到了广泛的研究，尽管目前还缺乏对形式化过程的认识论作用的描述。我们认为，形式严谨性最好被理解为从非正式严格的数学论证中动态抽象出来的。这种非正式严谨的论点将通过批判性地分析来自不同数学子领域的案例研究来研究，以确定严格推理的模式。

This project investigates the interplay between informal mathematical theories and their formalization, and argues that this dynamism generates three different forms of understanding:(I) Different kinds of formalizations fix the boundaries and conceptual dependences between concepts in different ways, thus contributing to our understanding of the content of an informal mathematical theory. We argue that this form of understanding of an informal theory is achieved by recasting it as a formal theory, i.e. by transforming its expressive means.(II) Once a formal theory is available, it becomes an object of understanding. An essential contribution to this understanding is made by our recognition of the theory in question as a formalization of a particular corpus of informal mathematics. This form of understanding will be clarified by studying both singular intended models, and classes of models that reveal the underlying conceptual commonalities between objects in different areas of mathematics.(III) The third level concerns how the study of different formalizations of the same area of mathematics can lead to a transformation of the content of those areas, and a change in the geography of informal mathematics itself. In investigating these forms of mathematical understanding, the project will draw on philosophical and logical analyses of case studies from the history of mathematical practice, in order to construct a compelling new picture of the relationship of formalization to informal mathematical practice. One of the main consequences of this investigation will be to show that the process of acquiring mathematical understanding is far more complex than current philosophical views allow us to account for.While formalization is often thought to be negligible in terms of its impact on mathematical practice, we will defend the view that formalization is an epistemic tool which not only enforces limits on the problems studied in the practice, but also produces new modes of reasoning that can augment the standard methods of proof in different areas of mathematics. Reflecting on the interplay between informal mathematical theories and their formalization means reflecting on mathematical practice and on what makes it rigorous, and how this dynamism generates different forms of understanding. We therefore also aim to investigate the connection between the three levels of understanding described above, and the notion of rigor in mathematics. The notion of formal rigor (in the proof theoretic sense) has been extensively investigated in philosophy and logic, though an account of the epistemic role of the process of formalization is currently missing. We argue that formal rigor is best understood as a dynamic abstraction from informally rigorous mathematical arguments. Such informally rigorous arguments will be studied by critically analyzing case studies from different subfields of mathematics, in order to identify patterns of rigorous reasoning.