📝 SummarXiv

Abstract

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.