I've been reading Hofstadter's Gödel, Escher, Bach: An Eternal Golden Braid, and I'm loving it, though there are some things I don't quite understand yet.
Propositional Calculus is a formal system, and since it's embedded in Typographical Number Theory (TNT), it would appear TNT is a formal system made of other formal systems. But TNT incorporates more symbols than those of the PC, among these are found the universal quantifier $\forall$ and the existential quantifier $\exists$, and some extra inference rules.
My questions are:
Is this how first order logic is "inside" TNT? is first logic inside TNT at all, or is it some "meta-system" used to talk about TNT? Or do TNT with first order logic form together a first order theory?
The well formed formulas of a formal system are not true or false per se, but there need to be an meaningful interpretation of the symbols before the well formed formulas acquire meaning (and therefore, truth value). So, any formal system able to describe number theory can be given an intepretation, so the theorems of the system come out true when interpreted. My question is: what is the "real" number theory? how do we compare theorems of systems that represent number theory to reality, to see effectively if they are true statements about number theory?
I'm quite new to the subject, so patience is welcome.