cs.LO — Logic in Computer Science
On the scope of computability and formal axiomatic systems
This survey explores the theoretical scope of effective computation and formal axiomatic systems, emphasizing a constructive perspective based on computable trees and their associated path spaces. No new technical results are presented; rather, the aim is to synthesize established results from computability theory and mathematical logic into a unified framework that clarifies what can be computed in principle, complementing the classical emphasis on undecidability results. It is argued that standard models of computation, such as Turing machines and equivalent formalisms, are computationally saturated: any effective extension of their instruction sets does not enlarge the class of effectively computable functions and algorithms. This saturation corresponds, on the logical side, to the representational completeness of Robinson arithmetic, which is sufficient to encode all computable functions despite being finitely axiomatized. The survey proceeds by showing how standard models of computation give rise to computable trees whose infinite paths correspond to complete and consistent, but typically non-computable, extensions. This construction links effectively closed classes in Cantor space with spaces of completions of formal theories and clarifies the boundary between effective computability and logical possibility. Since Cantor space is homeomorphic to the classical Cantor set, this framework provides a natural bridge between discrete computability-theoretic and logical structures on the one hand, and continuous topology on the other.