  Thus, as part of his formal system, Frege developed a strict understanding of a ‘proof’. In essence, he defined a proof to be any finite sequence of statements such that each statement in the sequence either is an axiom or follows from previous members by a valid rule of inference. Thus, a proof of a theorem of logic, say φ, is therefore any finite sequence of statements (with φ the final statement in the sequence) such that each member of the sequence: (a) is one of the logical axioms of the formal system, or (b) follows from previous members of the sequence by a rule of inference. These are essentially the definitions that logicians still use today.