Why $¬¬\bot \not\in PROP$?
I'm reading Dalen's Logic and Structure.
He gives the definition of the set $PROP$:
Definition $\bf2.1.2$ The set $PROP$ of propositions is the smallest set $X$ with the properties
$\begin{array}{rl} \rm(i)&p_i\in X(i\in N),\bot\in X,\\ \rm(ii)&\varphi,\psi\in X\Rightarrow(\varphi\wedge\psi),(\varphi\vee\psi),(\varphi\to\psi),(\varphi\leftrightarrow\psi)\in X,\\ \rm(iii)&\varphi\in X\Rightarrow(\neg\varphi)\in X.\\ \end{array}$
Then there are some examples:
And he says that $¬¬\bot \not\in PROP$, but I don't understand it. Isn't $¬¬ \bot=\bot$ due to the property of double negation? Considering this is true, $\bot\in PROP$. Of course, in this question, I'm pressuposing some kind of evaluation, that $¬¬ \bot$ becomes $\bot$ due to the law of the double negation, but perhaps it should be hold in an unevaluated form.
Ex:. $1+1=2$ because we presupose the $1$ merges with $1$ and then becomes two. If the merge (evaluation) does not happen, then I guess:
$$1+1=1+1$$ $$2=2$$ $$2\neq 1+1$$ $$1+1\neq 2$$
Perhaps it's something like that, I took the idea from Mathematica. Sometimes it does treats things as different in the absence of full evaluation.
Solution 1:
As the author himself alerts to: look at the brackets. What's in $PROP$ is $\left(\neg \left(\neg\bot\right)\right)$ (note the two pairs of $()$).
It isn't true that $\neg \left(\neg \bot\right)=\neg \neg \bot$ simply because they aren't the same string of characters. In mathematical logic, particularly in formal systems, one looks at propositions as actual mathematical objects, more precisely as finite strings of characters. The second character in $\neg \left(\neg \bot\right)$ is $\color{blue}($ which differs from the second character in $\neg \neg \bot$. Therefore they are different.
It is likely that eventually, after some familiarity with these concepts has been acquired,that $\neg \neg \bot$ might be defined as $\left(\neg (\neg \bot)\right)$, but for now they are different. Not only that, as the author proves, $\neg \neg\bot \not \in PROP$ according to the formation rules.
Regarding your example, if you look at $1+1$ and $2$, not as representing objects, but as objects themselves, then they are different because, well..., they are different.
Solution 2:
Regarding your example :
$1+1=2$
if you want to "test it" according to van Dalen's rules, you must first take into account that it is a formula of predicate logic and, in particular, of formal number theory.
To show that it is well-formed, you must review the formation rules of the language; see Dirk van Dalen, Logic and Structure (5th ed - 2013), page 56-57 :
Definition 3.3.1 TERM is the smallest set $X$ with the properties [...]
Definition 3.3.2 FORM is the smallest set $X$ with the properties [...]
Then, see page 82 : The language of arithmetic, and the notations introduced in page 83.
Solution 3:
I guess that you are reading the book I know from Dirk van Dalen. If that's the case, at some point the author states that:
In order to simplify our notation we will economize on brackets. We will always discard the outermost brackets and we will discard brackets in the case of negations. Furthermore we will use the convention that $\land$ and $\lor$ bind more strongly than $\rightarrow$ and $\leftrightarrow$ (cf. $\cdot$ and + in arithmetic), and that $\neg$ binds more strongly than the other connectives.
Page 12 of Dirk van Dalen's Logic and Structure - Fifth edition.
Maybe you skipped it and that's what generated the confusion.