Proving formal definitions of informal concepts

It’s been a long time since my last post. Thanks to Shin’ichi Mochizuki and Peter Woit, I found some interesting reflections. That was end of August, but now we have beginning of November. In fact, it is much worse. In September 2021, I finished the conclusion with:

Let me instead mention a logician and philosopher, who seems to consistently produce incredibly awesome overlength material: Walter Dean. I still need to read his latest paper on informal rigour. I really enjoyed his previous paper on consistency and existence in mathematics.

I still haven’t advanced beyond page 19 (4.1.3 From schematization to formalization) of the 83 page arXiv version of “On the methodology of informal rigour: set theory, semantics, and intuitionism”. While writing this, I noticed that there are also slides, which I just read completely, to ease my bad consciousness at least at bit. But now, let’s get started with the IUT saga and my reflections on definitions (of informal concepts).

My comment on Cathy O’Neil’s reflections and the IUT saga

At some point this IUT saga really made me appreciate Cathy O’Neil’s reflections on What is a proof? I know that she spotted that connection herself three month later, and discussed “politics” in both her initial reflections and its later application to IUT. The IUT saga has turned into political theatre by now, but that is not what I appreciate about her reflections. I rather like her initial motivation: “… I discussed with my students … the question of what is a proof. … smart kids … questions about whether what they’ve written down constitutes a proof. … A proof is a social construct – it is what we need it to be in order to be convinced something is true.”

Cathy defends her definition against “commenters who want there to be axioms or postulates”. Proofs going beyond axioms are rare. Gentzen’s proof of the consistency of Peano arithmetic doesn’t rely on axioms for “explaining why” epsilon_0 is well ordered. Besides justifications for the existence of certain specific ordinal or cardinal numbers, only justifications for mathematical definitions of informal concepts seem to go beyond axioms in current mathematical practice. Besides the rare examples of proof using a squeezing argument, such justifications often simply avoid claiming to be mathematical proofs. They pretent to be just definitions.

IUT seems to heavily rely on definitions. At least one commenter on Cathy’s abc post expressed hope that this might work out:

Or he’s invented a new, excruciatingly difficult language because that’s what the new result requires, in which case I don’t see why anyone else should share the credit, regardless of how long it takes number theorists to understand it. Grothendieck’s new language is an example of that: it was never “interpreted” to the world.

So initially there were hopes that IUT might teach us entirely new types of proof, but in the end it seems like we are left with Cathy’s reflections.

Let me add my own two cents to Cathy’s thoughts. She writes: “it does not constitute a proof if I’ve convinced only myself that something is true”. But any proof must also convince myself, not just some specific audience. Why? Because the skeptical audience must have a chance to challenge me on specific points or holes in my proof, but that would be impossible if I never was convinced by my proof. Cathy also writes: “It turns out that people often really want to explain their reasoning no to the typical audience, but to the expert audience.” Here IUT is very strange, because it aims neither for the expert audience, nor for the typical audience, but only to a dedicated “early career” number theorist audience. Which feels like a recipe for desaster to me.

What are the “natural” operations in a commutative ring?

I once asked Which associative and commutative operations are defined for any commutative ring? and Martin Brandenburg’s answer started with: “As argued in the comments, it is natural to require that the operation is natural 😉 in the sense that ∗ is a natural transformation, …”. Here is an excerpt from the preceeding discussion in the comments:

He: By “operation” you probably mean a operation which is defined for all rings simultanously, without any case distinction. This may be formalized using the notion of naturality in category theory: You require that for every ring homomorphism …

Me: I think I already found a counterexample to my question. Take the unary operation $u(x)$ which maps any element of the group of units to $1$ , and all other elements to $0$ . Then $u(xy)$ is an associative and commutative binary operation not covered by $x_{abc}y$ . By “operation”, I mean that only the ring structure is used, and not an order or field structure, which wouldn’t be available in a general ring. …

He: Yes, this is an example, but it is not natural (in the sense of category theory). You really have to put some compatibility condition on the operations defined for various rings, because otherwise you may for example define it as $xy$ for one “half” of the rings, and $x+y$ for other half. Or take $\min(x,y)$ for ordered rings, and $x+y$ for non-ordered rings.

It took me a bit longer to understand why my operation was not “natural” in the sense of category theory. But here, I want to ask the opposite question: Does the formal definition from category theory correctly captures the informal concept of a “natural” operation.

Formal mathematical definitions are relative to the ambient “world”

My operation was not “natural” with respect to the category of rings using normal ring homomorphisms as morphisms between objects (rings). However, if only isomorphisms are allowed as morphisms, then we get another category. It seems as if my operation would be “natural” for that category. It is probably even possible to find a less restrictive notion of morphism (i.e. those ring homomorphisms which preserve non-units) with respect to which my operation is still “natural”. (Question: I guess the forgetful functor no longer has a right adjoint in the “ring category variations” where my operation is “natural”. Is this true? Is there a simple proof? Would this justify calling those “ring category variations” unnatural or artificial?)

It looks like restricting the morphisms to isomorphisms gives some sort of maximally broad notion of “natural” operation. Are his two exampes (“you may for example define it as $xy$ for one “half” of the rings, and $x+y$ for other half. Or take $\min(x,y)$ for ordered rings, and $x+y$ for non-ordered rings.”) “natural” with respect to this maximally broad notion? The first example certainly not. Whether his second example is “natural” boils down to the question whether there can be more than one order on a given ring. Interesting question. (Answer: the quadratic number field $\mathbb Q(\sqrt{2})$ is ordered, and has the non-order preserving automorphism $\sqrt{2}\to-\sqrt{2}$ . So the second example fails to be “natural” too.) Is this really the broadest notion possible? Well, one could cheat and only allow the identities as morphisms. Of course, then any operation would be “natural”. But that is pointless, because we threw away all the available structure in that case. But to what extent are the isomorphisms immune to that objection? I guess they are fine, and actually provide another answer to my even older question Which constructions on a category are still interesting for a groupoid?

Instead of a conclusion, let’s add a further example to this section. The following request for a formal mathematical definition was my motivation to finish this post:

“Complete Knowledge” and “Certainty” mean the same thing. If you disagree, provide a consistent mathematical definition for both.

What a formal mathematical definition would do is to allow you to instantiate the defined concept in any suitable ambient mathematical “world”. Typical mathematical worlds are models of set theory, and certain categories called “topoi“. You can define stuff like relative randomness in such ambient “worlds”, for example Chaitin’s omega number is random, relative to Turing computability. But they are different from the informal concept in the real world that we care about. On the other hand, Frederik (Fra) with his computationally (and memory wise) bounded observers comes close to the point where informal physical and formal mathematical definitions start to mean the same thing again. (Stephen Wolfram and Jonathan Gorard also like to talk about such bounded observers, but when I tried to dig into details, I got the impression that they slightly overstreched that concept to arrive at their desired conclusions. But maybe that is just the way modern science works.)