Construct a deductive system where $1^n$ is provable iff $n$ is prime

Question

I'd appreciate some help or at least a hint for the following exercise:

Construct a (as simple as possible) deductive system where all sequences of the form $1^n$ (which means 111... $n$-times) is provable if and only if n is prime. (Note: As simple as possible means that the deductive rules and axioms should follow a simple schema. For example the schema "$1^n$ is an axiom iff n is prime" isn't a considered simple)

At first I thought this can't be possible because I would have to construct an algorithm which gives me all prime numbers. But then I thought it should be possible to decide for every natural number if it is prime by test division. For deductive system I would take all sequences of the symbols $1$,$*$,$+$ and $=$ and with them I would like to somehow construct deductive rules which are the analogy to the test division and giving me the number if the test division only works for the sequence ($111...$) itself or the sequence $1$.

Answer 1

Here how I would go about this:

1. Construct a subsystem that can prove: $\operatorname{lt}(1^k, 1^n)$ iff $k < n$, and $\operatorname{add}(1^k, 1^l, 1^n)$ iff $k+l = n$. This should be straightforward.

2. Extend it to a system that can prove: $\operatorname{ndiv}(1^k, 1^n)$ iff $k$ does not divide $n$. You can do this with two rules:

$$\frac{\operatorname{lt}(y,x)}{\operatorname{ndiv}(x,y)} \text{ and } \frac{\operatorname{ndiv}(x,y),\, \operatorname{add}(x,y,z)}{\operatorname{ndiv}(x,z)}$$

Well, be careful with $0$ and all. Also, you can do it with an axiom schema instead of a rule schema and just use modus ponens as the only derivation rule...

3. And finally, extend it with $\operatorname{ndivsmaller}(1^k, 1^n)$, which should be provable iff no $l$ divides $n$ for all $2 \leq l < k$. This is a particular case of induction:

$$\frac{\emptyset}{\operatorname{ndivsmaller(11, 1x)}} \text{ and }\frac{\operatorname{ndivsmaller}(y, x), \, \operatorname{ndiv}(y,x)}{\operatorname{ndivsmaller}(1y, x)}$$

4. With this $n$ is prime iff you can derive $\operatorname{ndivsmaller}(1^n, 1^n)$, so you add this as your final rule:

$$\frac{\operatorname{ndivsmaller}(11x, 11x)}{11x}$$

(The two $1$s are there to avoid dealing with $0$ and $1$.)

Again, there are some details left to fill out and you can do it in many different ways, but I hope that the idea is clear.