I am designing a logic, that is simpler than FOL + PA. And I like to know if there already exists something in this direction.

First of all a non-deterministic Turing equivalent is defined by expression which has free variable $x_1 ... x_n$ and looks like:

$\exists u_1 ... \exists u_m \ \varphi_1 \wedge \varphi_2 \wedge ... \varphi_p$

Where any $\varphi_i$ is a comparison of two variables, a comparison with zero, the successor relation between two variables or the transitive reflexive closure of an other expression, which can operate on multiple variables in parallel.

Such expression is a simple description of a non-deterministic, Turing complete, machine. Since it does not have a negation or something with similar effect, it doesn't have an oracle.

A theorem consist of the comparison of two of those machines and has the form:

$\forall x_1 ... \forall x_n \ (\exists u_1 ... \exists u_m \ \varphi_1 \wedge \varphi_2 \wedge ... \varphi_p) \rightarrow (\exists v_1 ... \exists v_k \ \phi_1 \wedge \phi_2 \wedge ... \phi_q)$

A theorem can not be part of a larger construct and is context free (so, it can't be under assumption).

Despite the restrictive expressiveness, a set of axiom schemes and inference rules can be given, that makes reasoning over finite objects possible, with probably (I hope), the same strength of FOL + PA, for those theorems that can be expressed in both systems.

Although there is no deep theory behind this, I like this system, because of it simplicity (you can do formal math, without learning proposition logic or predicate logic), because it puts computability in the center and for it is constructivism.

My questions are:

- Does such system already exists or something very similar?
- I want to prove that it is as strong as FOL + PA. Probably I can do that with cut-elimination. For that I first have to extend this system. For the extended system I can make translations from FOL + PA to this system. But if someone directly has some remarks, let me know.