 One important reason for the successes of modern logic is its use of what has been called “formalization”. This term is usually employed to cover several distinct (though related) phenomena, all of them present in Frege (1879). One of these is the use of a completely specified set of artificial symbols to which the logician assigns unambiguous meanings, related to the meanings of corresponding natural language expressions, but much more clearly delimited and stripped from the notes that in those natural language expressions seem (to the logician) irrelevant to truth-conditional content; this is especially true of symbols meant to represent the logical expressions of natural language. Another phenomenon is the stipulation of a completely precise grammar for the formulae construed out of the artificial symbols, formulae that will be “stripped” versions of correlate sentences in natural language; this grammar amounts to an algorithm for producing formulae starting from the basic symbols. A third phenomenon is the postulation of a deductive calculus with a very clear specification of axioms and rules of inference for the artificial formulae (see the next section); such a calculus is intended to represent in some way deductive reasoning with the correlates of the formulae, but unlike ordinary deductions, derivations in the calculus contain no steps that are not definite applications of the specified rules of inference.