How Does Applied Math Impact Foundations?

April 30, 2013

How Does Applied Math Impact Foundations?

Posted by John Baez

$MathML-enabled post (click for more details).$

This weekend I’m giving a talk on “The Foundations of Applied Mathematics”. It’s mostly about how the widespread use of diagrams in engineering, biology, and the like may force us to think about math in new ways, at least if we take those diagrams seriously.

I wouldn’t typically emphasize the term ‘foundations of mathematics’ when talking about this. But I’m speaking at a Category-Theoretic Foundations of Mathematics Workshop, so I want to fit in.

Unfortunately, this means I need to think a bit more generally about how applications of mathematics can impinge on foundational issues. I need to do this just so I’m not taken by surprise when people start objecting or asking tough questions.

So, I’d like to hear what you have to say. Preferably before Sunday morning!

$MathML-enabled post (click for more details).$

Here’s a bit of what I’m saying. Again, this isn’t the important part of my talk, just the introduction… but I’m afraid I’m biting off more than I can chew.

We often picture the flow of information about mathematics a bit like this:

Of course this picture is oversimplified in many ways! For example:

The details depend enormously on time and place. Let’s focus on post-WWII mathematics just to keep the topic from growing too large.

There are many branches of science and engineering, and a very complex flow of information among these.

In academia, only some applications of mathematics are now classified as “applied mathematics”.

Some branches of physics now communicate more directly to “pure mathematics” than “applied mathematics”.

Computer science also plays a distinctive role, often communicating directly to “foundations of mathematics”.

But the picture is close enough to true that deviations are interesting.

In particular: can developments in applied mathematics force changes in the foundations of mathematics?

Applied mathematics often provokes new developments in pure mathematics. But can it demand new foundations?

Can applications of math directly affect the foundations of math, or is the conversation always mediated by pure mathematicians?

Computer science is the biggest example of “applied math” that grew directly out of work in logic, where new ideas directly impact foundations:

Uncomputability, undecidability,…

Computer-aided proofs: what is a proof?

Category-theoretic logic

etcetera

But I want to talk about some other applications of mathematics that seem to call for category-theoretic foundations….

Posted at April 30, 2013 8:21 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2616

43 Comments & 1 Trackback

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Are we allowed topics close to home, like how some of the inspiration for modalities in homotopy type theory comes from the axiomatisation of cohesion?

Posted by: David Corfield on April 30, 2013 9:12 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

You’re certainly allowed to talk about this (or anything)! I guess Lawvere’s original interest in ‘cohesion’ arose from applications of mathematics to classical mechanics… and of course Urs is interested in its applications to quantum field theory.

Posted by: John Baez on April 30, 2013 11:09 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Vladimir Voevodsky argued that:

applied mathematics is complex, but not very abstract.
elegant mathematics is highly abstract, but of low complexity.
For real applications, we need highly abstract, highly complex mathematics. For this we need a new (univalent) foundations.

I hope the quote is precise. It is from this video.

Posted by: Bas Spitters on April 30, 2013 9:30 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Thanks, that’s interesting!

Posted by: John Baez on May 1, 2013 3:39 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

I’m surprised that I haven’t seen any influence of quantum-mechanics or quantum-computing on foundations. Then again I’m having problems envisioning a foundation where the terms are fundamentally uncertain.

Posted by: RodMcGuire on April 30, 2013 9:53 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

I think the diagrammatic approach to logic and proof theory has recently been strongly influenced by quantum computation; see Physics, topology, logic and computation: a Rosetta stone for one survey of this. But many people working on foundations won’t consider this ‘foundational’, and they may not do so until something like a ‘quantum topos’ is defined, which is rich enough to do something a bit like set theory, but includes something more quantum-mechanical, maybe something like the category of C*-algebras, as a special case. There have been attempts to define a ‘quantum topos’, but so far none seem very convincing.

(The topos-theoretic approach to quantum theory goes in a somewhat different direction, since it makes quantum theory seem classical internal to a topos, rather than trying to generalize topos theory to include quantum features. But maybe you could count this as a different way quantum theory is beginning to impinge on ‘foundations’.)

Posted by: John Baez on May 1, 2013 6:54 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

