Questions about Gödel, formal systems, propositional calculus and first order logic.

Question

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:

1. 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?

2. 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.

Answer 1

The "system" $\mathsf {TNT}$ of Typographical Number Theory is "nothing special"; we can have several different Formal systems : what counts is their "expressive capability".

Propositional calculus has a very limited expressive capability, but it is very useful for pedagogical reason, because with it it is possible to show the basic concept and properties of formal systems : syntax, semantics, consistency, completeness, etc.

First order logic is much more "useful" because with it we can formalize many (much of) mathematical thpories, like set theory and arithmetic.

First-order logic (FOL) is "made of" a language (the so called f-o language) with the quantifiers : $\forall$ and $\exists$, rules of inference : modus ponens, generalization, and (zero or more) logical axioms.

A first-order theory is "generated" from FOL adding "specific" (non-logical) axioms : see $\mathsf {PA}$ for (first-order) Peano arithmetic or $\mathsf {ZF}$ for Zermelo-Fraenkel Set Theory.

System $\mathsf {TNT}$ is a sub-system of Robinson arithmetic $\mathsf {Q}$, which is in turn a subsystem of $\mathsf {PA}$.

---

Thus, to your first question :

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?

Yes, $\mathsf {TNT}$ is a first-order theory, and thus FOL is "inside" it.

---

---

Your second question :

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?

is more thorny. True for a formula of a formal system means exactly : true in a specific interpretation.

Thus, the same formula comes out true in some interpretattion and false in another one.

Arithmetic is a very, very basic building block of our mathematical (and not only) knowledge : we have a "natural" (innate ?) understanding of what are the true "facts" about numbers, and of their properties, like $0 \ne 1, 1+1=2, \ldots$.

Thus, our expectation regarding any "reasonable" formal system for arithmetic is that it can derive (i.e. prove) all known facts of "natural" arithmetic and nothing that contradicts them.

This "natural" set of arithmetical facts is what mathematician call : "the standard model" of formal arithmetic : $\mathbb N$.