# How do we formalize the following:For all natural Nos :

1. Aug 16, 2011

### solakis

How do we formalize the following:

For all natural Nos : $n^2$ is even$\Rightarrow$ n is even

2. Aug 16, 2011

### Rasalhague

Re: formalization

Here's one way:

$$(\forall n \in \mathbb{N})[((\exists p \in \mathbb{N})[n^2=2p])\Rightarrow((\exists q\in \mathbb{N})[n=2q])].$$

Here's another:

$$\left \{ n \in \mathbb{N} \; | \; (\exists p \in \mathbb{N})[n^2 = 2p] \right \} \subseteq \left \{ n \in \mathbb{N} \; | \; (\exists q \in \mathbb{N})[n=2q] \right \}.$$

The symbol $\mathbb{N}$, like the name "the natural numbers", is ambiguous, so you might want to specify whether you mean the positive integers, $\mathbb{N}_1=\mathbb{Z}_+ = \left \{ 1,2,3,... \right \}$, or the non-negative integers, $\mathbb{N}_0 =\mathbb{Z}_+ \cup \left \{ 0 \right \}=0,1,2,3,...$.

3. Aug 18, 2011

### solakis

Re: formalization

Thank you ,i think the first formula is the more suitable to use in formalized mathematics.

The question now is how do we prove this formula in formalized mathematics

4. Aug 18, 2011

### Rasalhague

Re: formalization

$$1. \enspace (\exists p \in \mathbb{N}_0)[n^2 = 2p]$$

$$\Rightarrow ((\exists a \in \mathbb{N}_0)[n=2a]) \vee ((\exists b \in \mathbb{N}_0)[n=2b+1]).$$

$$2. \enspace (\exists b \in \mathbb{N}_0)[n=2b+1])$$

$$\Rightarrow (\exists q \in \mathbb{N}_0)[n^2=(2b+1)^2=4b^2+4b+1=2q+1]$$

$$\Rightarrow \neg (\exists p \in \mathbb{N}_0)[n^2 = 2p].$$

$$3. \enspace\therefore ((\exists p \in \mathbb{N}_0)[n^2 = 2p]) \Rightarrow (\exists a \in \mathbb{N}_0)[n=2a] \enspace\enspace \blacksquare$$

Or, to see the argument clearer, let $A = (\exists a \in \mathbb{N}_0)[n=2a]$ and let $B = (\exists b \in \mathbb{N}_0)[n=2b+1],$ and suppose $(\exists p \in \mathbb{N}_0)[n^2 = 2p]$. Then $A \vee B.$ But $\neg B.$ So $A.$

5. Aug 18, 2011

### solakis

Re: formalization

I think to change the variables inside the existential quantifier without dropping it first it is not allowed by logic.

Also it becomes confusing and impossible to follow.

I also wander is necessarily a formalized proof also a formal one??

Or to put in a better way is it possible to have a proof like the one above ,where one uses only formulas , without mentioning the laws of logic and the theorems upon which these laws act to give us the formalized conclusions of the above proof??

6. Aug 19, 2011

### Rasalhague

Re: formalization

Simple answer: I don't know. I'm curious. I hope someone better informed can give say more about this. Seems like it would at least be a good idea to make explicit which statements and which rules of inference are used in each line; so, we could append to the final line: / 1,2,DS. (Disjunctive syllogism.) I could be mistaken but here is what looks like an example of someone using formal and formalized as synonyms: http://arxiv.org/abs/math/0410224

A problem with my proof as it stands: a full, formal proof would have to justify the assumption that natural numbers are odd or even but not both.

I don't see what the problem is with substitution. Maybe you could elaborate?