[QUOTE=Dominic Mulligan]
I’ve been teaching myself some basic logic from free online textbooks and lecture notes. One thing that I’ve noticed is that lemmas and concepts from other branches of mathematics are used to prove lemmas in mathematical logic. For example, the (“a”) proof of Hintikka’s lemma requires the notion of a “Hintikka set”. Other proofs require Zorn’s lemma, for instance.
But isn’t there a degree of circularity going on here? Isn’t mathematical logic supposed to be the foundation of mathematics? How can we use Zorn’s lemma to prove theorems about the foundations of mathematics, for instance? Doesn’t Zorn’s lemma build upon these foundations itself?
[/QUOTE]
One answer is that “It’s elephants all the way down”. Logic is founded on common language (how else could it be?) and whether you take sets or some other things as the founding notion, this is undefinable. Moreover, with some feeble exceptions (quantifier-free predicate logic) it cannot be proved consistent. Certainly Goedel showed that no logic strong enough to support arithmetic cannot be proved consistent (unless, ironically, it is actually inconsistent, in which case every proposition can be proved). My favorite foundation takes function and (partial) composition thereof as the undefined notions, instead of sets and membership, but that is a matter of taste. I have no problem with the other.
Without some axiom of infinity, you cannot show that anything but finite sets exist. Finitists (and ultrafinitists who don’t even accept numbers as large as a googol) can work on finite combinatorics, including difference equations, but the mathematics they do is very limited. If your axiom of infinity is strong enough to allow ordinarily finite induction, you can do quite a lot. Essentially the constructive parts of analysis and algebra turn out to be provable. For analysis, the best exposition is still probably Errett Bishop’s book called Constructive Analysis that dates back to around 1970 (and he committed suicide shortly thereafter). I know less about constructive algebra, but there is an active group of people in the US SW, maybe Arizona or New Mexico, that studies that.
To move beyond that, what you need is something like AC (equivalently, Zorn’s lemma or Well ordering or transfinite induction). If you are going to use them, then there is no reason not to use them in logic itself. I don’t know what Hintikka’s lemma is (I am not a logician) but it sounds like another proposition equivalent to AC. Fine, if you are going to use AC, use it.
Let me mention, in reply to one of the other replies that the following infinite set of axioms is consistent and has models. Suppose P is a proposition with one free variable. Then consider:
P(0), P(1), P(2), …, P(n), …, (exists n, not P(n))
This gives rise to non-standard models of arithmetic.
Let me add that the vast majority of research mathematicians could not state, say, the Zermelo-Fraenkel axioms of set theory if their careers depended on it. The axioms of logic are interesting, but impinge on the consciousness of the average mathematician. This may surprise you, but, believe me, it is true.