Apu Kapadia asked me some questions today about "Logic and Godel and stuff" and I sent him a long mail putting it all in a nutshell. I thought it might be useful to reproduce it here. The following is a massively condensed description of First Order Logic and its (in-)completeness theorems. I have not ventured into any philosophical speculations. A good book for that would be Douglas Hofstadter's

Godel,Escher, Bach.

Every First Order Logic theory is in a language (say L) with 3 kinds of symbols - predicates, constants and functions. So you can make a statement like P(a,b) ^ Q(f(b),c) which means "P holds of a and b, and Q holds of f(b) and c".

To give semantics to a first order formula, each of these symbols must have an interpretation. This is done by using what is called an L-structure. There are two things required for an L-structure, first a set of objects called the universe, and an interpretation for each symbol of L w.r.t this universe. So each constant refers to some element of the universe and each function symbol (predicate symbol) refers to a function (relation) on the domain of these objects. Depending on how you define your L-structure M, it can either satisfy a First order formula 'phi' written in the language L, or not. If it does, it's called a model and you write M |= phi. For eg. suppose G= (U, @) is an L-structure for the language L with just the relational symbol P, s.t. @ is commutative over U. @ is the interpretation of P in G. Therefore G |= P(x,y) = P(y,x).

Suppose you have two formulas phi and psi s.t. every model of phi is a model of psi, then you write phi |= psi .

Now we need to define provability. First we define a set of syntactic manipulations you can do to a formula to get another one. If by taking some fomulas (axioms) Sigma and doing those manipulations you get phi, then you can write Sigma |- phi. For eg. Modus Ponens: if you have Sigma |- phi => psi and Sigma |- phi, then you can say Sigma |- psi .

Godel's Completeness theorem states that, Sigma |- psi iff Sigma |= psi. So in one sense the notion of provability captures the notion of truth, but only if by truth you mean what statements your axioms can entail.

Godel's Incompleteness theorem however says this: Let L contain the symbols {0, S, +, x, <}. Consider an L-structure NN defined in this way: Take N as the set of natural numbers and define the other symbols in the obvious way (S is the successor function so S(0) is 1, S(S(0)) is 2 etc). Let Th(NN) be all the formulas written in L that are true in the model NN. Can we find an axiomatization of Th(NN), ie. a set of formulas Sigma, s.t. if NN |= phi then Sigma |- phi ? Can we do it so that Sigma is computable ie. there exists an algorithm which recognizes if some formula belongs in the set of axioms Sigma? Godel showed that this was impossible. Church showed in addition that Th(NN) is algorithmically undecidable.

So therefore, when you're interested only in the "truth" w.r.t a particular model NN, then your proof system will be incomplete.

Finally to clear up a common misconception, the

Continuum Hypothesis is not an example of such a Godel statement (true but not provable). The truth of the CH depends on the choice of the model you choose from among the models that satisfy the axioms of Set theory. In some models it is true, and in others it isn't.

In another post perhaps, I'll mention some lesser known but almost-as-wonderful results in logic such as the Compactness theorem, the existence of non-standard models of arithmetic and Tarski's "Undefinability of truth".