How to prove (4|n)→(2|n) in P

Question

Let 4|n means n is divisible by 4. How to prove (4|n)→(2|n) in P?

Knowing that we have ¬(4|5), so we have ¬∀n(4|n). That is, we can not suppose 4|n because otherwise we would have ∀n(4|n) by generalization, but the hypothesis is in contradiction with ¬∀n(4|n). This shows that the hypothetical proof: if B ├ C then ├ B→C of propositional logic cannot be applied to predicate logic.

We prove (4|n)→(2|n) intuitively by suppose 4|n. If we cannot suppose it, how to prove it?

Answer 1

Sketch of a proof (Natural Deduction-like).

The proof obviously needs Peano axioms; thus, what we will prove is :

$\mathsf {PA} \vdash \forall n \ [\exists k \ (n = 4 \times k) \to \exists l \ (n = 2 \times l)]$.

1. $\exists k \ (n = 4 \times k)$ --- assumed [a] (this is : $4 | n$)

2. $n = 4 \times k_1$ --- assumed [b] from 1) for $\exists$-elim

3. $\mathsf {PA} \vdash (4= 2 \times 2)$ --- from axioms for $\times$

4. $n = (2 \times 2) \times k_1$ --- from 2) and 3) by properties of equality

Now we need the associative law for $\times$, i.e. :

$\mathsf {PA} \vdash \forall a,b,c \ [(a \times b) \times c = a \times (b \times c)]$

and we have, by transitivity of equality :

5. $n=2 \times (2 \times k_1)$

6. $\exists l \ (n = 2 \times l)$ --- from 5) by $\exists$-intro (this is : $2 | n$)

7. $\exists l \ (n = 2 \times l)$ --- from 1) and 2)-6) by $\exists$-elim, discharging [b]

8. $\exists k \ (n = 4 \times k) \to \exists l \ (n = 2 \times l)$ --- from 1) and 7) by $\to$-intro, discharging [a]

9. $\mathsf {PA} \vdash \forall n \ [\exists k \ (n = 4 \times k) \to \exists l \ (n = 2 \times l)]$ --- from 8) by $\forall$-intro.

---

Note : you concern about Deduction Theorem is right for Hilbert-styple proof systems with "unrestricted" Generalization rule (see Mendelson's textbook).

The restriction on Universal generalization rule typical of Natural Deduction gives us the benefit of using $\to$-introduction rule (aka : Deduction Theorem) without restrictions also in predicate calculus.

In any case, the above proof is sound also for Mendelson's system, because the only use of Generalization in performed after the Deduction Th step to a variable $n$ that is not free in any assumption.

Answer 2

Let me assume what you want to prove is $(\forall n\in \mathbb{Z})[4|n\implies 2|n]$ (I'm not sure what your $P$ stands for, positive integers?)

Proof: For any integer $n$, if $4|n$, we can find an integer $p$ such that $4p=n$ (This follows by the Division Theorem). Then, by arithmetic we have $4p=2(2p)=n$. Since $p$ is an integer, $2p$ is also an integer. Thus, let $q=2p$, and we have found the integer $q$ that satisfies $2q=n$. By the definition of divisibility, $2|n$. That completes the proof.

Clarification: To prove the implication, we do not suppose $4|n$ for all $n$, we suppose that for each possible $n$.

Answer 3

I doubt that (4|n)→(2|n) can be proven in P. I think that it could be necessary to add a new rule of deduction for that. Let's call it the rule of conditional deduction and denote it by CDt here.

With CDt, we deduct in a restricted domain of discourse. The domain of discourse of P is natural number N. For any non empty class C⊂N, CDt works as a theory system P' that is the same as P except that its domain of discourse is C. Then, all TRUE formulas in P free of the quantifier ∃ are TRUE formula in P'. A TRUE formula in P containing ∃ cannot be translated to P'. Knowing that ¬∀x(f(x)) should be considered as ∃x(¬f(x)), and ¬∃x(f(x)) should be considered as ∀x(¬f(x)). So, we have less TRUE formulas in P' than in P at beginning of CDt. A TRUE formula in P' containing neither free variable nor quantifier ∀ is also a TRUE formula in P. A TRUE formula containing free variable x denoted by f(x) can be translated to a TRUE formula in P by (x∈C)→f(x), similarly, ∀x(f(x)) to ∀x((x∈C)→f(x)).

With CDt for proving (4|n)→(2|n), we use the C relative to the formula 4|n according to the axiom IV.1 which is similar to the axiom of comprehension. So, we have ∀n((n∈C)↔(4|n)) in P so also in P'.

We can add 4|n to P', or in other words assume 4|n in P', under CDt because the ¬(4|5) in P cannot lead to contradiction in P' for the reason that 5 is not in C. Then we can obtain 2|n by deduction in P', and translate 2|n in P' to (4|n)→(2|n) in P.

This process is the same as what we do usually by intuition. So, CDt just formalize what we do usually by introducing restricted domain of discourse. We get (4|n)→(2|n) by extension of domain of discourse, but not by reason that it's part of some TRUE formula or it's defined recursively.

In general, the restricted domain of discourse can be extended to variable domain of discourse that can further be used to extend P to a bigger domain of discourse. For example, (4|n)→(2|n) would become isN(n)→((4|n)→(2|n)) where isN(x) is TRUE if and only if x is a natural number. This would permit a unified formal theory system by mixing all theory systems in a unified domain of discourse: the universe.