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 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.

`$\Pi^0_2$`

sentence in a automated way. – Lucas K. Nov 23 '10 at 22:37`$\Pi^0_2$`

sentences are very important. Most questions in logic are`$\Pi^0_2$`

. Furthermore, I discovered when making a computer program, the puzzles to be solved are of`$\Pi^0_2$`

nature.`$\Pi^0_2$`

sentences can be expressed as the equivalence of two Turing programs with input. And, finally I read that`$\Pi^0_2$`

sentences have absoluteness, although I do not entire understand that concept. So, I was curious if one could restrict logic to these sentences. And indeed, not allowing negation in some cases. – Lucas K. Nov 23 '10 at 23:00`$\Pi^0_2$`

sentences are a very important set and covers almost all problems in discrete mathematics. You hardly need more arithmetic depth than that. Sentences with more depth might be also be constructed via a meta-level. So, one can also say that it is quite unnatural to allow arbitrary depth. – Lucas K. Nov 23 '10 at 23:20