The Literature of Symbols. Beauty and Type Theory

by Leandro Caniglia

One of the most fascinating characteristics of mathematics is its ability to express complex concepts with elegance and precision. This can produce a fascination that teaches us to see beauty where there are only symbols, drawn from an alphabet barely expanded by a few Greek letters and a handful of recurring operators. Mathematics is the fantastic literature that takes shape beneath these signs.

Type theory creates beauty by incorporating rigor through a system of stricter syntactic rules. Its goal seems to be to dispense completely with natural language, in a display of expressive purity that awakens other intellectual sensibilities. When human beings transitioned from oral storytelling to the written word, they did precisely that: they radically dispensed with all accessories, such as tone of voice, gestures, or the physical setting. The challenge was to provoke the same emotional states without resorting to suggestion, restricting themselves exclusively to the interpretation of abstract characters that, taken individually, lacked any meaning.

Just as reading moves us because we recognize it not as an innate ability but as an acquired one, type theory brings pleasure every time it manages to symbolically capture what classical mathematics delegates to informal explanation. This substitution of the oral parallels the invention of writing: it is the confirmation that our thought can be encoded well beyond the limits of complexity to which we believed ourselves confined by semiotics.