Extra-Logical Proof-Theoretic Semantics in Homotopy Type Theory
Homotopy Type theory instantiates a new form of axiomatic approach, which is more friendly to physics than the standard axiomatic approach stemming from Hilbert. This new axiomatic approach combines logical and geometrical methods in a new way and brings about a non-trivial constructive concept of identity applicable in various physical contexts including Quantum Mechanics and General Relativity.
The non-standard identity concept developed in the Homotopy Type theory allows for an alternative analysis of Frege’s famous Venus example, which explains how empirical evidences justify judgements about identities and accounts for the constructive aspect of such judgements.
Homotopy Type theory and its Model theory provide a novel formal semantic framework for representing scientic theories. This framework supports a constructive view of theories according to which a theory is essentially characterised by its methods. The constructive view of theories was earlier defended by Ernest Nagel and a number of other philosophers of the past but available logical means did not allow these people to build formal representational frameworks that implement this view.
The identity concept developed in the Homotopy Type theory (HoTT) supports an analysis of Frege's famous Venus example, which explains how empirical evidences justify judgements about identities. In the context of this analysis we consider the traditional distinction between the extension and the intension of concepts as it appears in HoTT, discuss an ontological signicance of this distinction and, nally, provide a homotopical reconstruction of a basic kinematic scheme, which is used in the Classical Mechanics, and discuss its relevance in the Quantum Mechanics.