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

Question

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.

Thank you in advance!

Answer 1

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$$

Answer 2

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$$