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.

  • 3
    $\begingroup$ I think of geometry and topology as motivated in large part by the desire to understand shape: what shapes there are, how things can be shaped, how can shapes be arranged, and so on. "Shape" seems stand-alone to me: I don't see how it fits into a pair like "one"/"many", etc. Do you see a pair that "shape" fits into? $\endgroup$
    – user164898
    Jun 28 at 19:50
  • $\begingroup$ @A.S. I agree with you that "shape" is hardly thought in regard to any kind of opposite and that in some extent it may have motivated the study of those fields. As we're not speaking of some precise mathematical definitions, it is however harder to present this in a convincing and deep enough fashion. I reckon this could be illustrated at some specific point in the historic development of those fields. $\endgroup$
    – Johan
    Jun 28 at 21:49
  • 2
    $\begingroup$ If you prefer something precise with an actual definition, perhaps the definition of a group? The definition of a group formalizes the natural-language notion of "a type of symmetry": the two-element group formalizes (via the sets it acts on) the notion of bilateral symmetry, the dihedral groups formalize the notion of "having the symmetries of a polygon", and so on. This notion of "type of symmetry," formalized by the definition of a group, again seems stand-alone to me: I do not see how it fits into a pair like "one"/"many." $\endgroup$
    – user164898
    Jun 28 at 22:45
  • $\begingroup$ @A.S. I'm not sure what Lautman would say about groups, but I could imagine someone arguing that there is a dialectic between the concept of a group as an abstract thing in itself, versus a set of transformations. Today we distinguish a representation of a group from the group itself, but historically, the distinction was not always so crisp. $\endgroup$ Jun 29 at 12:18
  • $\begingroup$ I would say the idea of a function as a map between sets, rather than some "naturally" occurring formula. $\endgroup$ Jun 29 at 14:34

1 Answer 1


An example that is closely related to computation is proof. Mathematicians have been proving theorems ever since Euclid (and presumably even earlier). But it was not until the 20th century that the concept of a proof was formalized to the point where they could be studied as mathematical objects in their own right.

Though it does not have a well-known name like "Church–Turing Thesis," there is an analogous "formalization thesis" about proofs that I have mentioned elsewhere on MathOverflow as well as on the Foundations of Mathematics mailing list:

Given any precise mathematical statement, one can exhibit a formal sentence S in the first-order language of set theory with the property that any mathematically acceptable proof of the original mathematical statement can be mimicked to produce a formal proof of S from the axioms of ZFC.

  • $\begingroup$ That's a great example. It's really on point and captures most of the things I'm trying to show. Notably the fact that such definitions will hide some realities about those natural language concepts e.g. the fact the a proof can also be seen as a consensus. I don't know what is the modus operandi for the big-list tag but I'll accept it in a few days if nothing else comes. $\endgroup$
    – Johan
    Jul 1 at 22:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.