用类型理论形式化物理概念的诞生机制。
How are Scientific Concepts Birthed? Typing Rules of Concept Formation in Theoretical Physics Reasoning
- 提出认知类型规则，将科学概念形成过程形式化。
- 在爱因斯坦相对论推导中验证了该框架的有效性。
- 为理解科学发现提供可计算的逻辑模型，适合理论物理与认知科学读者。
本文旨在形式化理论物理发现过程中科学概念形成的若干方式。尽管这看似超出精确科学范畴，但文章首先论证了科学概念形成可被形式化的合理性。随后引入类型理论作为自然且合适的框架，将概念区分、性质保持和概念变迁等“发现新概念的方式”形式化为认知类型规则。接着，将这些规则应用于物理学史上的两个案例：爱因斯坦推导出“冻结波不可能存在”的推理，以及他通向时间相对性的概念路径。在此过程中，将物理学家非正式表述的“概念发现方式”重构为由认知类型规则组合而成的类型规则，从而将其形式化为科学发现机制。最后，将爱因斯坦关于时间相对性的概念路径以类型论重构，并建模为程序合成任务，实现可计算化。
原文摘要 · Abstract (English)
This work aims to formalize some of the ways scientific concepts are formed in the process of theoretical physics discovery. Since this may at first seem like a task beyond the scope of the exact sciences (natural and formal sciences), we begin by presenting arguments for why scientific concept formation can be formalized. Then, we introduce type theory as a natural and well-suited framework for this formalization. We formalize what we call "ways of discovering new concepts" including concept distinction, property preservation, and concept change, as cognitive typing rules. Next, we apply these cognitive typing rules to two case studies of conceptual discovery in the history of physics: Einstein's reasoning leading to the impossibility of frozen waves, and his conceptual path to the relativity of time. In these historical episodes, we recast what a physicist might informally call "ways of discovering new scientific concepts" as compositional typing rules built from cognitive typing rules - thus formalizing them as scientific discovery mechanisms. Lastly, we computationally model the type-theoretic reconstruction of Einstein's conceptual path to the relativity of time as a program synthesis task.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。