An apple pie from scratch. Where do we start?

Mathematics is there to be used. It's a little like a game and a defining feature of it is that it always involves some collection of rules. There are, however, many many different ways to play that game, and so we inevitably need to specify how we're going to play. Every explanatory math text must a mix of formal and informal explanations. Since the mathematics in the following is supposed to completely self-contained and unambiguous, the question how to pass from this sort of text to precise formalizations is important to me. I've read several logic books and texts which give the impression the author thinks he provides a conceptually clear elaboration of the passage from the informal to the formal. In reality I find myself coming back to a book only a year later, when I know enough about the subject to interpret the formal introduction. It's somewhat ironic if the authors strife for clarity makes you put the book away.

todo
Ref to the logic section of Literature

The beginning must be an understanding of syntax manipulation, which is essential to doing mathematics. But specifying those basic rules (in particular in text form, as opposed an interaction with an agent like a teacher or a computer) is a mind-boggling enterprise. Here two examples of informal statements:

• “The two expressions $2\times(1+2)$ and $2+4$ are the same.”
• “If $x$ is $a^2$ and $y$ doesn't depend on $a$, then replacing $a$ in $x+y$ with $b$ gives $b^2+y$.”
• “The two expressions $(d/dx)5$ is $0$.”

Appealing to experience, it is clear what is meant by those sentences. But in reality the conceptual overhead here is gigantic. Even if we define the computation (i.e. the transition between expressions) in an informal way, the concept of certain symbols representing certain other symbols or the symbols being of different type is difficult to express concisely. There are many many obstacles here. Note for example that the symbols $($, $/$, $x$ and $5$ in '$(d/dx)5$' are all of qualitatively different content. Or note that two variables $x,y$ can be different but denote the same value. Or how bound variables, as in $\int_0^y f(x)\,\mathrm dx$, must be kept track of and possibly re-indexed when the expression “is operated upon”. And of course, counting indices presupposed some notion of natural numbers in any case. The more we want to be formal, the more complex are the vehicles we need to use. It's difficult to introduce the notion of a variable being free or independent of another without appealing to functions and naive set theory, and expressions are best expressed via syntax trees.

I don't know exactly what's path I'm going to take here, but likely I'll start much further in the middle and climb backwards to these issues. I don't really want to bother with this..

Ref.: Taylors “Practical foundations of mathematics does give an introduction over several pages about this - although I also don't find it so simple to understand”

-Idea: A good idea would be to take everything a language like Haskell provides you with. Some basic concepts could be introduced in terms of the language there.
-Let's just note here, that we like confluent systems and of course normal forms.

141208 todo: Make it clear how symbols and also indexed symbols are part of the proper meta and I just use those

Wikipedia: Abstract rewriting system

On reading