This is an answer to the question in your title (“How does applied math impact foundations?”) rather than the last sentence of your post (asking for applications that call for category-theoretic foundations). I’m thinking of the conjunction between statistics and logic, as expounded in, for example, Jaynes’s book Probability Theory: The Logic of Science. I bet you’re familiar with this book, and David C must be too. Jaynes argues that to do inference right in the real world, one has to get straight the foundations of probability theory, and for him that means Bayesianism.

He’s not the only one to see logic and statistics as closely related. For instance, the University of Barcelona has a Department of Probability, Logic and Statistics.

Posted by: Tom Leinster on May 1, 2013 12:41 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Yes, a great book. But I wonder if John will count changes to the foundations of a particular branch of maths, i.e., to its basic ideas, rather than to the foundational language of maths itself.

On the other hand, if Mumford is right in The Dawning of the Age of Stochasticity, the radical step of introducing random variables into the foundations is needed.

As far as I know, however, nothing came of Mumford’s plan. It’s extremely difficult for me to imagine a change to foundations which is not mediated by logicians, computer scientists or pure mathematicians. I could imagine homotopy type theory taking over, but any such change will have been mediated by all three groups.

Posted by: David Corfield on May 1, 2013 9:14 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

David wrote:

On the other hand, if Mumford is right in The Dawning of the Age of Stochasticity, the radical step of introducing random variables into the foundations is needed.

As far as I know, however, nothing came of Mumford’s plan.

Recently Paul Christiano, Eliezer Yudkowsky, Marcello Herreshoff and Mihaly Barasz introduced the concept of a ‘stochastic model’ of a set of axioms—they actually called it a ‘coherent probabilistic valuation’, but I think my name captures the idea just fine: it’s just a probability measure on the set of models. More importantly, they used this idea to find a kind of workaround to Tarski’s theorem on the undefinability of truth!

I wrote an article about this called Probability theory and the definability of truth. I was asked if I’d like to visit the Machine Intelligence Research Institute (formerly the Singularity Institute) to discuss this further, and it looks like I’ll do that in December. I feel there’s more that can be done with this idea.

It’s extremely difficult for me to imagine a change to foundations which is not mediated by logicians, computer scientists or pure mathematicians.

Yes, I was wondering if logicians could talk directly to people in applied mathematics, unmediated by pure mathematicians. My main (and only?) example of this is the conversation between logicians and computer scientists… which seems to have arisen because computer science grew out of logic. So that might be the avenue to bring probability theory into logic — and my little story above seems to confirm that.

Posted by: John Baez on May 1, 2013 3:24 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

The (alleged) non-rigorous use of infinitesimals by engineers etc. seems to have been an inspiration for the development of synthetic differential geometry, and thereby a whole lot of topos theory.

One modus operandi that I like is to observe that a group of people (e.g. engineers) are doing things “wrong” (e.g. by invoking apparently mythical numbers which are nonzero but whose square is zero) and yet end up getting right answers. A dismissive person will think of them as heathens. A more curious person will try to uncover the real foundations of the method.

Other examples: Euler’s formal proofs (e.g. that $1 + 2 + \cdots = -1/12$ ), seven trees in one, path integrals, and the way that mathematicians can manipulate sets accurately without knowing ZFC.

Posted by: Tom Leinster on May 1, 2013 1:22 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Tom wrote:

The (alleged) non-rigorous use of infinitesimals by engineers etc. seems to have been an inspiration for the development of synthetic differential geometry, and thereby a whole lot of topos theory.

That’s a good example! (David may have been alluding to it earlier in his remarks about ‘cohesion’, but I’d forgotten the role of engineers.)

A related example is how the electrical engineers Heaviside and Dirac used generalized functions that weren’t functions. This affected pure math but didn’t (mainly) hit ‘foundations’, since it was dealt with by Laurent Schwarz and others using new ideas in functional analysis.

One can imagine an alternative history in which these generalized functions pushed nonstandard analysis or synthetic differential geometry into prominence.

(I know that Dirac had a career in physics after he stopped being an electrical engineer, but I can’t help but wonder if having been an engineer gave him some sort of edge when it came to mathematical audacity.)

Posted by: John Baez on May 1, 2013 3:31 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

David may have been alluding to it earlier…

I was alluding first to the inspiration that Lawvere found in physics, which led to several category theoretic constructions, such as cohesion. But then if someone didn’t want to count this as foundational, I was also alluding to the way cohesion is proving to be a key example in working out how to add modalities to homotopy type theory.

