I have been asked this question several times in my logic or set theory classes.
The conclusion that I have arrived at is that you need to assume that we know how to deal
with finite strings over a finite alphabet. This is enough to code the countably many
variables we usually use in first order logic (and finitely or countably many constant,
relation, and function symbols).
So basically you have to assume that you can write down things.
You have to start somewhere, and this is, I guess, a starting point that most mathematicians
would be happy with.
Do you fear any contradictions showing up when manipulating finite strings over a finite
alphabet?
What mathematical logic does is analyzing the concept of proof using mathematical methods.
So, we have some intuitive understanding of how to do maths, and then we develop mathematical
logic and return and consider what we are actually doing when doing mathematics.
This is the hermeneutic circle that we have to go through since we cannot build something from nothing.
We strongly believe that if there were any serious problems with the foundations of mathematics (more substantial than just assuming a too strong collection of axioms), the problems would show up in the logical analysis of mathematics described above.
I tried to go through Birkhoff and Lewis many years ago but it is not easy because they use different variables and the style is so different to modern proofs.
In modern terms, the key idea is that if a graph contains a vertex $v$ of degree k, then you can get an expression of the form
$$P(G,\lambda) = (\lambda-k) P(G-v,\lambda) + \text{other terms}$$
where the other terms are all chromatic polynomials of minors of $G$.
So if the inductive hypothesis is that $P(G,x)> 0$ for all $x\geq 5$, then this reduction gives the inductive step.
Then we know that any planar graph has a vertex of degree at most 5, and that a minor of a planar graph is planar, and so we're done.
The expression involving $(\lambda-k)$ was proved by Thomassen, separately by Woodall, and more generally for all matroids by Oxley whose result preceded the others by two decades. However, although he proved the result, Oxley didn't actually state it explicitly, so missing it can be excused.
I'll dig out the BL paper tomorrow and see if their approach was essentially the same.
Added I think that the result is contained in Theorem 3.1 on page 413 in the BL paper (freely available from AMS), which bounds the coefficients of a polynomial $Q$ (the chromatic polynomial after a few trivial factors are removed). They helpfully remark that in this chapter, their usage of the symbol $\ll$ is "contrary to the notation of the preceding chapter", presumably to prevent any complacency on the part of the reader.
Best Answer
The version of the notes I have is from 2006, they are organized in the form of a short book. It is my understanding they have been updated since, and I believe the current version has new material on model theory, computability, and incompleteness. In particular, I think that Woodin's proof of the second incompleteness theorem for set theory, that I have covered elsewhere, is discussed there.
I think that the notes are distributed to the students at Berkeley that take the course, usually taught by Ted or Hugh, but I do not know whether they plan to publish them, and I am not sure they want to disseminate them otherwise.
The table of contents of the version I have is as follows:
To give an idea of the content, the languages that are discussed are finite (or recursive), and set theoretical prerequisites are kept at a minimum. This simplifies the discussion of some key results (such as compactness or the Löwenheim-Skolem theorems). Besides what I have already mentioned, topics covered include elimination of quantifiers, model completeness, Presburger arithmetic, and a study of definability for particular structures.
I would expect that contacting Ted or Hugh directly is the best way to obtain a copy of the notes.