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.

1more comment