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.

  • 8
    $\begingroup$ I think it would help if you were to give a complete, self-contained definition of PCA. $\endgroup$ Jun 8, 2015 at 1:10
  • $\begingroup$ That would require a few pages. I am busy with making a web-based theorem checking tool and then I want to show that you can prove that there are infinite number of primes. I think the description above should be enough to ring a bell, if it already exists. A comparison with PRA is inevitable (although I didn't start with that). Basically, it is just comparing two programs, where the programs can be non-deterministic (no oracles). A non-deterministic loop in computer science, is a transitive reflexive closure in math. $\endgroup$
    – Lucas K.
    Jun 8, 2015 at 8:45
  • 5
    $\begingroup$ At the very least, you should write down what the language of your theory is, and what your induction looks like. Otherwise I would suggest to close it as "unclear what you are asking". $\endgroup$
    – Goldstern
    Jun 8, 2015 at 10:19
  • $\begingroup$ I will add the induction scheme tonight, but if above description doesn't ring a bell, then I have my answer. $\endgroup$
    – Lucas K.
    Jun 8, 2015 at 12:25
  • 1
    $\begingroup$ Lucas, is it really so hard to explain what PCA is? I have a vague idea of what your axioms might be, but it is hard to answer your question unless you tell us what your system is. One can define PRA in a short paragraph, assuming familiarity with primitive recursive functions; can you give us a similar description of PCA? $\endgroup$ Jun 8, 2015 at 12:29


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.