Posted by: David Corfield on May 2, 2013 8:42 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Would another example be the discovery/invention of complex numbers, which originally would have also seemed like “mythical numbers”, and which today are also used by electrical engineers?

Another example would be when Newton invented calculus.

Posted by: Jeffery Winkler on May 7, 2013 10:48 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

You can see the slides of my talk here.

There’s a somewhat cryptic reference to categorifying the category of vector spaces over $\mathbb{C}(z)$ , which I will explain using the blackboard in my actual talk if I have time! This is a project I’m working on now.

Posted by: John Baez on May 1, 2013 10:02 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Nice!

Slide 32 might make you think that quasi-toposes and Univalent Foundations involve string diagrams, but they’re not so obvious there. Is the trouble with morphisms going right up to $\infty$ ?

Posted by: David Corfield on May 2, 2013 9:14 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Yes, that’s the trouble. I wasn’t meaning to suggest that any of this line of foundational work has much to do with string diagrams. Indeed my subtext is that while others are shooting off into the stratosphere, I prefer to explore the humble weedy fields of applied math looking for interesting ideas that haven’t received the recognition they deserve from ‘pure’ mathematicians.

However, the whole distinction between ‘foundations’, ‘pure math’ and ‘applied math’ is something I try not to concern myself with. It somehow worked its way into my talk as I tried to justify why I’m discussing control theory and stochastic Petri nets at a workshop on ‘category-theoretic foundations of mathematics’. Perhaps if I were braver I would have just said “Here’s what I’m interested in these days… it may not count as ‘foundational’, but I think this workshop needs someone to stir up a bit of trouble. If we focus too much on ‘foundations’ and ignore the big messy world out there, our souls will dry up.”

Posted by: John Baez on May 2, 2013 9:48 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Simple. If anyone complains just quote Lawvere

In my own education I was fortunate to have two teachers who used the term “foundations” in a common-sense way (rather than in the speculative way of the Bolzano-Frege-Peano-Russell tradition). This way is exemplified by their work in Foundations of Algebraic Topology, published in 1952 by Eilenberg (with Steenrod), and The Mechanical Foundations of Elasticity and Fluid Mechanics, published in the same year by Truesdell. The orientation of these works seemed to be “concentrate the essence of practice and in turn use the result to guide practice”. (Lawvere 2003: 213)

‘Foundations and applications: axiomatization and education’, Bulletin of Symbolic Logic 9 (2003), 213-224.

Posted by: David Corfield on May 2, 2013 10:45 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

On the last slide, I’m not sure I would agree with the implication that it’s only applied mathematicians who find the logicians’ reduction of diagrams to 1-dimensional strings of symbols too clumsy. I think plenty of pure mathematicians use “syntax” that more directly models the things they are studying as well. Category theorists use string diagrams and pasting diagrams without bothering to reduce them to linear equations, and low-dimensional (and even high-dimensional) geometers draw pictures of manifolds and cobordisms without feeling the need to write out formulas.

Posted by: Mike Shulman on May 2, 2013 9:03 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Yes, you’re right. What intrigues me is that when pure mathematicians are pressed to be rigorous, they usually tell some story where their use of diagrams is ‘justified’ by some setup involving linear strings of symbols. But it seems some engineers and the like don’t even try… probably because they haven’t had a certain kind of ‘rigor’ imposed on them in school. And perhaps as a result, they’ve made up some kinds of math that haven’t even been brought under the umbrella of pure math.

The case of control theory is a good one. If you try to formalize how control theorists use ‘signal flow diagrams’ in a hasty way, you may conclude they’re a notation for linear maps between finite-dimensional vector spaces over $\mathbb{C}(z)$ . That’s what everyone says. And that’s not completely wrong, but it misses the point that there’s more information in the diagrams than in these linear maps — and that’s why the diagrams are so useful!

There’s at least a bicategory going on here: a categorification of the category of finite-dimensional vector spaces over $\mathbb{C}(z)$ . But if you asked a control theorist about this, of course they wouldn’t say this. They just know how to do stuff with these diagrams.

There are probably also cases in pure math where people use diagrams in ways that are more powerful than those people have managed (or bothered) to formalize. Anyone know any?

Posted by: John Baez on May 2, 2013 10:20 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

