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?