Revolutions and Paradigms in Logic. The Case of Proof-Theoretic Semantics

库恩关于科学革命和范式的理论，以及拉卡托斯关于科学研究计划的理论，构成了对科学历史概念发展的哲学重建的两大贡献。这两种方法在物理和化学等经验科学中都得到了卓有成效的应用；相反，它们是否也可以用来评估正式的科学却有很多争论。虽然库恩和拉卡托斯的理论对数学的适用性有些争议，但当涉及到更具体的（形式）逻辑领域时，这个问题基本上没有被探索过。在我的项目中，我的目标是解决后弗雷格和后希尔伯特逻辑的潜在Kuhnian和Lakatosian渲染的主题。虽然这个一般性的问题当然会作为我调查的起点来处理，但我还是会支持一种个案明智的策略，试图从较小但重要的样本中得出广泛的结论。特别是，我将集中在现实主义和（反现实主义）建构主义之间的逻辑对立的关键案例研究。我的关键主张如下：逻辑目前由现实主义的库恩范式主导，由模型论和集合论的结合构成。与此相反，人们可以发现一个（目前）次要但完善的建构主义拉卡托斯研究纲领，我将主要理解为普拉维茨的语义学和Martin-Löf的直觉主义类型理论的结合。现实主义范式的出现是为了回应逻辑学历史上的一个关键时刻，即语义和集合论悖论的发现，以及极限结果的证明，如Gödel的不完备性定理。这决定了放弃以前的基础态度，并采用新的核心概念来分析有效性和数学基础。然而，以前框架中的一些成分幸存下来，并合并成一系列理论，导致了今天广泛的证明理论语义领域。拟议中的研究项目，除了本身具有创新性外，似乎也有很多原因。首先，它允许从哲学历史的角度来看待哲学的经典主题之一，否则通常用形而上学的术语来解决，即现实主义者和反现实主义者之间的斗争。其次，在库恩的影响下，这个视角也可能是社会学的；更具体地说，人们可以将理论之间的竞争理解为不同“地理理论”传统之间的斗争，每种理论都有自己的位置和“拥护者”。第三（但清单可能并不详尽），这项研究可能构成一个更雄心勃勃的项目的第一步，即从根岑到现在的一般证明理论的历史，这是一个至关重要的，但到目前为止，在其他多样化的证明理论研究传统中缺失的一部分。

Kuhn’s theories on scientific revolutions and paradigms, and Lakatos’ theories on scientific research programmes constitute two major contributions to the philosophical reconstruction of the historical-conceptual development of science. Both these approaches have been fruitfully applied to empirical sciences such as physics and chemistry; it is on the contrary much debated whether they can be employed also for the assessment of formal sciences. While the applicability of Kuhn’s and Lakatos’ theories to mathematics is somewhat debated, the issue is instead mostly unexplored when referred to the more specific field of (formal) logic. In my project, I aim at addressing the topic of a potential Kuhnian and Lakatosian rendering of post-Fregean and post-Hilbertian logic. Although this general question is of course expected to be dealt with as a starting point of my investigation, I shall otherwise endorse a sort of case-wise strategy, trying to draw broad conclusions from smaller but significant samples. In particular, I shall focus on the crucial case-study of the logical opposition between realism and (anti-realist) constructivism. My pivotal claim is the following: logic is currently dominated by a realist Kuhnian paradigm, constituted by the combination of model theory and set theory. Against this, one can detect a (currently) minor but well-established constructivist Lakatosian research programme, which I shall mainly understand as given by the combination of Prawitz’s semantics and Martin-Löf’s intuitionistic type theory. The realist paradigm arose in response to a critical moment in the history of logic, i.e. the discovery of semantic and set-theoretic paradoxes and the proof of limiting results such as Gödel’s incompleteness theorems. This determined the abandonment of previous foundational attitudes, and the adoption of new core-concepts for the analysis of validity and the foundations of mathematics. However, some ingredients from the previous frameworks survived, and merged into a sequence of theories which led to today’s wide field of proof-theoretic semantics. The proposed research project, besides being innovative in itself, is also seemingly fruitful for a number of reasons. First, it permits to ground in a philosophical-historical perspective one of the classical themes of philosophy, otherwise addressed in usually metaphysical terms, i.e. the fight between realists and anti-realists. Second, via Kuhn’s influence, the perspective may be also sociological; more specifically, one may understand the competition between theories also as a fight between different “geo-theoretical” traditions, each with its places and “champions”. Third (but the list may not be exhaustive), the research may constitute the first step towards a more ambitious project, i.e. a history of general proof-theory from Gentzen to the present time, a crucial, but so far missing piece in the otherwise variegated tradition of proof-theoretic studies.