Joel Hamkins interviewed on About Logic

It's a real eye opener, this one!

I got a bit carried away in the comments because they asked for questions:

Yes, this is great! 18:27 I have a question I would ask him on fictionalism / formalism / realism / structuralism: Aren't these Universes [which] Set Theory holds to be real objective things ultimately all models described in some metalanguage of their own? I'm just thinking of the tiny class of ones I have heard about, such as the Von Neumann cumulative hierarchy with this and that extra cardinals, say. It seems to take quite a lot to define V_\alpha let alone these higher cardinals, and isn't that new metalanguage just another language that one day will have to be formalised, and won't that require a new metalanguage and so on and so forth? So is it really those constructions which are real, or is there another more fundamental concept that is real, one that these are all just instances of?

This seems to me to be the idea Lawvere had with the theory of the Category of categories. I heard him say in a talk he gave some time in 2020 that the idea he had was "To finitely present one algebraic structure which captures a nodal state of mathematics at some point in time." (He was quite into Marx). Then I guess these nodal states would be forming at various times and in various branches of mathematics, so you are still left with an epistemic picture of the development of the whole, but why can this idea of the fundamentally syntactic form not be the real objective structure that lies behind set theory and mathematics in general? It's quite easy to formalize because you can describe a metagrammar in a grammar quite trivially, and Functor Categories exhibit a duality between syntax and semantics via adjoint pairs which produce beautiful symmetry-preserving lattices that can be extended without bounds.

26:24 Modulo some possible confusion between modal logics and model logics, aren't all first-order logics defined by definitions of truth-in-a-model a la Tarski? They are defined in a metalanguage ([called] syntax language in the olden days) which gives a denotation for every well-formed statement in the object language, usually in terms of elements of some set of truth values? So if the modal logics so constructed in terms of these models are all fundamentally in terms of some first-order set theory, then might that not be the reason that set theorists feel they are uncovering objective facts about independently existing Universes of sets? If some complete madman were to cook up a model that was not in any recognisable way anything you could hope to describe in a first-order set theory, then they would presumably reject it, wouldn't they? I have an example if anyone is interested, my email address is in my YouTube profile. It's seventeen years old and no set theorist who has read it (this is a non-empty set, because it contains at least one element who is denoted by the good name Thomas) has ever had anything to say about it. The thing is, I think there are some unspoken rules operating in set theory and they're more of the character of sociology than logic. But that's interesting too!

55:02 I have another question I would like to ask him, if that's OK. It's again about formal models, but models of theories modulo deduction systems. It is often said that intuitionistic logic is more expressive than classical logic, and that is at the heart of the reason why the distinction between proof of a negation and proof by contradiction is important to constructivist mathematicians. It's because if you can just admit the constructive mathematician to your house for long enough to understand how they can mathematically model a classical proof system and explicitly construct the whole theory, then that it is all actually a subset of the model in Homotopy Type Theory. This is actually a plan that Awodey et al are trying to carry out in Lean. So it is conceivable that in the not too distant future one will be able to formalise all of Lean's MathLib which is the theory of ZFC, in Homotopy Type Theory, in a formal system which is just Martin-Löf's intuitionistic type Theory, and does not admit the Law of Excluded Middle. In such a system you will be able to formally prove, in a quite direct manner, all the important historical theorems of Classical mathematics before Brouwer was even born. So the question is "Why is it harmful to expose undergraduates to constructive mathematics before they have learned to prove, say, the Radon-Nikodym theorem?" In other words, why not give undergraduates a training in Mathematics which is explicit about what constitutes a proof, and therefore which gives them one (or more) intuitive reason(s) as to why the Radon-Nikodym theorem is considered to be true and by whom and under precisely what circumstances? In yet other words, why is it better to study ever increasingly elaborate classical theorems about inaccessible cardinals and independence proofs of "almost everything," as he said, than learn a constructive proof system in which all of these proofs can be expressed and formally verified?

