1.4: Our Axioms

The ZFC axioms are important in studying and justifying the foundations of mathematics, but for practical purposes, they are much too primitive. Proving theorems in ZFC is a little like writing programs in byte code instead of a full-fledged programming language—by one reckoning, a formal proof in ZFC that \(2 + 2 = 4\) requires more than 20,000 steps! So instead of starting with ZFC, we’re going to take a huge set of axioms as our foundation: we’ll accept all familiar facts from high school math.

This will give us a quick launch, but you may find this imprecise specification of the axioms troubling at times. For example, in the midst of a proof, you may start to wonder, “Must I prove this little fact or can I take it as an axiom?” There really is no absolute answer, since what’s reasonable to assume and what requires proof depends on the circumstances and the audience. A good general guideline is simply to be up front about what you’re assuming.

Logical Deductions

Logical deductions, or inference rules, are used to prove new propositions using previously proved ones.

A fundamental inference rule is modus ponens. This rule says that a proof of P together with a proof that \(P \text{ IMPLIES } Q\) is a proof of \(Q\).

Inference rules are sometimes written in a funny notation. For example, modus ponens is written:

Rule.

\[\nonumber \frac{P, \quad P \text{ IMPLIES } Q}{Q}\]

When the statements above the line, called the antecedents, are proved, then we can consider the statement below the line, called the conclusion or consequent, to also be proved.

A key requirement of an inference rule is that it must be sound: an assignment of truth values to the letters, \(P, Q, \ldots\), that makes all the antecedents true must also make the consequent true. So if we start off with true axioms and apply sound inference rules, everything we prove will also be true.

There are many other natural, sound inference rules, for example:

Rule.

\[\nonumber \frac{P \text{ IMPLIES } Q, \quad Q \text{ IMPLIES } R}{P \text{ IMPLIES } R}\]

Rule.

\[\nonumber \frac{\text{NOT}(P) \text{ IMPLIES } \text{NOT}(Q)}{Q \text{ IMPLIES } P}\]

On the other hand,

Non-Rule.

\[\nonumber \frac{\text{NOT}(P) \text{ IMPLIES } \text{NOT}(Q)}{P \text{ IMPLIES } Q}\]

is not sound: if\(P\) is assigned T and \(Q\) is assigned F, then the antecedent is true and the consequent is not.

As with axioms, we will not be too formal about the set of legal inference rules. Each step in a proof should be clear and "logical"; in particular, you should state what previously proved facts are used to derive each new conclusion.

Patterns of Proof

In principle, a proof can be any sequence of logical deductions from axioms and previously proved statements that concludes with the proposition in question. This freedom in constructing a proof can seem overwhelming at first. How do you even start a proof?

Here’s the good news: many proofs follow one of a handful of standard templates. Each proof has it own details, of course, but these templates at least provide you with an outline to fill in. We’ll go through several of these standard patterns, pointing out the basic idea and common pitfalls and giving some examples. Many of these templates fit together; one may give you a top-level outline while others help you at the next level of detail. And we’ll show you other, more sophisticated proof techniques later on.

The recipes below are very specific at times, telling you exactly which words to write down on your piece of paper. You’re certainly free to say things your own way instead; we’re just giving you something you could say so that you’re never at a complete loss.