## February 27, 2015

### Concepts of Sameness (Part 4)

#### Posted by John Baez

This time I’d like to think about three different approaches to ‘defining equality’, or more generally, introducing equality in formal systems of mathematics.

These will be taken from old-fashioned logic — before computer science, category theory or homotopy theory started exerting their influence. Eventually I want to compare these to more modern treatments.

If you know other interesting ‘old-fashioned’ approaches to equality, please tell me!

Posted at 10:21 AM UTC | Permalink | Followups (32)

## February 26, 2015

### Introduction to Synthetic Mathematics (part 1)

#### Posted by Mike Shulman

John is writing about “concepts of sameness” for Elaine Landry’s book Category Theory for the Working Philosopher, and has been posting some of his thoughts and drafts. I’m writing for the same book about homotopy type theory / univalent foundations; but since HoTT/UF will also make a guest appearance in John’s and David Corfield’s chapters, and one aspect of it (univalence) is central to Steve Awodey’s chapter, I had to decide what aspect of it to emphasize in my chapter.

My current plan is to focus on HoTT/UF as a synthetic theory of $\infty$-groupoids. But in order to say what that even means, I felt that I needed to start with a brief introduction about the phrase “synthetic theory”, which may not be familiar. Right now, my current draft of that “introduction” is more than half the allotted length of my chapter; so clearly it’ll need to be trimmed! But I thought I would go ahead and post some parts of it in its current form; so here goes.

Posted at 6:15 AM UTC | Permalink | Followups (50)

## February 25, 2015

### Concepts of Sameness (Part 3)

#### Posted by John Baez

Now I’d like to switch to pondering different approaches to equality. (Eventually I’ll have put all these pieces together into a coherent essay, but not yet.)

We tend to think of $x = x$ as a fundamental property of equality, perhaps the most fundamental of all. But what is it actually used for? I don’t really know. I sometimes joke that equations of the form $x = x$ are the only really true ones — since any other equation says that different things are equal — but they’re also completely useless.

But maybe I’m wrong. Maybe equations of the form $x = x$ are useful in some way. I can imagine one coming in handy at the end of a proof by contradiction where you show some assumptions imply $x \ne x$. But I don’t remember ever doing such a proof… and I have trouble imagining that you ever need to use a proof of this style.

If you’ve used the equation $x = x$ in your own work, please let me know.

Posted at 1:20 AM UTC | Permalink | Followups (39)

## February 23, 2015

### Concepts of Sameness (Part 2)

#### Posted by John Baez

I’m writing about ‘concepts of sameness’ for Elaine Landry’s book Category Theory for the Working Philosopher. After an initial section on a passage by Heraclitus, I had planned to write a bit about Gongsun Long’s white horse paradox — or more precisely, his dialog When a White Horse is Not a Horse.

However, this is turning out to be harder than I thought, and more of a digression than I want. So I’ll probably drop this plan. But I have a few preliminary notes, and I might as well share them.

Posted at 3:31 AM UTC | Permalink | Followups (49)

### Concepts of Sameness (Part 1)

#### Posted by John Baez

Elaine Landry is a philosopher at U. C. Davis, and she’s editing a book called Categories for the Working Philosopher. Tentatively, at least, it’s supposed to have chapters by these folks

• Colin McLarty (on set theory)
• David Corfield (on geometry)
• Michael Shulman (on univalent foundations)
• Steve Awodey (on structuralism, invariance, and univalence)
• Michael Ernst (on foundations)
• Jean-Pierre Marquis (on first-order logic with dependent sorts)
• John Bell (on logic and model theory)
• Kohei Kishida (on modal logic)
• Robin Cockett and Robert Seely (on proof theory and linear logic)
• Samson Abramsky (on computer science)
• Michael Moortgat (on linguistics and computational semantics)
• Bob Coecke and Aleks Kissinger (on quantum mechanics and ontology)
• James Weatherall (on spacetime theories)
• Jim Lambek (on special relativity)
• John Baez (on concepts of sameness)
• David Spivak (on mathematical modeling)
• Hans Halvorson (on the structure of physical theories)
• Elaine Landry (on structural realism)
• Andrée Ehresmann (on a topic to be announced)

