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?

A serious book on these subjects will certainly take care to avoid circular reasoning, since that is pretty much the point of this kind of analysis. On the other hand, an introduction aiming to explain the concepts might take a few shortcuts and end up seeming circular. This is especially so when you’re using multiple introductionary texts at the same time.

As an example, you’ve probably encountered the fact that Zorn’s Lemma is equivalent to the Axiom of Choice. That means that an exposition of the theory could start with Zorn’s Lemma and deduce the Axiom of Choice. Another exposition could well start out with the Axiom and end up with the Lemma. Both are acceptable ways of setting up the foundations of mathmatics.

Novices however, might start in the second text, see that Zorn’s Lemma is proven using the Axiom, which in the other text is proven using Zorn’s Lemma and incorrectly conclude faulty reasoning. Is this the kind of problem you’re encountering?

It appears to me, and others, that mathematics is a game with numbers that starts from a set of independent and non-contradictory assumptions. The game consists of drawing as many valid inferences as possible from the assumptions or from inferences previously drawn from the assumptions.

Basically, you’re right: you do have to be very careful to avoid circularity. The technique is to note the difference between statements in a logical theory and statements about a logical theory (and statements about statements about statements in a logical theory, and…). The simplest example I can think of is a theory of arithmetic [symbol]W[/symbol] with exactly three axioms:
[ol]li(P(x))*(P(x + 1) [symbol]®[/symbol] P(x))[symbol]~[/symbol]P(0)[/ol][/li]You can’t prove that ([symbol]"[/symbol]x)([symbol]~[/symbol]P(x)), but you can prove that there is no number n such that P(n) (roughly speaking). As long as you’re good about making distinctions like that, you should be safe.

We like to think so, but proving consistency and independence of axioms requires some creativity if it’s even possible at all. And if those proofs are in the language rather than the metalanguage, you could be in trouble.

Does the fact that Zorn’s lemma and the AoC are equivalent make the use of Zorn’s lemma in logic admissable? Is there a limit on what can be used to prove what? Could an arbitrary lemma from another branch of mathematics be used to (creatively) prove the compactness theorem, for instance?

A proof is a sequence of statements A[sub]1[/sub], A[sub]2[/sub], …, A[sub]n[/sub] such that each statement is an axiom or provable from the previous statements in the proof using whatever rules of inference are admissable. In other words, anything that’s been proved may be used to prove other statements.

If you want to use choice, you have to either take it as an axiom, or take as an axiom something that implies choice and then prove choice. Same deal with Zorn’s lemma–it’s not free unless your axioms imply it. After you’ve got either statement, you can use it as you see fit.

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.

So you could feasibly take any notion as a foundation of mathematics? Why was set theory and logic chosen, then?

This ties into another question that I had, too. For thousands of years, diagrams were considered a valid form of proof. The Greeks relied on them heavily, for instance. Some of the diagrammatic proofs that I’ve seen are a lot more “intuitive” than their more formal counterparts (i.e. n^2 = sum of odd numbers).

Diagrams seemingly fell out of favour in the nineteenth century when mathematical logic proper was born. I read elsewhere that there was a famous case of an incorrect diagram fooling everyone into believing that a theorem was provable when it wasn’t, but is this really the reason? Surely a single incorrect proof isn’t sufficient to explain why diagrammatic reasoning was shunned by mathematicians? In the areas where diagrammatic reasoning is useful, why is it inadmissable as a method of proof?

Set theory was chosen because it’s what was being studied at the time, and sets are flexible enough that you can construct anything you like with them. You can do the same with general categories.

Diagrams can be used in proofs in areas where they’re rigorously defined and one diagram can contain all the information about an object in a comprehensible fashion. The standard graph of a function like we study in calculus fails the second part–it can’t show what’s happening outside of a fixed range, and it can’t show sufficient detail to distinguish important properties.

No, not any notion. Hari Seldon was for some reason trying to avoid using the term “category theory”.

Foundations are there to provide some sort of tie between abstract mathematical concepts and physical or philosophical terms. The point of set theory as foundation is to assert certain ontological truths – we can gather things together, what sorts of things are we sure we can gather together, and so on. It lays out a precise meaning for the terms used in other branches of mathematics. If a field cannot lay out those meanings it cannot be used as a foundation.