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

I'd appreciate some help for the following exercise:

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

is an axiom iff n is prime" isn't considered simple)

There is already an answered question to the problem of finding a similar deductive system in case n is not prime. Construct a deductive system where $$1^n$$ is provable iff $$n$$ is prime I am also interested in the solution to that problem, because I don't understand the notation in the answer (i.e. I don't know, what lt, ndiv, ndivsmaller etc means) and I can't simply write a comment there to clear that, because my reputation isn't high enough to do so yet.

To prove a number $$n$$ is not prime it suffices to provide a divisor greater than 1, and less than $$n$$.

Interpret $$1^n : 1^m :: 1^k$$ to mean that $$n \times m = k$$ Interpret $$1^k$$ to mean $$k$$ is composite.

Axiom $$1^n : 1 :: 1^n$$

Deduction Rules
1. $$1^n : 1^m :: 1^k \rightarrow 1^m : 1^n :: 1^k$$
2. $$1^n : 1^m :: 1^k \rightarrow 1^n : 1^{m+1} :: 1^{k+n}$$
3. $$1^{2+n} : 1^{2+m} :: 1^k \rightarrow 1^k$$ with $$n \ge 0, m \ge 0$$

Here is a proof that 4 is composite:
Axiom $$11:1::11$$ Rule 2 $$11:11::1111$$

Rule 3 $$1111$$

• Thank you! You really seem to know your stuff! – Studentu Oct 30 '18 at 0:08

Note: This system is for proving that numbers are prime, but the question was later changed to ask the opposite.

Interpret the string $$1^n | 1^m$$ to mean that $$\gcd (n, m) = 1$$
Interpret the string $$1^n || 1^m$$ to mean that $$\gcd(n, m') = 1$$ for all $$1 \le m' \le m$$
Intepret $$1^n : 1^m :: 1^k$$ to mean that there exists an integer solution in $$a,b$$ of $$a\times n + b\times m = k$$. And of course $$1^n$$ means $$n$$ is prime.

Let $$\epsilon = 1^0$$ be the empty string.

Axioms: $$1^n : 1^m :: \epsilon$$ $$1^n || \epsilon$$

Deduction rules:
1. Symmetry $$1^n : 1^m :: 1^k \rightarrow 1^m : 1^n :: 1^k$$
2. Adding to both sides $$1^n : 1^m :: 1^k \rightarrow 1^n : 1^m :: 1^{k+n}$$
3. Subtracting from both sides $$1^n : 1^m :: 1^{n+k} \rightarrow 1^n : 1^m :: 1^k$$
4. Bezout $$1^n : 1^m :: 1 \rightarrow 1^n | 1^m$$
5. $$1^n || 1^m, \,1^n | 1^{m+1}$$ $$\rightarrow$$ $$1^n || 1^{m+1}$$
6. $$1^{n+1} || 1^{n} \rightarrow 1^{n+1}$$

Here is the proof of the string $$11$$ which means "2 is prime".

First axiom $$11 : 1: \epsilon$$

Rule 2 $$11 : 1: 1$$

Rule 4 $$11 | 1$$

Second axiom $$11 || \epsilon$$

Rule 5 + Previous line $$11 || 1$$

Rule 6 $$11$$

Here is a proof of $$111$$ which means 3 is prime.

Lemma 1. $$111 | 1$$ $$111 : 1 : \epsilon$$ $$111 : 1 : 1$$ $$111 | 1$$

Lemma 2. $$111 | 11$$ $$111 : 11 : \epsilon$$ $$111 : 11 : 11$$ $$111 : 11 : 1111$$ $$111 : 11 : 1$$ $$111 | 11$$

Now apply rule 5 twice, and then rule 6 $$111 || 1$$ $$111 || 11$$ $$111$$

• Actually let me try out some proofs to see if this system is correct – Mark Oct 28 '18 at 17:51
• Okay, thank you very much. Please let me know if you find an error. \\ And sorry for the confusion about the title. I meant to open a thread for "n is not prime", but wrote in the description "n is prime". (I am interested in the solution to both problems anyways.) Should I change the title to "n is prime" now so that your answer belongs here? – Studentu Oct 28 '18 at 18:13
• I tried to answer the question as it was asked in the body. I'll just add a note at the top of my answer clarifying. – Mark Oct 28 '18 at 18:15
• I did some proofs using the system and I think it works. I'll think if I can modify it to prove non-primes – Mark Oct 28 '18 at 18:19
• Axioms 1 2 and 3 encode some basic rules of arithmetic in the natural numbers. Rule 4 is a statement of the converse of Bezout's Identity applied to gcd(n,m)=1. But in that case, it means that n and m are coprime. Rule 5 and 6 allows you to collapse a list of statements of coprimeness into a single statement, like I did for the 3 is prime proof. The reason I wanted to use Bezout's Identity is to avoid directly trying to encode the concept of non-divisibility. Does that make sense? – Mark Oct 30 '18 at 5:35