use of diagrams is ‘justified’ by some setup involving linear strings of symbols.

I’m surprised that Logic Programming hasn’t had some influence on foundations. There a basic term is a structure (diagram) in which substructures can be shared (and when “occur check” is absent can contain cycles). Structure sharing takes the place of the need for distinguished variables in a linear string of symbols and as a bonus such “variables” can be partially bound within a continuum from completely unbound to fully bound to “over bound” (a contradiction).

Posted by: RodMcGuire on May 2, 2013 11:57 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Logic programming has impacted foundational work, just not quite in the way your are suggesting in your comment. Operationally, there are two sides to logic programming: on the one hand, unification is used to do equality reasoning, and on the other, proof search is used to do propositional reasoning.

Proof-theoretic analyses of proof search have led to the concept of focalization and polarization in type theory, and that is a major strand of Jean-Yves Girard’s foundational program of Ludics. (A good introduction to this, with a focus on the foundational consequences, is Lecomte et al’s Ludics and Anti-realism. Girard’s original paper, Locus Solum: from the rules of logic to the logic of rules is good but very eccentric.)

The unification algorithm, on the other hand, has not had such an impact on foundations yet. Its proof-theoretic significance is IMO best-understood in terms of the Girard/Schroeder-Heister rules for introducing and eliminating equality. See Rules of Definitional Reflection, with the rules for equality given below:

$\begin{array}{ll} \frac{}{\Gamma \vdash t = t} \qquad & \frac{\forall \theta\in\mathrm{csu}(s,t).\; \theta(\Gamma) \vdash \theta(C)} {\Gamma, s=t \vdash C} \end{array}$

Here $\mathrm{csu}(s,t)$ is read as “a complete set of unifiers for $s$ and $t$ ”. So you use a hypothetical equality by showing the conclusion under all the possible ways that the two terms could be equal. The main reason that this approach has not had much uptake is that the unification problem for most nontrivial theories is undecidable.

However, this rule is still of practical interest, because it corresponds to the style of dependent programming common in Agda, which uses the equations embedded into dependently-typed terms to rule out impossible branches of case distinctions. It also corresponds to natural styles of informal paper proofs. In contrast, in standard Martin-Loef type theory, proving a contradiction from an impossible equality is a somewhat roundabout process involving a large elimination. So getting a better understanding the relationship between the Girard/Schroeder-Heister equality and the ML identity type seems like a worthwhile problem, which could have some foundational significance.

The use of unification in the equality elimination also (and this is vague, I admit) reminds me a bit of the split/funsplit formulations of the elimination forms for $\Pi$ and $\Sigma$ types.

Posted by: Neel Krishnaswami on May 8, 2013 11:23 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

in standard Martin-Loef type theory, proving a contradiction from an impossible equality is a somewhat roundabout process involving a large elimination.

I used to also think this process was roundabout, but now I see it as just a special case of a general method for calculating path spaces in (higher) inductive types. Over the past few months, Dan Licata, Guillaume Brunerie, Peter Lumsdaine, myself and others have used essentially the same method (or generalizations thereof) to prove lots of homotopy-theoretic results such as $\pi_n(S^n)=\mathbb{Z}$ , the Freudenthal suspension theorem, and the van Kampen theorem. Dan Licata was the one who originally isolated this method, which he calls “encode-decode”.

In all cases, the large elimination is necessary to ensure that the category of types has sufficient higher structure. You can’t have $\pi_1(S^1)=\mathbb{Z}$ if all types are sets, for instance, so you need a univalent universe to ensure the presence of higher homotopy. The case of (for instance) disjointness of injections into a coproduct is just the case $n=0$ of this, where you need to ensure that the category of types is not a poset (otherwise the injections would not be disjoint), and for that a not-necessarily-univalent universe suffices.

There’s a discussion of the encode-decode method for the case $\pi_1(S^1)=\mathbb{Z}$ , and how it generalizes the classical proofs of injectivity and disjointness of constructors, in this paper.

Posted by: Mike Shulman on May 8, 2013 5:52 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Wow, Mike, that’s a really cool paper! I’m reading now, and enjoying–I might have some questions later.

I see that it extends nicely to bouquets of circles. What sorts of topological results are you hoping to try next? Some knot groups might be nice, and fixed point theorems, and a new proof of Poincare would be handy…

