Modified realizability subtoposes and total Weihrauch reducibility
2026-08-03 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors study how certain logical rules relate to each other by using a concept called oracle computability combined with a mathematical structure known as sheaves. They focus on total computability, which means computations that always produce an answer. By using special substructures called sheaf subtoposes linked to oracles, the authors show clear distinctions between different levels of logical principles like the weak law of excluded middle, the lessor limited principle of omniscience, and Markov's principle. Their work helps clarify how these logical rules fit into a broader hierarchy.
oracle computabilityLawvere-Tierney topologysheaftotal computabilitysheaf subtoposweak law of excluded middleLLPOMarkov's principlelogical hierarchiesreducibility
Authors
Akihito Kajikawa, Masamori Kaku, Takayuki Kihara, Satoshi Nakata
Abstract
In recent years, there has been rapid development in the foundational study of oracle computability from the perspective of Lawvere-Tierney topologies and their sheaves. In this article, we formulate and analyze the notion of reducibility within the framework of total computability. Then, using sheaf subtoposes derived from oracles in the total computable setting, we establish separations between various hierarchies of logical principles, including the hierarchies of the weak law of excluded middle $\mathbf{WLEM}$, the lessor limited principle of omniscience $\mathbf{LLPO}$, and Markov's principle $\mathbf{MP}$.