In his famous article ‘What the tortoise said to Achilles’ in the journal Mind in 1895, Lewis Carroll raised the Zeno-like problem of how a proof ever gets started. Suppose I have as premises (1) p and (2) p→q. Can I infer q? Only, it seems, if I am sure of (3) (p & p→q)→q. Can I then infer q? Only, it seems, if I am sure that (4) (p & p→q & (p & p→q)→q)→q. For each new axiom (N) I need a further axiom (N+1) telling me that the set so far implies q, and the regress never stops. The usual solution is to treat a system as containing not only axioms, but also rules of inference, allowing movement from the axioms. The rule modus ponens allows us to pass from the first two premises to q. Carroll’s puzzle shows that it is essential to distinguish two theoretical categories, although there may be choice about which theses to put in which category.