In his work, Albert Lautman thinks the genesis of some mathematical works as a dialectic that takes place between opposite notions, like between global and local. He argues that while those notions, in the natural language, are obviously linked by their opposition, the souci or concern that stems from it can only be studied in mathematics. In other words, the study of the crux of this opposition ends up being a mathematical study. He then suggests that the friction between such pairs of opposite notions, originally in the language, is the origin of many mathematical developments.
I would like to show that there are "lone" notions, that is notions not thought as part of a pair like one/many, intrinsic/extrinsic etc., that led through their study (or can be linked, maybe notwithstanding some historical reality of the study) to interesting mathematical developments. Hence my question :
What are examples of stand-alone notions (in the language) that calls (by their importance and their wide meaning) for a formalisation which can be linked to new mathematical works ?
An example : The development of the theory of computability may be seen as an answer to the souci that comes from the informal concept of "computation". I can do a computation on a sheet of paper, Babbage's machine does computation, a sum is a computation... Then what unifies those ideas of computation ? Three attempts to capture the idea behind it have been made. Those are the theory of general recursive functions, Turing machines and the lambda calculus ; each of those embodies some aspect of the notion of computation, and it happens that those three definitions are equivalent. Hence, the Church-Turing thesis states, arguably, that those indeed capture the pre-conceptual notion of "computation".
This will be in a writing addressed to philosophers. So the simpler and the more fundamental, the better.