How Would an Intuitionist Prove This?

Question

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?

Answer 1

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.

Answer 2

To add a few details to Carl's answer...

Assuming your system includes full induction, your system can prove that any bounded arithmetic formula is decidable (i.e., $P \lor \lnot P$ is provable for these). The bounded arithmetic formulas are those built from atomic formulas ($s = t$ and $s \leq t$ for terms $s,t$) using logical connectives (${\land},{\lor},{\to},{\lnot}$) and bounded quantifiers $\forall x \leq t\ldots$ and $\exists x \leq t\ldots$ where $t$ is an arithmetic term in which the variable symbol $x$ does not occur. The proof that such formulas are decidable relies on the fact that, assuming $\forall x(P(x) \lor \lnot P(x))$ one can prove by induction on $y$ that $\forall x \leq y P(x)$ and $\exists x \leq y P(x)$ are decidable as well.

These formulas include many elementary arithmetic notions in (essentially) their natural forms: $$\begin{aligned} x \mid y \quad&\equiv\quad \exists z \leq y(xz = y)\\ \operatorname{Prime}(x) \quad&\equiv\quad x\geq 2 \land \forall y \leq x\forall z \leq x(yz = x \to y = x \lor z = x)\\ \operatorname{Composite}(x) \quad&\equiv\quad \exists y \leq x(y \neq 1 \land y \neq x \land y \mid x) \end{aligned}$$

Although $\lnot P \to Q$ does not entail $P \lor Q$ intuitionisitcally, the additional hypothesis that $P$ is decidable ($P \lor \lnot P$) does allow us to reach this conclusion using only intuitionistic reasoning. Assuming $P$, we immediately derive $P \lor Q$. Assuming $\lnot P$ and $\lnot P \to Q$, we conclude $Q$ and hence $P \lor Q$. Thus $$(P \lor \lnot P) \to (\lnot P \to Q) \to (P \lor Q)$$ is intuitionistically valid. Therefore, the $(\lnot P \to Q) \to (P \lor Q)$ is provable intuitionistically so long as $P$ is a bounded arithmetic statement.

Answer 3

The question was about intuitionism specifically, not some variant of constructivism, nor about some particular formalization of intuitionism (I don't think an intuitionist would recognize any particular formalization as being complete or even meaningful).

Your statement is not of the form $$P \to (Q \vee R).$$ It's of the form $$(\forall n)\Big(P(n) \to \big(Q(n) \vee R(n)\big)\Big).$$ (Quantification here is over natural numbers.)

To prove this intuitionistically, we don't necessarily need a proof of $(\forall n)(P(n) \to Q(n))$ or a proof of $(\forall n)(P(n) \to R(n)).$ What we need is a constructive way of finding, for each natural number $n,$ either a proof for that specific $n$ of $P(\underline{n}) \to Q(\underline{n})$ or a proof for that specific $n$ of $P(\underline{n}) \to R(\underline{n}),$ where $\underline{n}$ is the numeral representing $n.$

In general, to prove intuitionistically that $(\forall n)S(n),$ we need a constructive way of finding, for each natural number $n,$ a proof of $S(\underline{n})$ for that specific $n.$

In your example, it's clear that one can intuitionistically determine whether $b$ is composite or prime (simply check all possible factors between $2$ and $b-1\text{)}.$ If $b$ is composite, we immediately have a proof that "$b$ is composite or $(b \mid a)\text{."}$ If $b$ is prime, then since we are given that $n\ne 1\,\wedge\,(n\mid a)\,\wedge\,(n\mid b),$ we can conclude that $n=b,$ so $b\mid a,$ and again we have a proof of $\text{"}b$ is composite or $(b \mid a)\text{."}$

So we have an intuitionistically acceptable method, given any any $a, b, \text{ and }n$ such that $n\ne 1$ and $n$ divides both $a$ and $b$, of finding a proof that $"\!\underline{b}$ is a composite number or $\underline{b}$ divides $\underline{a}\!",$ which is exactly what is needed.

Now, there are ultrafinitists who might dispute the fact that each natural number $\gt 1$ is either prime or composite, but intuitionists would have no problem with that statement.

Answer 4

You ask how a constructive mathematician would prove the theorem. Just like you did! We only need to verify that every number is either composite or prime, see below. But Carl Mummert gave the "proof from the book", which is constructive:

Theorem: If $n \neq 1$ and $n$ divides both $a$ and $b$, then $b$ is composite or $b$ divides $a$.

Constructive proof (Carl Mummert). Either $n = b$ or $n \neq b$. If $n = b$ then $b$ divides $a$. If $n \neq b$ then $b$ has a non-trivial divisor and is composite. QED.

---

Here is your proof, worked out in a bit more detail.

Constructive proof. If $n$ is not composite then it is prime by the Lemma below. Because $n$ divides $b$ it follows that $b = n$, hence $b$ divides $a$. QED.

Lemma: A number $n > 1$ is either composite or prime.

Constructive proof. Let us be careful about the meaning of words here. By composite we mean "a product of two numbers, each of which is different from $1$". By prime we mean "a number $p > 1$ whose only divisors are $1$ and $p$". Since every number is dividisble by $1$ and itself, primality is equivalent to "a number $p > 1$ such that it has no divisor between $2$ and $p-1$."

Suppose $\phi$ is a decidable predicate on natural numbers, i.e., we have $\forall k \in \mathbb{N} \,.\, \phi(k) \lor \lnot\phi(k)$. Then also the predicates $\forall k \leq n \,.\, \phi(k)$ and $\exists k \leq n \,.\, \phi(k)$ are decidable. (Exercise, prove by induction on $n$.) Using this we can prove:

1. Given $n$ and $k$, it is decidable whether $k$ divides $n$.
2. Given $n$ it is decidable whether there is $k$ such that $2 \leq k < n$ and $k$ divides $n$.

But the second statement says that it is decidable whether $n$ is composite. To finish the proof we need to show that a number $n > 1$ which is not composite is prime. Suppose $n > 1$ is not composite. Consider any $k$ such that $2 < k < n$. Either $k$ divides $n$ or it does not. But it cannot divide $n$, or else $n$ would be composite. Therefore $n$ is prime. QED.