Mental note from: The Princeton Companion to Mathematics

Frege formulated the idea of a formal system, in which one defines in advance all the allowable symbols, all the rules that produce well-formed formulas, all axioms (i.e., certain preselected, well-formed formulas), and all the rules of inference. In such systems any deduction can be checked syntactically —in other words, by purely symbolic means. On the basis of such systems Frege aimed to produce theories with no logical gaps in their proofs.