Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

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

  1. Aug 16, 2011 #1
    How do we formalize the following:

    For all natural Nos : [itex]n^2[/itex] is even[itex]\Rightarrow[/itex] n is even
  2. jcsd
  3. Aug 16, 2011 #2
    Re: formalization

    Here's one way:

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

    Here's another:

    [tex]\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 \}.[/tex]

    The symbol [itex]\mathbb{N}[/itex], like the name "the natural numbers", is ambiguous, so you might want to specify whether you mean the positive integers, [itex]\mathbb{N}_1=\mathbb{Z}_+ = \left \{ 1,2,3,... \right \}[/itex], or the non-negative integers, [itex]\mathbb{N}_0 =\mathbb{Z}_+ \cup \left \{ 0 \right \}=0,1,2,3,...[/itex].
  4. Aug 18, 2011 #3
    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
  5. Aug 18, 2011 #4
    Re: formalization

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

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

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

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

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

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

    Or, to see the argument clearer, let [itex]A = (\exists a \in \mathbb{N}_0)[n=2a][/itex] and let [itex]B = (\exists b \in \mathbb{N}_0)[n=2b+1],[/itex] and suppose [itex](\exists p \in \mathbb{N}_0)[n^2 = 2p][/itex]. Then [itex]A \vee B.[/itex] But [itex]\neg B.[/itex] So [itex]A.[/itex]
  6. Aug 18, 2011 #5
    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??
  7. Aug 19, 2011 #6
    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?
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook