This week I am at the conference Groupoids, Graphs and Algebras in Sydney. I gave a talk based on these two blog posts:
As well as the preprint
(which is a sequel to the papers Internal categories, anafunctors and localisations and
On Certain 2-Categories Admitting Localisation by Bicategories of Fractions).
The handwritten notes for my talk are here.
By this I mean the consistency, or inconsistency, of certain systems of mathematical axioms. There are very few systems, of very low strength, that we know are consistent. Presburger arithmetic is complete and consistent (and even decidable, but the decision procedure is has at least doubly-exponential runtime) but cannot even define the multiplication function 
One might ask in what system such implications are proved—what is the metatheory here? This leads to the remark in a blog post by Russell O’Connor:
As I understand, Gentzen showed that believing in the consistency of PA is equivalent to believing in the well-foundedness of ε0. This can be rephrased as a claim that a particular program, say the hydra game, terminates on all inputs. Therefore, if you believe in the well-foundness of ε0 and you believe Gentzen’s argument, which is done in PRA, then you believe PA is consistent, even if it has impredicative induction principles.
PRA has consistency strength equivalent to the well-foundness of ωω, which can be stated again as the termination of some other program on all inputs. Presumably this equivalence is proved in a still weaker system.
Curious about this ‘still weaker system’, I asked on MathOverflow “What is the weakest system that suffices to prove that well-foundedness of ωω implies consistency of PRA?” Emil Jeřábek provided a very nice answer, and even ironed out some wrinkles: it gets more difficult to talk about what well-foundedness means as the background theory gets weaker. Instead of the classical definition, which requires talking about subsets of the collection, one talks about induction schema instead, and how complex formulas can be that one wants to use. But in any case, the short answer is that the ‘still weaker system’ is the theory PA–, which is roughly the part of PA that models an ordered semiring (ie the natural numbers with their ordering) with no induction. This is basically Robinson arithmetic, which while incomplete (after Gödel) it is “only just” incomplete.
This then gets to the heart of ordinal analysis: if one believes the fragment of arithmetic capturing the ordered semiring structure of 
One can represent, as Jeřábek does on MathOverflow, the set ωω as the set of all finite tuples of natural numbers; in essence 
One could try to go down the rabbit hole, and ask what is the corresponding result for Q: what well-foundedness statement is enough to prove Q’s consistency? But it appears that the theories are getting so weak that one needs to resort to different tools. As far as PA is concerned, Timothy Chow gives a conceptual statement (see Theorem 2) equivalent to the well-foundedness of ε0
THEOREM 2. If M is a Turing machine that given i as input, outputs an ordinal M(i), and M(i) ≥ M(i+1) for all i, then the sequence stabilizes.
with a footnote saying “the theorem can be further weakened to assert the stabilization of all primitive recursive descending sequences of ordinals”. (Here by “ordinals” Chow means something he describes in finitary terms using finite nested lists à la Lisp)
If you find it ‘intuitive’ that ωω is well-founded, and Theorem 2 of Chow’s note convincing, then you have just been convinced that PA is consistent.
At the end of last year and beginning of this year I finally read Sydney Padua’s very entertaining graphic novel The thrilling adventures of Lovelace and Babbage about (parallel universe) Ada Lovelace, and then tracked down what seems like the only book on the Lovelace’s correspondence, Ada, Enchantress of Numbers, by Betty Toole.
The title of the latter is a slight misquote of something Babbage wrote of Lovelace, describing her as “Enchantress of Number”. I have skimmed through the Lovelace–de Morgan correspondence before, painstakingly and faithfully LaTeXed by Christopher Hollings, and was hoping for something in the latter book of a similar nature. Unfortunately all mathematical content is excised. And even some minor typographical changes are pervasive, such as rendering abbreviations like Weddy (for Wednesday) as Weddy. More unfortunate in Toole’s book is the forced analogies that the author tries to make between the conceptual ideas of Ada the person with the design and structure of the Ada programming language. While undoubtedly a thorough treatment of Lovelace’s correspondence would require familiarity with 19th century cultural norms and social history, any examination of precedents of 20th century computer science nascent in the letters to Babbage also requires more than passing knowledge of computer science. Such enthusiastic sections can be safely skipped. But overreaching claims aside, one can see that Lovelace thought deeply about the mathematics she was learning, and how it might be applied to other situations, some rather novel. In the following letter of 1840 she is thinking about how one might mathematically analyse a peg solitare game.
I feel Toole’s book, which consists of chapters of (edited) letters of Lovelace together with explanatory text, lacks somewhat in that one almost always only gets the letters in one direction (there are a few letters from Babbage or de Morgan, for instance, to Lovelace)—unlike the digital Lovelace–de Morgan correspondence. However, at the least, one gets to see the development of Lovelace’s personality from childhood to married life and being a parent while trying to study mathematics, and on to her decline and slow death from cancer. The letters paint a fascinating picture of Victorian Society, whereby mesmerism is seen as a form of medical treatment (though not without some scepticism on Ada’s part against her mother’s urging), and electromagnetism is in the process of being discovered, and mathematics is just about to go through somewhat of a revolution (in the 1830s-40s rigorous analysis was just being established, as was logic as a mathematical discipline). Lovelace’s creativity is surprising, but I would not be surprised if there were periods of real mania, either drug-induced or due to mental health issues. This BBC article notes “At times, Ada certainly had an exaggerated sense of her own destiny. Many of her letters are very long and self-obsessed and often a bit over the top.” Metaphor is used freely and richly, though sometimes it is not clear whether it is fanciful and playful writing or being taken seriously; Toole at times says that Lovelace really did mean the more ‘spacey’ of the descriptions, though it really is not clear. As Stephen Wolfram describes it, some of the letters between Lovelace and Babbage during the drafting and editing of the translation of Meabrea’s article and Lovelace’s attached Translator’s Note read like thick and fast email conversation around modern research (there were of course at the time multiple post deliveries per day, plus servants dispatched with additional letters).
It is this type of modern metaphor that Sydney Padua, freed from the constraints of needing to be historically accurate, plays with freely. The only time the cyberpunk/alternate history asthetic with its modern metaphors feels out of place is in the one ‘real history’ chapter (the opener), where Lovelace goes to tweet about a Babbage party she is at, momentarily mistaking her fan for a smartphone. But once the alternate history starts, the jodhpurs-wearing, pipe-smoking Lovelace is a wonderful character. Padua infuses the writing with a Victorian feel by lifting phrases and dialogue from Lovelace’s and Babbage’s letters, giving pointers when this is done and where they came from, in footnotes. Oh yes, the footnotes. There are footnotes on footnotes. There are pages of endnotes on each chapter, giving real-world historical insight into the fictionalised version. Other historical characters get a look in, such as the engineer Isambard Kingdom Brunel (here seen in the two bottom left panels), or Queen Victoria, whose offer of a variety of knighthood Babbage refused (in real life as in the comic) as it did not come with the honorific ‘sir’.
There is also a lot of historical material in the appendices, including contemporary articles that Padua sourced by trawling through Google scans of 19th century newspapers. Despite the fictional treatment of the historical characters, one can use Padua’s book at a stepping-off point to find real sources, which she carefully tracked down to inform her fiction, to read more about these larger-than-life personalities.
If only someone would edit a Lovelace–Babbage correspondence and included the mathematics and technical details, and gave informed commentary on the context coming from the history of mathematics at the time….
If 
write p/q = n + k/q, where 0 ≤ k/q < 1, equiv 0 ≤ k < q. if k = 0: halt; else return q/k, and loop.
is guaranteed to halt, since we must eventually hit 
Assume 
r = 1 + (r-1) --> 1/(r-1) = (r+1)/(r^2 - 1) = r+1 = 2 + (r-1) --> 1/(r-1)
Which will never halt, so no such rational number can exist.
I learned this nice proof from Doron Zeilberger’s manuscript Two Motivated Concrete Proofs (much better than the usual one) that the Square-Root of 2 is Irrational .
ON 31st July 1974 André Joyal gave a talk with the title Arithmetisation dans le topos. Anders Kock took notes, and kindly shared them with me a few years back. He gave me permission to host them publicly, so here they are: pdf link.
Just a quick note to advertise some slides by Taylor Dupuy recently presented at Rice University
Explicit Computations in IUT, slides for talk in AGNT Seminar, Rice University April 8, 2019 (pdf)
This is joint work with Anton Hilado modelled on his series of YouTube videos presented earlier this year (and there are links to them in the slides, for technical details). Note that all of this is explicitly stated by Dupuy as being conditional on Corollary 3.12 in Mochizuki’s third IUT paper, the written proof of which is not accepted by almost the entire number theory community.
I see the benefit here as at least simplifying what seems like the sound part of Mochizuki’s work (even if dependent on something still regarded as conjectural) to ordinary mathematics; no dismantling alien ring structures or odd metaphors about how school students get confused by logarithms. Not only that, but the statement of Corollary 3.12 is rendered in ordinary mathematics, rather than in the language of Frobenioids and their ilk.
Just a short post to point out the possibilities of writing cardinals in a more modern typeface. Pick your favourite solution from this list. The following compares the Euler math font version from the AMS with the FDSymbol version at the TeX.SE answer.
Code below the fold.
