Using Bars to Push the Limits of Computability

This paper introduces Brouwerian Type Theory ( \(( {BTT}) \) ), an extension of Constructive Type Theory incorporating Brouwer’s notion of computability to move beyond the Church-Turing paradigm. \( {BTT} \) achieves this by internalizing the notion of choice sequences—dynamic constructs with an evolving temporal nature central to intuitionistic mathematics. To support these constructs, which evolve over time through non-lawlike decisions, in a type system, \( {BTT} \) leverages the concept of bars, inspired by Kripke-style and Beth-style possible-world semantics, which enable structured handling of the temporal progression inherent in choice sequences. This ensures structured handling of evolving states while maintaining type-theoretic properties like transitivity and symmetry, alongside possible-world properties such as monotonicity and locality. The paper examines two concrete types of bars: Beth bars, which require constructing a complete bar to validate types, and open bars, which simplify validity by requiring only local extensions. While the former captures a purely constructive interpretation, the latter is shown to be compatible with classical reasoning, highlighting how varying bar interpretations in \( {BTT} \) affect compatibility with classical reasoning. Finally, the paper demonstrates the robustness of \( {BTT} \) for internalizing choice sequences by validating their core theory.