This short essay explains the difference of Symbolic Logic System, (Hilbert's) Formalism, in today's math foundation context, and the meaning of today's common math practice of using axioms in text books, its relation to logicism and formalism.

Logicism, a Symbolic Logic System as foundation of math, is today known as Mathematical Logic. It went thru several names in recent history as the subject matured: predicate logic, first order logic, symbolic logic, mathematical logic. As such, it is effectively a study of Formal Language systems. A Formal Language basically means starting with some “symbol strings” called “axioms”, and with given rules to derive more symbol strings called “theorems”.

Formalism in our context, is basically the beginning of the study on mathematical logic, in particular Hilbert's own idea of it, his perspective of mathematics as form manipulation. Today, it basically refers to the idea of inference rules, also known as production rules, string transformation, term rewrite system.

Russell's Logicism, again, is also a early conception of mathematical logic studies. In particular, Russel's logicism is he and Whitehead's work on the foundation of mathematics as a logic system. Now, in our context, we want to know what is the relation between Mathematical Logic and Formalism. Basically, today, not much. They are just 2 aspects/emphasis of the same studies. “Mathematical Logic” refers to the study of Formal Languages, while Formalism refers to the philosophy or practice of using Formal Language as a foundation or approach to doing mathematics.

Now, Axiomatic System, is pretty much the odd man out here in our context. A axiomatic system in mathematics, pretty much means a math subject done by developing from a set of axioms. It is primarily a approach to rigor in mathematics. A math done axiomatically, does not necessarily mean it is done in a mathematical logic or formalism style. Often, it is done using Set Theory as a foundation. Now, what's the relation of Set Theory to Mathematical Logic? … they are somewhat disparate subjects… usually have different contexts.

It turns out, there is a active academic community that shares the exact concerns i had. Namely, it is mostly part of the community who advocate “Calculational Proofs”. And, a notable major figure is Edsger Dijkstra (1930 – 2002). This community is also associated with the community of doing automatic theorem proving. In fact, a systematic formulation of math notations for formalism/“calculational proofs” have been presented.

References:

- 《Functional Mathematics》, by Raymond Boute, 2006. http://www.funmath.be/
- 《Funmath LRRL (Language Rationale and Reference Leaflet)》 (≈2001), by Raymond Boute — INTEC, Universiteit Gent. http://www.funmath.be/LRRL.pdf
- 《Formalized Mathematics》 , by John Harrison. http://www.rbjones.com/rbjpub/logic/jrh0100.htm

- 《How Computing Science created a new mathematical style》 (1990), by Edsger W Dijkstra. EWD1073
- 《Under the spell of Leibniz's dream》 (2000), by Edsger W Dijkstra. EWD1298