I am researching a system that was designed by myself and what I call PCA (Primitive Closure Arithmetic), because it looks like PRA.
The differences are: - PRA uses recursive definition with a descending parameter. While PCA uses closures. - PRA has functions that have always exactly one result. In PCA there are relations, that may have no results (for instance in case of an endless loop) or multiple. - In PRA every theory consists of the equality of two primitive recursive functions (e.g. F(x) = G(x)). In PCA it consists of an inequality of two relations (e.g. F(x,y) => G(x,y)).
The similarities are that you always compare two functions/relations and that it is logic free. No logical symbols, no quantifiers, no 'and', no 'or' etc. The boolean operators must first be defined.
PCA is more expressive than PRA. For instance, you can not express that there are infinite prime numbers in PRA, but you can in PCA. Still PCA is finitistic, because it has only potential infinite, but no actual infinite (it doesn't have a infinite set).
PCA might be interested for proving correctness of programs. Loops without a descending variable can easily be translated to a closure, but not to PRA. But of course, you need to have some sort of love for weak systems.
My question is, for my further research, does something like the system I described already exists? Before I continue with this, I want to be sure that I don't re-inventing something. In my search I already did, I couldn't find something in this direction.
Thanks in advance.
Edit, a more formal description of the language.
Value-expressions consists of 0 or variables, $x$, $x_1$, $x_2$, $y$, etc.
There are two pre-defined predicate, the equality:
$$ x = y $$
And the successor operator $y = x + 1$:
$$ s(y, x) $$
A new predicate can be defined, by the conjunction of predicates already defined. For instance, a relation that adds two can be defined as follows:
$$ AddTwo(y, x) := s(y, z), s(z, x) $$
Any variable that appears on the right side, but not on the left side, is existential automatically (in the example above the variable $z$).
You can take transitive reflexive closure of any predicate with an even number of parameters. In this way, the natural numbers can be given in a "potential infinite" way:
$$ N(x) := s^*(x, 0) $$
Closures can also be used in defining new predicates. If the predicate contains more than 2 variables, then the closure is over multiple variables at once. The even variables are connected to the odd ones. In this way the addition relation can be defined ($z = x + y$):
$$ PlusMinus(y, x, w, v) := s(y, x), s(v, w) $$ $$ Add(z, x, y) := PlusMinus^*(z, x, y, 0), N(x) $$
A theorem is a comparison of two predicates: $$ Even(x) := AddTwo^*(x, 0) $$ $$ N(x) \Leftarrow Even(x) $$ Which says that the even numbers are a subset of the natural numbers. The $\Leftarrow$ is preferred over $\Rightarrow$ because it is more convenient when making proofs.
The main axiom scheme is of replacement. The right side of a theorem can be made stronger (more restrictive).
There are more axioms, but the most interesting is the inductive scheme. The scheme is not on numbers, but on the closure:
$$ H(x, y) := F(x, z), G(z, y) $$ $$ H'(x, y) := F(x, z), G^*(z, y) $$ If: $$ F(x, y) \Leftarrow H(x, y) $$ Then: $$ F(x, y) \Leftarrow H'(x, y) $$
Where $x$, $y$ and $z$ can also be multiple variables. In plain English it says, that if applying a certain relation does not alter a property, then the property is also not altered if applied multiple times (the closure).
I hope this outlines the system in it most basic form. The complete axioms and schemes are of course more elaborate.