How to prove an element does not belong to an inductively defined set?

Question

The set $S$ is defined as the least set derived by the induction rules below:

1. $1 ∈ S$
2. if $x ∈ S$ then $2x ∈ S$
3. if $x+3 ∈ S$ then $x ∈ S$

I understand that we could prove some elements are in $S$ by giving the full derivation using rules. For example, to show that 5 is in the set $S$: $1 ∈ S \to 2 \in S \to 4 \in S \to 8 \in S \to 5 \in S$.

However, I am not sure how to formally prove that some elements are not in $S$. For example, intuitively, I know that $3 \notin S$, since we cannot derive 3 using rules above:

• To prove $... \to 3 \in S$, the previous step must be $... \to 6 \in S \to 3 \in S$ since the only rule could possibly derive $3 \in S$ is rule 3.
• Then we can apply rule 2 or rule 3. However, if we use rule 2, it would go back to the status where we need to derive $3 \in S$. Thus, we apply rule 3 again: $... \to 9 \in S \to 6 \in S \to 3 \in S$
• Following the same reason as the first step, we can only use rule 3 here: $... \to 12 \in S \to 9 \in S \to 6 \in S \to 3 \in S$
• Following the same reason as the second step, we can only use rule 3 here (we have been in the status of $6 \in S$ before): $... \to 15 \in S \to 12 \in S \to 9 \in S \to 6 \in S \to 3 \in S$
• ...

Informally, I know that these steps will never end since we are going away from the base case, and there is no chance to go back to the base case $1 \in S$.

My question is, how to formally prove $3 \notin S$ in this case?

Answer 1

Indeed, no move can ever produce a multiple of $3$. Any path to an element $s\in S$ is a successive application of rules $\#2, \#3$ and neither of those moves can change a non-multiple of $3$ into a multiple of $3$.