Published October 29, 2025 | Version v1
Preprint Open

Absolute Constructive Limit: An Improved Upper Bound for the Proof-Theoretic Ordinal of CZF

Description

This paper introduces the Absolute Constructive Limit (ACL) – a universal measure of expressive power for formal systems, defined as the supremum of the Fast-Growing Hierarchy below the proof-theoretic ordinal. We prove ACL is finite, maximal, and base-invariant. 

Our main result establishes a new upper bound for Constructive Zermelo-Fraenkel Set Theory (CZF):
PTO(CZF) ≤ ψ₀(ε_{Ω₁ + 1}),
improving upon Rathjen's 1994 bound of ψ₀(ε_{Ω+1}). Consequently:
ACL(CZF) ≤ f_{ψ₀(ε_{Ω₁ + 1})}(3).

This work precisely delineates the boundary of constructive googology and provides the current strongest estimate of CZF's mathematical reach.

Files

Absolute_Constructive_Limit_CZF_Preprint.pdf

Files (223.0 kB)

Name Size Download all
md5:5692dac64bf790e8bde54d750d0d6005
223.0 kB Preview Download

Additional details

Dates

Accepted
2025-10-29

References

  • Rathjen, M. (1994). Proof-theoretic analysis of KPM. Archive for Mathematical Logic
  • Buchholz, W. (1986). A new system of proof-theoretic ordinal functions. Annals of Pure and Applied Logic
  • Aczel, P. (1978). The type theoretic interpretation of constructive set theory. Studies in Logic