Pregeometry, Formal Language and Constructivist Foundations of Physics

TL;DR

This paper explores the foundations of physics through pregeometric structures, proposing a formal language and type theory approach to conceptualize space and geometry in a constructivist framework.

Contribution

It introduces a novel synthesis of pregeometric ideas with formal language and homotopy type theory to model space and geometry in physics.

Findings

Type-theoretic routines model physical spaces and algebras.

Formal language provides a taxonomy for different geometries.

Constructivist approach links formal computation to physical models.

Abstract

How does one formalize the structure of structures necessary for the foundations of physics? This work is an attempt at conceptualizing the metaphysics of pregeometric structures, upon which new and existing notions of quantum geometry may find a foundation. We discuss the philosophy of pregeometric structures due to Wheeler, Leibniz as well as modern manifestations in topos theory. We draw attention to evidence suggesting that the framework of formal language, in particular, homotopy type theory, provides the conceptual building blocks for a theory of pregeometry. This work is largely a synthesis of ideas that serve as a precursor for conceptualizing the notion of space in physical theories. In particular, the approach we espouse is based on a constructivist philosophy, wherein ``structureless structures'' are syntactic types realizing formal proofs and programs. Spaces and algebras relevant to physical theories are modeled as type-theoretic routines constructed from compositional rules of a formal language. This offers the remarkable possibility of taxonomizing distinct notions of geometry using a common theoretical framework. In particular, this perspective addresses the crucial issue of how spatiality may be realized in models that link formal computation to physics, such as the Wolfram model.