We’re supposed to have our chapters done by April. To make writing my part more fun, I thought I’d draft some portions here on the $n$-Café.

Posted at 12:20 AM UTC | Permalink | Followups (33)

## February 18, 2015

### Quantum Physics and Logic at Oxford

#### Posted by John Baez

There’s a workshop on quantum physics and logic at Oxford this summer:

Posted at 9:52 PM UTC | Permalink | Followups (1)

## February 12, 2015

### Can a Computer Solve Lebesgue’s Universal Covering Problem?

#### Posted by John Baez

Here’s a problem I hope we can solve here. I think it will be fun. It involves computable analysis.

To state the problem precisely, recall that the diameter of a set of points $A$ in a metric space is

$diam(A)=\sup\{d(x,y) : x,y\in A\}$

Recall that two subsets of the Euclidean plane $\mathbb{R}^2$ are isometric if we can get one from the other by translation, rotation and/or reflection.

Finally, let’s define a universal covering to be a convex compact subset $K$ of the Euclidean plane such that any set $A \subseteq \mathbb{R}^2$ of diameter $1$ is isometric to a subset of $K$.

In 1914 Lebesgue posed the puzzle of finding the universal covering with the least area. Since then people have been using increasingly clever constructions to find universal coverings with smaller and smaller area.

My question is whether we need an unbounded amount of cleverness, or whether we could write a program to solve this puzzle.

There are actually a number of ways to make this question precise, but let me focus on the simplest. Let $\mathcal{U}$ be the set of all universal coverings. Can we write a program that computes this number to as much accuracy as desired:

$a=inf\{ area(K) : K \in \mathcal{U}\} \; ?$

More precisely, is this real number $a$ computable?

Right now all we know is that

$0.832 \le a \le 0.844115376859\dots$

though Philip Gibbs has a heuristic argument for a better lower bound:

$0.84408 \le a$

Posted at 12:53 AM UTC | Permalink | Followups (46)

## February 9, 2015

### Higher-Dimensional Rewriting in Warsaw

#### Posted by John Baez

This summer there will be a conference on higher-dimensional algebra and rewrite rules in Warsaw. They want people to submit papers! I’ll give a talk about presentations of symmetric monoidal categories that are important in electrical engineering and control theory. There should also be interesting talks about combinatorial algebra, homotopical aspects of rewriting theory, and more:

Here’s a description…

## February 4, 2015

### More on the AMS and NSA

#### Posted by Tom Leinster

Just a quickie. This month’s Notices of the AMS ran an article by Michael Wertheimer, recently-retired Director of Research at the NSA, largely about the accusation that the NSA deliberately created a backdoor in a standard cryptographic utility so that they could decode the messages of anyone using it.

Wertheimer’s protestations garnered an unusual amount of press and a great deal of scepticism (e.g. Le Monde, Ars Technica, The Register, Peter Woit, me), with the scepticism especially coming from crypto experts (e.g. Matthew Green, Ethan Heilman).

Some of those experts — also including Bruce Schneier — are writing to the Notices pointing out how misleading Wertheimer’s piece was, with ample historical evidence. And crucially: that in everything Wertheimer wrote, he never actually denied that the NSA created a backdoor.

If you support this letter — and if more broadly, you think it’s important that the AMS reconsiders its relationship with the NSA — then you can add your signature.

Update:   The letter from Green, Heilman and Schneier has just appeared in the June/July 2015 issue of the Notices of the AMS, under the title “Misleading mathematicians”.

Posted at 2:37 AM UTC | Permalink | Followups (21)

### Lebesgue’s Universal Covering Problem

#### Posted by John Baez

Lebesgue’s universal covering problem is famously difficult, and a century old. So I’m happy to report some progress:

• John Baez, Karine Bagdasaryan and Philip Gibbs, Lebesgue’s universal covering problem.

But we’d like you to check our work! It will help if you’re good at programming. As far as the math goes, it’s just high-school geometry… carried to a fanatical level of intensity.

Posted at 1:23 AM UTC | Permalink | Followups (13)