Define a logical formula as another formula I'm reading Dirk van Dalen's Logic and Structure and noticed that in many parts of his book he defines some formula to be an alias for another formula (he doesn't use the name alias, he just says that some formula will be defined as another formula).
Example Let $\phi$ be a formula of the system and $t$ a term that receives two parameters. Define $\phi$ such that $\phi(n) := t(n, x)$.
What definition in predicate logic allows one to do that? What does this 'define as' stands for? Is it the same of affirming $\phi(n) \leftrightarrow t(n, x)$? Or is it some meta-logical construct?
 A: The definition is not something that happens in predicate logic.
The formal system itself does not know anything about the letter $\phi$. Its only symbols are the primitive ones: variable letters, constant letters, function letters, predicate letters, the various logical connectives quantifiers, and whatever punctuation (such as parentheses) one needs to put them together.
When the author defines a meaning for $\phi$, that happens outside the formal system, and merely provides him with a convenient way of speaking about particular strings of primitive symbols in a succinct and systematic way. So each time a wff involving $\phi$ appears on the page, the reader is to understand that what actually is seen by the core definitions of the formal system is the string of primitive symbols that the letter $\phi$ stands for, not the letter $\phi$ itself.
This is not very different from what happens in elementary algebra. When we set forth a fact such as $a+b=b+a$, one might ask what definition in arithmetic allows one to add the letters $a$ and $b$. But there is none; the variables live outside basic arithmetic and are never really seen by the "addition" operation. However, when we substitute whatever concrete numbers the $a$ and $b$ represent, the formula is going to represent an arithmetic calculation that can actually be carried out.
