Divisibility
Division is a very different story than subtraction.
First of all, we do not always have
multiplicative
inverses - we certainly don't for the integers - so "division"
cannot just be syntactic sugar.
Division should work so that
$a * x = b$ and $x = b \div a$ should be equivalent.
In other words, division is defined as the solution to an equation.
Of course if $a=0$ that equation may have no solution, which is
why division by 0 is a problem. And, of course, over the
integers the equation may not have a solution even when $a\neq
0$, like $2*x = 1$.
We may tolerate the problems with divison by zero for the
rationals and reals, where dividing by anything other than zero
is possible, and allow a division operator. But we certainly
cannot do that with the integers, where for most pairs of
numbers $a,b$ the result of "$a$ divided by $b$" is not an
integer. However, while we may not have a division operator, we
have some related concepts.
Your homework gave one example, the "removing common factors"
theorem. In high school algebra, if you see the equation
$ab=ac$, you probably would just divide both sides by $a$ to get
$b=c$. If you are a bit more careful, you would realize that this
is only possible when $a\neq 0$. But in the integer case, where
we don't have a division operator, what do we do? Well the
"Removing common factors" theorem tells us that if you know
$ab=ac$, then you can deduce $a=0$ or $b=c$. So even though we
don't have division, we can still draw the same conclusion from
$ab=ac$.
What we do have with the integers is the notion
of divisibility. For example: 21 is divisible by 7.
Note that this is not an operator, because operators are
functions - they take objects as input and produce objects as
outputs. A statement about divisibility is either true or
false - "21 is divisible by 7" is true, "13 is divisible by 4"
is false. Therefore, divisibility is a predicate.
For two integers $a$ and $b$
we say $a$ divides $b$ (or $b$ is divisible by $a$)
if and only if $a \neq 0$ and $\exists x[a*x = b]$.
We will use the notation "$a|b$" to express that $a$ divides $b$.
(Sorry for using the same symbol as we sometimes to mean
"or".)
Note that "divides" is a predicate, so $a|b$ gives a
true/false value, like $a = b$ or $a \lt b$.
There are number of important theorems and definitions that
build on this basic notion of divisibility.
ACTIVITY
Prove the following theorem twice - once as a prose proof, and
then as a full first-order logic proof:
For any integers $u$, $v$ and $w$,
if $u|v$ then $u|(v*w)$.
Here is a solution to the activity.
| prose proof |
first-order logic proof |
Proof:
Assume $u|v$.
Then by definition, $u*k=v$ for some $k$.
So $u*k*w = v*w$, which we rewrite as
$u*(k*w) = v*w$, and therefore
$u|(v*w)$
qed
|
Proof:
A1: u|v [Assumption A]
A2: ∀a,b[a|b <=> a ≠ 0 ∧ ∃x[a*x=b]] [Def of divides]
A3: u|v <=> u ≠ 0 ∧ ∃x[u*x=v] [Spec of 2 a=u, b=v]
A4: u|v => u ≠ 0 ∧ ∃x[u*x=v] [Equivalence splitting on 3]
A5: u ≠ 0 ∧ ∃x[u*x=v] [Modus ponens A4, A1]
A6: ∃x[u*x=v] [And elimination A5]
A7: u*k = v [Existential instantiation on A6, x=k]
A8: (u*k)*w = v*w [reflex. and subst. of equality]
A9: u*(k*w) = v*w [Assoc. of *]
A10: ∃x[u*x = v*w] [Existential introuction, k*w goes to x]
A11: u|v*w <=> u ≠ 0 ∧ ∃x[u*x=v*w] [Spec of 2 a=u, b=v*w]
A12: u ≠ 0 ∧ ∃x[u*x=v*w] => u|v*w [Equivalence splitting]
A13: u ≠ 0 [And elimination A5]
A14: u ≠ 0 ∧ ∃x[u*x=v] [And introduction A13, A10]
A15: u|v*w [Modus ponens A12, A14]
1: u|v => u|v*w [Close assumption A]
qed
|
In this example, we really start to see how requiring a full
first-order logic proof is becoming unwieldy. In particular
to go from the second to last line of the prose proof, "$u*(k*w) = v*w$", to the
last line, "$u|(v*w)$", requires six lines of first-order
logic (lines A10-A15)!
Here's one more important consequence of our definition of divisibility.
(Divisors are smaller)
For positive integers $a$ and $b$,
$a|b$ implies $a \leq b$.
Suppose $a|b$. Then there is a number, call it $c$, such
that $a*c = b$. Since $a$ and $b$ are positive, $c$ must be
as well. So
$
\begin{array}{rcl}
1 &\leq& c\\
a*1 &\leq& a*c\\
a &\leq& b
\end{array}
$
In looking at this proof, hopefully you see that one could
expand it to full first order logic. If not, you might have a
quesion, like "how do you know $c$ is positive?"
If so, you have every right to demand that I provide more
details on that before you accept my proof!