A Constructive Approach Towards Formalizing Relativization Using Combinatory Logic
Marlou M. Gijzen

Abstract:
We present a formal system, ACT, that is used to express the time-complexity of computing functions. Every proof that can be made within the system relativizes. The system uses combinatory logic instead of Turing machines. We do show that it is invariant with respect to Turing machines.
We obtained that ACT is conservative over HA. We also present an extension to the system that allows for the usage of diagonalization. We then show that the P vs NP problem is independent from this system.