Posted by: stefan on May 8, 2013 7:14 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Thanks. I should say that Dan wrote most of the text of that paper, and all of the Agda.

What do you think the best homotopical characterization of knot groups would be? It’s tricky to say things that classically involve topological spaces arising from concrete constructions. Is the complement of a trefoil a higher inductive type? Fixed point theorems also involve an interaction between concrete topology and homotopy theory, and hence are tricky.

I’ve given a bit of thought to duality, but no real results yet. One thing that I think is close on the horizon is the Eilenberg-Steenrod axioms for homology and cohomology, which would then suffice for a whole lot of calculations. I’m also waiting for our first spectral sequence.

Posted by: Mike Shulman on May 9, 2013 6:32 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

If you build a connective spectrum, then you can have a Leray-Serre spectral sequence.

Posted by: Jesse McKeown on May 9, 2013 7:52 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Well, if you can write terms that mean $K(G,n)$ , then you can also write terms that mean $\mathbf{B}^n(Map(X,K(G,m))$ : the $(n+1)$ -connected cover of $Map(X,K(G,m+n))$ ; and if $X$ is a fiber $X_b$ of $E\to B$ , then sections of $\mathbf{B}^n(\operatorname{Map}(X,K(G,m))$ over $B$ arrange themselves into sequences (not fiber or exact, just sequences)

(1)

\forall b, \mathbf{B}^n Map(X_b, G) \to \forall b, \mathbf{B}^{n-1} Map (X_b, K(G,1)) \to \cdots \to \forall b, Map(X_b,K(G,n))

the $l+1$ -page of the spectral sequence is given by (components of the fiber of) the composites of length $l$ , modulo details of what $\forall b, \mathbf{B}^n Map(X_b, G)$ really is. And the reason we get to call this “Leray-Serre” is that the fiber of one of these maps has component group $H^k(B, H^m (X_b))$ with $k+m=n$ .

I must hastily admit I don’t know if the terms will be computationally useful — can one extract generators-and-relations from them? — but that’s never been how I thought of using HoTT anyway.

Posted by: Jesse McKeown on May 10, 2013 9:44 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Okay, that sounds vaguely like an approach Eric Finster and I were considering, although I don’t understand all your notation — I’m used to B meaning delooping, is that what it is for you? What do you mean by ‘components of the fiber’ and ‘composites of length l’?

But the big question that we never got to is, how do you know that it converges to anything?

Posted by: Mike Shulman on May 11, 2013 5:58 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Oh, it converges-to-something (for connective spectra, such as are Eilenberg-MacLane) because everything is finite; the sequence I called $(1)$ is all of $n$ -truncated spaces. Yes, $\mathbf{B}$ means delooping; unbolded $B$ is just a space, the base of the fibration. I’m using $\forall b$ instead of $\prod_{b:B}$ , I can’t remember why…

“[A] composite of length $l$ ” means the map $\forall b, \mathbf{B}^{k+l}(X_b,K(G,r)) \to \forall b, \mathbf{B}^k (X_b,K(G,r+l))$ , which fits in $(1)$ when $n=k+l+r$ .

Does that clarify something of it? I must say I’m glad it looks familiar-enough, because I’d hate for all that typesetting to be completely wrong…

Posted by: Jesse McKeown on May 17, 2013 1:36 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

I’m looking for a proof, in homotopy type theory, that it converges to the thing we hope. If you’re trying to give me one, then you’re a lot quicker than I am.

Posted by: Mike Shulman on May 17, 2013 5:44 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Alas, not yet; I had decided that the right way to talk about this filtration-like-thing was via the big diagram of pullbacks collecting the fibers of each composite map, and the pasting lemmata, but that’s something I haven’t found a way to serialize neatly.

Posted by: Jesse McKeown on May 17, 2013 3:21 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

What do you mean by “you can have”? We certainly have some connective spectra, e.g. Dan and Guillaume (I think) have constructed Eilenberg-Mac Lane spectra of abelian groups. Can you construct the LSSS from that, inside of type theory?

Posted by: Mike Shulman on May 9, 2013 9:19 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

I vaguely recall that knot complements are $K(\pi,1)$ ’s, in which case describing their homotopy type can be done by specifying a group. That sounds kinda boring. But maybe here’s a way homotopy type theory might help.

As you probably know, different ways of drawing a knot give different presentations of the knot group: the Wirtinger presentations, with one generator for each strand and one relation for each crossing. For example, the usual drawing of the trefoil gives a group with three generators, such that conjugating each generator by the previous one gives the next one:

A given knot has lots of different drawings, but you can get from one to the other by moves called Reidemeister moves. These change one Wirtinger presentation to another in a very nice way:

So, there’s an issue here ‘things being different yet homotopic’ — namely, we’ve got a groupoid of different presentations of the same group, where the morphisms are Reidemeister moves. Perhaps homotopy type theory could be used to clarify this issue, or at least explore it in a somewhat new way.

Posted by: John Baez on May 9, 2013 6:24 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Interesting idea! Is there any way in which knot drawings can be defined inductively? If so, then we could perhaps consider the Reidemeister moves as path-constructors in a corresponding higher inductive type, and Wirtinger presentations as giving a map from this HIT to the type of groups.

Posted by: Mike Shulman on May 9, 2013 9:18 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

The question that John poses is related to that of studying all group presentations of a group and Tietze transformations between them. That in turn is related to rewriting presentations of any mathematical structure, monoids, algebraic theories etc, and so, presumably, to the relationship between combinatorial homotopy theory and homotopical algebra. The first studying the presentations of the objects of the second. Interesting idea if it could be approached from a Homotopy Type Theory direction?

Posted by: Tim Porter on May 10, 2013 6:53 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

I’m not sure what it would look like to define a knot drawing inductively, unless it would mean having the 0-crossing knot diagram as our base case. Then define an n-crossing knot diagram as taking any (n-1)-crossing knot diagram and adding a crossing (via Reidemeister moves and possibly a knotting move–exchanging a over-crossing for an under-crossing).

Meanwhile, it might also be fun to think of the alternative Markov moves for creating any knot diagram from another equivalent one as long as both are given in closed braid form. The second link gives one way to picture the Markov moves, but I think of them as 1) conjugation in the braid group, and 2) the first Reidemeister move.

