We just had the first *Categories for the Boulderite* meetup, in which a bunch of people who don’t know category theory tried to teach it to each other. Some of the people there had not had very much experience with proofs, so getting “a proof” was hard even though the concepts weren’t very deep. I got the impression that those who had trouble mainly did because they did not yet know the “follow your nose” proof tactic which I learned in my first upper division math class in college. That tactic is so often used that most proofs completely omit it (i.e. assume that the reader is doing it) and skip to when it gets interesting. Having it spelled out for me in that class was very helpful. So here I shall repeat it, mostly for my fellow Categories members.

Decide what to do based on a top-down analysis of the sentence you are trying to prove:

Shape of Sentence |
Shape of Proof |

If P, then Q. (aka. P implies Q) | Suppose P. <proof of Q> |

P if and only if Q | (→) <proof of if P implies Q>. (←) <proof of Q implies P> |

For all x such that C(x), Q | Given x. Suppose C(x). <proof of Q> |

There exists x such that Q. | Let x = <something> (requires imagination). <proof of Q> |

P or Q | Either <proof of P> or <proof of Q> (or sometimes something tricksier like assume not P, <proof of Q>) |

P and Q | (1) <proof of P>. (2) <proof of Q>. |

not P | Assume P. <find contradiction> (requires imagination) |

X = Y | Reduce X and Y by known equalities one step at a time (whichever side is easier first). Or sometimes there are definitions / lemmas that reduce equality to something else. |

Something really obvious (like X = X, or 0 ≤ n where n is a natural, etc.) |
Say “obvious” or “trivial” and you’re done. |

Something else | Find definition or lemma, substitute it in, continue. |

Along the way, you will find that you need to use the things you have supposed. So there is another table for how you can use assumptions.

Shape of assumption |
Standard usage |

If P, then Q (aka P implies Q) | Prove P. Then you get to use Q. |

P if and only if Q | P and Q are equivalent. Prove one, you get the other. |

For all x such that C(x), P(x) | Prove C(y) for some y that you have, then you get to use P(y). |

There exists x such that C(x) | Use x and the fact that C(x) somehow (helpful, right? ;-). |

P and Q | Therefore P / Therefore Q. |

P or Q | If P then <goal>. If Q then <same goal>. (Or sometimes prove not P, then you know Q) |

not P | Prove P. Then you’re done! (You have inconsistent assumptions, from which anything follows) |

X = Y | If you are stuck and have an X somewhere in your goal, try substituting Y. And vice versa. |

Something obvious from your other assumptions. | Throw it away, it doesn’t help you. |

Something else | Find definition, substitute it in, continue. |

Let’s try some examples. First some definitions/lemmas to work with:

**Definition** (extensionality): If X and Y are sets, then X = Y if and only if for all x, if and only if .

**Definition**: if and only if for every a, implies .

**Theorem**: X = Y if and only if and .

*Follow your nose proof*.

- (→) Show X = Y implies and .
- Assume X = Y. Show and .
- Substitute: Show and .
- We’re done.

- (←) Show and implies .
- Assume and . Show .
- (expand definition of = by extensionality)
- Show forall x, if and only if .
- Given x.
- (→) Show implies .
- Follows from the definition of our assumption .

- (←) Show implies .
- Follows from the definition of our assumption .

See how we are mechanically disassembling the statement we have to prove? Most proofs like this don’t take any deep insight, you just execute this algorithm. Such a process is assumed when reading and writing proofs, so in the real world you will see something more like the following proof:

*Proof.* (→) trivial. (←) By extensionality, implies since , and implies since .

We have left out saying that we are assuming things that you would naturally assume from the follow your nose proof. We have also left out the unfolding of definitions, except perhaps saying the name of the definition. But when just getting started proving things, it’s good to write out these steps in detail, because then you can see what you have to work with and where you are going. Then begin leaving out obvious steps as you become comfortable.

We have also just justified a typical way to show that two sets are equal: show that they are subsets of each other.

Let’s see one more example:

**Definition**: Given sets A and B, a function f : A → B is a __surjection__ if for every , there exists an such that f(x) = y.

**Definition**: Two functions f,g : A → B are equal if and only if for all , f(x) = g(x).

**Definition**: .

**Definition**: For any set , the __identity__ is defined by .

**Theorem**: Given f : A → B. If there exists f^{-1} : B → A such that , then f is a surjection.

*Follow your nose proof.*

- Given f : A → B.
- Suppose there exists f
^{-1}: B → A and . Show f is a surjection. - By definition, show that for all , there exists such that .
- Given . Show there exists such that .
- Now we have to find an x in A. Well, we have and a function from B to A, let’s try that:
- Let . Show .
- Substitute: Show .
- We know , so by the definition of two functions being equal, we know , and we’re done.

Again, notice how we are breaking up the task based on the structure of what we are trying to prove. The only non-mechanical things we did were to find x and apply the assumption that . In fact, usually the interesting parts of a proof are giving values to “there exists” statements and using assumptions (in particular, saying what values you use “for all” assumptions with). Since those are the interesting parts, those are the only parts that an idiomatic proof would say:

*Proof.* Given . Let . since .

Remember to take it step-by-step; at each step, write down what you learned and what you are trying to prove, and try to make a little progress. These proofs are easy if you *follow your nose*.

Thanks for the refresher

Following your nose is mostly using the subformula property to conduct a cut-free proof? https://oncourse.iu.edu/access/content/group/SP13-BL-CSCI-C241-16413/tableaux.pdf

I posted a related q/a at math.se: http://math.stackexchange.com/q/360372/11994