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

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

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.