My question concerns the proof of the following: Let $a,b,n \in \mathbb{N}$. If $n \neq 1$ and $n$ divides both $a$ and $b$, then $b$ is a composite number or $b$ divides $a$. My proof:


Suppose $b$ is not composite. Then $b$ is prime. Since $n \neq 1$ and $n$ divides $b$, we must have $n = b$. Thus $b$ divides $a$.


This proof has the form $(P \wedge \neg R) \to Q$. If we were using normal first order logic, I could conclude $P \to (Q \vee R)$. But, using intuitionistic logic, I cannot conclude that which was to be proven. How would you carry out this proof in intuitionistic logic?



How Would an Intuitionist Prove This?
In general, when working in constructive mathematics, the strategy for proving $Q \lor R$ is to prove $Q$ or to prove $R$. In this case, just knowing abstractly that "there is an $n \not = 1$ that divides both $a$ and $b$" does not directly tell you whether $b$ is composite or whether $b$ divides $a$. So you will need more information to come up with a constructive proof. 


If you know more than the fact that there *is* such an $n$, and you actually know the value of $n$, that would help. In particular, if you could tell whether your value of $n$ is equal to $b$, then you can tell which side of the disjunction holds. So we could use the fact $(\forall k)[k = b \lor k \not = b]$ to finish the constructive proof.


Many real-world constructive systems include additional facts like that about the natural numbers, which would not be true for other objects. In particular, many constructive systems prove the sentence $(\forall n,m \in \mathbb{N})[n = m \lor n \not = m]$, which says the natural numbers have decidable equality. The motivation for accepting this in constructive systems is that, given two concrete (terms for) natural numbers, we could in principle examine them to see if they are equal. This is not the case for other objects, such as real numbers, for which equality is not decidable. The fact that equality of natural numbers is decidable is provable, in many systems of constructive math, from induction axioms that are already included. 


With a little work, these constructive systems prove that each natural number is either composite or not composite. And, with that extra fact, the remainder of the original proof goes through constructively. This may be out of the scope of an introductory proofs class, but it is one way a constructivist could prove the result. 


