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.
Philosophy dictionary. Academic. 2011.