There are some theories which, in essence, have only $\Pi^0_2$ formulas, in a way which I think captures what you're trying to capture. These theories are actually entirely quantifier free, but they allow free variables. A proof of some statement like $\phi(x,t)$ where $t$ is a term containing $x$ free is then viewed as a proof that $\forall x\exists y\phi(x,y)$. This only makes sense if you expect your witness $y$ to be given explicitly by a term, but that's often true, and will certainly be tree true if the kinds of things you're thinking about are Turing machines and discrete math.
Primitive recursive arithmetic is sometimes presented like this, and Godel's theory T (a theory of functionals) has this form as well. T is very similar to the $\lambda$-calculus, and I believe some theories of $\lambda$-calculus are also presented in the same way.
