Abstract
We develop a model for a successor-free nondeterministic
flavour of Gödel’s T, which is built with particular consideration made to keep
it as convenient to compute as possible, while still being adequate. We desire
this convenience since we will use deterministic programs to compute the interpretation
of nondeterministic programs, and from this establish a relationship
between deterministic and nondeterminstic complexity classes.