About Logic - Is Mathematics a Story?

They're threatening to do this weekly, ...

Looking forward to the Dana Scott interview! Maybe there's not time to do this before then, but I would like to hear a discussion about the different views people have about models. I sometimes think that Computer scientists look for models in the zoo of mathematical theories, because they feel like this the only possible source of their legitimacy: they say something like "Well, this type system is sound because if it wasn't then ZFC would be inconsistent and you would have much bigger things to worry about than the soundness of my little type system!" But then serious mathematicians who have Fields medals come along and say "Well actually, I have these proofs that I've done in Higher Homotopy theory and I seriously doubt anyone has checked them as carefully as I did, and I am not sure that I haven't made a mistake somewhere, ..." and then they find a type system that a computer scientist cooked up out of some left-over intuitionistic logic he found somewhere and the Fields medalists start formalising proofs in it, relying on the soundness of the type system, ... So it seems very clear that if you want to use a "fiction as a model of meaning" interpretation of mathematics, then mathematicians are like characters in the story that are writing that very story themselves. When I have written stories and it's gone well, I have often felt like it was the characters in the story who were writing it, and what happened next followed almost inevitably from a sort of internal logic. Lawvere's idea of functorial semantics then starts to seem like the only hope!

[So is a Functor a metaphor for metaphor or is it just isomorphic to one, like a simile?]

Subscribe to About Logic.

Douglas Hofstadter on Analogy and Cognition

Starts at 13:33

Subscribe to Stanford TV.

From nLab page on categorical semantics:

One may interpret mathematical logic as being a formal language for talking about the collection of monomorphisms into a given object of a given category: the poset of subobjects of that object.

More generally, one may interpret type theory and notably dependent type theory as being a formal language for talking about slice categories, consisting of all morphisms into a given object.

Conversely, starting with a given theory of logic or a given type theory, we say that it has a categorical semantics if there is a category such that the given theory is that of its slice categories, if it is the internal logic of that category.

Subscribe to IAS.

See Vladimir Voevodsky - What if Current Foundations of Mathematics are Inconsistent.

To continue with the "mathematics is a story" analogy,... There are some features that good stories have, and so you might want those in mathematics too. For example, sometimes in a story something really surprising happens, apparently for no reason whatsoever, but later you discover that there was actually a really good reason for that event and then what once seemed completely nonsensical and "random" turned out to be essential. Another good feature of a story is that at the end things seem to connect together and resolve into a moral of some sort. Perhaps some people enjoy stories that branch out never-endingly, like spin-offs of a popular soap opera. It's certainly good for the TV industry, but after a while very few of the spin-offs ever reach the same level of interest the original series had. See Joel Hamkins interviewed on About Logic and Impredicativity, Computation and Sheafification, then see About Logic - Interview with Dana Scott.

A story about diagram algebras. Invented in 1932 by Georg Rumer, Edward Teller and Hermann Weyl. See Eine für die Valenztheorie geeignete Basis der binären Vektorinvarianten.

See Urs Schreiber on the $1 Million Puzzle in The Category Enriched over the Category of Finite Sets, The Finitely Triangulated Manifold and the Magnitude of a Finite Category for more on the strange kinds of states that can how up in statistical mechanics.

On diagrams and monoidal Categories see Physics, Topology, Logic and Computation: A Rosetta Stone by John C. Baez and Mike Stay and the talk by John Baez in 2021: John Baez on Symmetric Monoidal Categories A Rosetta Stone and Noson S. Yanofsky on Diagonalization, Fixed Points, and Self-reference.

Subscribe to Daniel Tubbenhauer.

See also this n-Category Café post by Mike Stay from May 26, 2015: A 2-Categorical Approach to the Pi Calculus.

Subscribe to Topos Institute.

Toby with a story about why π was a square rational in ancient Egypt:

Subscribe to Tibees.

Ben Syversen on Al-Khwārazmī's Algebra book:

Subscribe to Ben Syversen.

The moral seems to be that it is all about computation (or construction):

Subscribe to Euclidea.

This week's Premises podcast:

On set theory and what is the domain of a proposition (or what is a property a property of) see Stefan Milius - Demystifying Codensity Monads through Duality. See also these n-Category Cafe posts by Tom Leinster: Where Do Monads Come From? and Where Do Linearly Compact Vector Spaces Come From?

My comment:

It's always good to hear intelligent people talk about these things! On the axioms of ZFC, I think more should be said about the independence of the axiom of infinity. There is an intriguing footnote in Church's A Formulation of the Simple Theory of Types where mentions that the need for a type-raising operator in the definition of the natural numbers is due to this. It's connected to the way induction is defined in Kleene's scheme for constructing the predecessor function. But the more general issue is that the independence of axioms depends entirely on what other axioms are considered as part of the theory, so there must be something almost algebraic in the higher structure of axiom independence and it must induce/be induced by, some other corresponding structure in the models, but I have never heard anyone talk about this. Perhaps though it is inherent in Lawvere's idea of categorical semantics and it's just that I don't know the language so I can't see that it's talking about this.

Subscribe to About Logic.

I have heard about people doing this, just not for fist order set theory per se: see Thierry Coquand on Computational Interpretation of Topos Theory and The Category Enriched over the Category of Finite Sets, The Finitely Triangulated Manifold and the Magnitude of a Finite Category.

From Olivia Caramello's first lecture in her series Toposes for the Working Mathematician: