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

[solakis]

How do we formalize the following:

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

 

[Rasalhague]

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,...$.

 

[solakis]

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,...$.

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

 

[Rasalhague]

$$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.$

 

[solakis]

$$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.$

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??

 

[Rasalhague]

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?