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?

  • $\begingroup$ By induction on $b$, perhaps? $\endgroup$ – Asaf Karagila Sep 27 '16 at 10:05
  • 2
    $\begingroup$ @AsafKaragila The reason this came up is that I am teaching an Intro to Proofs class that I am trying to make as constructive as possible. We have not hit induction yet. So, I was hoping for another way. $\endgroup$ – Joe Johnson 126 Sep 27 '16 at 10:10

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.

  • 2
    $\begingroup$ Thanks. While it is probably outside the scope to describe this to the students, I don't feel morally opposed to including the proof in my notes. $\endgroup$ – Joe Johnson 126 Sep 27 '16 at 10:35
  • 1
    $\begingroup$ The constructive proof that each number is composite or not composite, in the systems I am thinking of, is easier if we define some helper functions. Let $f(a,b,k)$ equal 1 if $bk = a$ and let it be $0$ otherwise. Decidable equality of naturals shows that this is a function. Let $g(a)$ be the sum of $f(a,b,k)$ over all $b,k$ in the interval $(1,a)$. It can be shown in these systems that $g$ is a function. Then a natural number $a$ is composite if and only if $g(a) \not = 0$. By making more complicated inductive arguments, it should be possible to eliminate the use of the functions. $\endgroup$ – Carl Mummert Sep 27 '16 at 10:44
  • 2
    $\begingroup$ I wholeheartedly with your answer. Two small additions: Firstly, one can prove "$\forall n,m \in \mathbb{N}: n = m \vee n \neq m" by induction. Secondly, a rather large and nice field which has decidable equality is the field of algebraic numbers. The extra information coming with an algebraic number, that is a polynomial with rational coefficient which has the given number as a zero, is enough to intuitionistically verify whether the number is zero or not zero. $\endgroup$ – Ingo Blechschmidt Sep 27 '16 at 12:22
  • 4
    $\begingroup$ I'm confused about your first statement: it's obviously false if you take, say $P=R\vee Q$. $\endgroup$ – cody Sep 28 '16 at 12:49
  • $\begingroup$ @cody: I see what you're saying. I will try to find a better way to phrase what I had in mind. $\endgroup$ – Carl Mummert Sep 28 '16 at 14:45

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.

  • $\begingroup$ This is also very helpful. Thanks. $\endgroup$ – Joe Johnson 126 Sep 27 '16 at 13:54

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.

  • 1
    $\begingroup$ This is also quite helpful in addition to the other responses. $\endgroup$ – Joe Johnson 126 Sep 28 '16 at 16:26

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.

  • 1
    $\begingroup$ This is also the proof I thought of first. I realized after a comment that there is an even easier one. Given the natural number $n$ from the hypothesis, it either equals the natural number $b$ or does not. If it does, then $b = n$ divides $a$. If it does not, then $n > 1$ divides $b$, so $b$ is composite. This is a constructive proof because equality for naturals is decidable. $\endgroup$ – Carl Mummert Sep 28 '16 at 16:06
  • $\begingroup$ Ah yes, that's much better! I'll put it in the answer. $\endgroup$ – Andrej Bauer Sep 28 '16 at 16:15
  • $\begingroup$ Thanks. I am learning a lot from these various answers. $\endgroup$ – Joe Johnson 126 Sep 28 '16 at 16:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.