Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Constructive Fragment of Physical Propositions

Milan Rosko

TL;DR

The work addresses how finite observational data from measurements in Minkowski spacetime constrain the space of meaningful physical statements. It introduces a proof-theoretic and realizability framework showing that extractable propositions live in the arithmetical fragment $Σ^0_1 ul Π^0_2$, with a realizability interpretation of $Δ_0$ HA on observation codes. A diagonal argument yields an operational form of incompleteness: true arithmetical statements about admissible extraction cannot be decided by any sound, recursively axiomatizable theory. The analysis ties constructive logic intrinsically to the structure of admissible evidence, highlighting that global or holographic claims are undetectable within the extractable fragment and that constructive reasoning emerges as the internal logic of operational access.

Abstract

We develop a proof-theoretic analysis of the Operational Standard of Matsas, Pleitez, Saa, Vanzella (2024) showing that admissible measurement in Minkowski Spacetime yields only finite observational sequences and thereby restricts the class of physically meaningful propositions to those admitting terminating extraction procedures or uniform stability conditions. These correspond exactly to the arithmetical fragment $Σ^0_1 \cup Π^0_2$, and the induced realizability structure interprets $Δ_0$ Heyting Arithmetic on the code of observational data. A diagonal argument then establishes an operational form of incompleteness: there exist true arithmetical propositions about admissible extraction that no sound, recursively axiomatizable theory of spacetime can decide. The result is structurally analogous to classical incompleteness but arises from the evidential limits of measurement rather than from ontological assumptions.

A Constructive Fragment of Physical Propositions

TL;DR

The work addresses how finite observational data from measurements in Minkowski spacetime constrain the space of meaningful physical statements. It introduces a proof-theoretic and realizability framework showing that extractable propositions live in the arithmetical fragment , with a realizability interpretation of HA on observation codes. A diagonal argument yields an operational form of incompleteness: true arithmetical statements about admissible extraction cannot be decided by any sound, recursively axiomatizable theory. The analysis ties constructive logic intrinsically to the structure of admissible evidence, highlighting that global or holographic claims are undetectable within the extractable fragment and that constructive reasoning emerges as the internal logic of operational access.

Abstract

We develop a proof-theoretic analysis of the Operational Standard of Matsas, Pleitez, Saa, Vanzella (2024) showing that admissible measurement in Minkowski Spacetime yields only finite observational sequences and thereby restricts the class of physically meaningful propositions to those admitting terminating extraction procedures or uniform stability conditions. These correspond exactly to the arithmetical fragment , and the induced realizability structure interprets Heyting Arithmetic on the code of observational data. A diagonal argument then establishes an operational form of incompleteness: there exist true arithmetical propositions about admissible extraction that no sound, recursively axiomatizable theory of spacetime can decide. The result is structurally analogous to classical incompleteness but arises from the evidential limits of measurement rather than from ontological assumptions.

Paper Structure

This paper contains 9 sections, 8 theorems, 9 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Extraction and Causality
  3. Predicative Extraction
  4. Computational Normal Form
  5. Logic
  6. Interpretation
  7. Limitative Result
  8. Curry--Howard--Clock Correspondence
  9. Undetectability of Holograms

Key Result

Lemma 2.6

By $\mu$-recursion, cf. odifreddi89, for every extractable $\varphi$ there exists a partial recursive function $f_\varphi$ with:

Figures (1)

  • Figure 1: The Operational Standard: Worldlines $O$ and $O'$ together with an event $Q$ determine a "Leibnizian" plane. The induced causal--temporal relations yield a structure in which the intuition of "distance" is recovered from Lorentz Covariance by logic.

Theorems & Definitions (14)

  • Definition 2.2: Causality--Distance--Machine Map
  • Definition 2.3: Extraction Procedure
  • Definition 2.4: Extractable Proposition
  • Definition 2.5: Partial Recursive Representation
  • Lemma 2.6: Turing Representation of Extraction
  • Lemma 2.7: Universal Extractor
  • Remark
  • Corollary 2.8: TM--Clock Injectivity
  • Lemma 2.10: Semi-Decidability
  • Remark
  • ...and 4 more