@GrothenDitQue That's an interesting way to put it, I've never heard that before. I guess it's a species of radical formalism? But what if someone, a Chinese person, for example, or better still an extraterrestrial intelligence, comes and asks for a formal definition of, say a symbol representing a literal token in the grammar? If you take a 'bivalent' view of syntax and semantics as dual structures in a lattice then you can "flip the lattice" and give a formal semantic definition of elements like the primitive literal tokens of the grammar, and you can go further and formally translate the symbols between Chinese and alien light-sounds or whatever they use. But ultimately you are still formalising the syntax, and you rely on any reader's actual knowledge of the meaning of the terms in which it is described. It's a bit hard to talk more about this without an actual example, but unfortunately I'm not Chinese, nor am an alien intelligence communicating in light-sounds. This reminds me of a story,...

The story is about a message John McCarthy posted some time around 2005/6 I think to the famous FoM list, which at the time was run by Martin Davis. McCarthy's post was to the effect of the objective nature of mathematics being evidenced by the fact that we can describe it to aliens in messages on plaques on Voyager spacecraft etc. I replied saying something to the effect that mathematics was all only up to isomorphism, so why not express it in intuitionistic arithmetic? And then I added that if an alien came down to earth and did a weird alien dance in front of someone, would they be sure to recognise it as mathematics? The message was rejected by Martin Davis on account of "not having sufficient foundational content". So that was the ignominious end to my career as a mathematical philosopher. Later on I got to see some very strong views expressed by a Reverse Mathematician on classical vs. intuitionistic logic which maybe explained the rejection. But I was greatly cheered to see a message from Martin Davis asking for peoples views on the equivalence between isomorphism and equality. This was around 2014 I saw it, just after the HoTT book was published. 43:43 It's not what one person teaches in an accredited course somewhere that determines what someone means when they say something! 47:10 It's not self-evident that teaching Classical mathematics isn't some day going to become harmful. It's not that long ago that G. H. Hardy was campaigning for undergraduates to learn to do more rigorous proofs in Calculus. Now they learn about diffeomorphism classes of smooth manifolds homeomorphic to R^4 and wonder why they are so diverse, and why nobody seems to care. Then they hear that the Pioneer Anomaly was explained by the first law of thermodynamics, so that's a relief: the aliens will eventually get their Math class!

Then someone mentioned Roger Penrose being criticised for abusing diagonal arguments so I had something to say about that too:

@drdca8263 OK, I read that in his book The Emperor's New Mind and a few years later he wrote a sequel where said he'd had a lot of feedback! In the sequel he extended this argument with maximally consistent models, trans-finitely and it got pretty complicated which must have quietened down the criticism! But I think in a way he was right about Gödel's theorem the first time, but he was wrong in saying we could see that the Gödel Sentence was true. He could see it, but without a formal proof how is he going to be able to convince anyone else? It's highly possible though that I am just inferior to him in a fundamental way, but how will I ever know? So does his argument tell me anything about the quantum world? I don't even know what that is! I did really enjoy his book and because of it I did a degree in mathematical sciences. It's good when someone is clear enough about what they believe that you can actually say why you think they are wrong.

Subscribe to About Logic.

This was probably because this morning I got told that I was low-key spamming the Assumptions of Physics Discord server because I didn't understand what the project was about, and that my posts were not related to what they were doing. I was just responding to this note on multi-decomposability of ensemble preparations being logically equivalent to superpositions of basis states in Hilbert space. I think it's a really good idea to make this formal distinction between measurements (i.e. ensemble preparations) and observables and the states they measure, but I think that it's important to include the relations between the basis states and the physical laboratory, because that is ultimately what determines the boundary between subsystems and this becomes crucial when you try to model entangled states. There is a well-defined formalism for this called Hilbert-Schmidt Operator Space. Maybe he thinks I am one of those annoying people he mentioned here.