Posted by: stefan on May 10, 2013 9:49 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Mike wrote:

Is there any way in which knot drawings can be defined inductively?

The homotopy type of the knot complement can be defined and studied not only for knots but also for tangles. And I believe that there’s a monoidal functor from a category where the morphisms are drawings of tangles to a category where the morphisms are ‘tangle complements’. In the first category, a morphism from $m$ to $n$ is a drawing of a tangle with $m$ strands coming in and $n$ going out. In the second category, a morphism from $m$ to $n$ is a cospan

$\mathbb{R}^2 - m \to X \leftarrow \mathbb{R}^2 - n$

where $\mathbb{R}^2 - m$ is the plane with $m$ points removed, similarly for $\mathbb{R}^2 - n$ , and $X$ is the complement of a tangle. In this second category, composition is the usual composition of cospans, using a pushout.

(Both these categories might profitably be viewed as $(\infty,1)$ categories. In the first, we have Reidemeister moves going between tangles as 2-morphisms, and so on. In the second, we have homotopy equivalences of cospans as 2-morphisms, and so on.)

The first category allows us to build up complicated pictures of tangles ‘inductively’ by composing and tensoring a few very simple ones:

I don’t know if this is the sort of induction you want, thought!

I’ve mainly seen this idea studied in John Armstrong’s paper The extension of knot groups to tangles. He doesn’t consider the whole homotopy type of the tangle complement, just the 1-type. In this case the process of composing cospans that I mentioned boils down to the Seifert–van Kampen formula for computing the fundamental group of a union of two spaces. He also focuses on the usual 1-category where morphism are tangles, not the $(\infty,1)$ -category I’m vaguely imagining, where 1-morphisms are tangle drawings, 2-morphisms are Reidemeister moves, etcetera etcetera. (One way to make this ‘etcetera etcetera’ precise is by considering a space of drawings of tangles.)

Tim wrote:

The question that John poses is related to that of studying all group presentations of a group and Tietze transformations between them. That in turn is related to rewriting presentations of any mathematical structure, monoids, algebraic theories etc, and so, presumably, to the relationship between combinatorial homotopy theory and homotopical algebra. The first studying the presentations of the objects of the second. Interesting idea if it could be approached from a Homotopy Type Theory direction?

Good question! I only know some vaguely related work, nicely summarized here:

Yves Guiraud, Homotopy of higher categories and rewriting.

They got into using polygraphs ( $\simeq$ computads), strict $\omega$ -categories, and a model structure on strict $\omega$ -categories developed here:

Yves Lafont, Francois Metayer, Krzysztof Worytkiewicz, A folk model structure on omega-cat.

You probably know about this stuff too. I imagine that homotopy type theory might be another nice way to formalize these syntactic/homotopy-theoretic considerations.

Posted by: John Baez on May 10, 2013 11:04 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

The work of Yves Guiraud and Philippe Malbos, both at the moment in PPS, was one of the sources of my comment. (I put a few more references on the n-Lab pages on them.) There is a nice possibility of using that stuff for Petri net analysis, but I do not know if it is possible to stochasticise n-categories or n-polygraphs in an intuitive and useful way.

Posted by: Tim Porter on May 11, 2013 6:26 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Ah, I see we’re getting back into cobordism/tangle hypothesis territory. Maybe we can describe this in HoTT with two steps of induction:

Define the category of tangles, using a HIT to implement its presentation as the free braided monoidal category on a dualizable object or whatever.
Define a functor on this category by recursion taking each tangle to its complement, where each recursive step uses a HIT (maybe just a pushout) to combine complements of smaller knots into the complement of larger ones.

Posted by: Mike Shulman on May 15, 2013 9:49 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Well, there are definitely plenty of applications of string diagrams that haven’t been formalized yet. If I recall correctly, only some fraction of the styles described in Selinger’s overview have been formalized. And then there are surface diagrams in all their forms.

By the way, I know you want to make a contrast to the higher-dimensional nature of diagrams, but I would be wary of putting too much emphasis on the “linear” nature of traditional syntax. There are other “nonlinear” ways to represent it, such as with labeled abstract trees, that I think most mathematicians would regard as equally formal and precise. Moreover, computers manipulating syntax generally use the nonlinear forms internally, and I think one can make a good case that so do humans (internally) — even if we generally write them out in a linear way in order to communicate from human to human, or from human to computer. Finally, traditional syntax isn’t even completely linear the way it’s usually written, e.g. matrices in linear algebra or sub- and superscripts on summation signs and integrals.

Posted by: Mike Shulman on May 3, 2013 6:27 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

By complete coincidence, today I ran into some amusingly snarky and defensive comments by the famous electrical engineer Heaviside:

Those who may prefer a more formal and logically-arranged treatment may seek it elsewhere, and find it if they can; or else go and do it themselves.

and

I think I have given sufficient information to enable any competent person to follow up the matter in more detail if it is thought to be desirable. It is obvious that the methods of the professedly rigorous mathematicians are sadly lacking in demonstrativeness as well as in comprehensiveness.

and

It is rather disagreeable to have to be self-assertive and dogmatic (especially when one thinks of the always possible risk of error); but there may be times when it becomes a duty—e.g., when mathematical rigourists are obstructive.

These are from a delightful article on Heaviside’s operational calculus. Fans of hard-to-rigorize manipulations with divergent series should enjoy this! Now I can better understand Heaviside’s remark

The series diverges; therefore we can do something useful with it.

Posted by: John Baez on May 2, 2013 10:28 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Here’s Tom Körner:

Oliver Heaviside was one of those men who always carry around a red rag on the off chance that they may see a bull to wave it at.

Posted by: Tom Leinster on May 2, 2013 11:01 PM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

I think the talk was great! It’s at least amusing that it’s precisely the ‘uninteresting’ equations $x=x$ that in type theory are the constructors that generate all equalities inductively. That is, the induction principle for Martin-Löf identity types says that if you want to prove something about all equalities, it’s enough to prove it for uninteresting ones. (-:

Posted by: Mike Shulman on May 7, 2013 5:07 AM | Permalink | Reply to this

Re: How Does Applied Math Impact Foundations?

$MathML-enabled post (click for more details).$

Thanks! That’s interesting, not uninteresting.

Posted by: John Baez on May 7, 2013 11:27 PM | Permalink | Reply to this

Read the post Categories for the Working Philosopher
Weblog: The n-Category Café
Excerpt: Elaine Landry is editing a book called Categories for the Working Philosopher.
Tracked: November 18, 2013 4:48 AM

The n-Category Café

Skip to the Main Content

April 30, 2013