You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Morgan Rogers (he/him) (Feb 12 2025 at 14:42):To hazard a guess at what Mike was referring to, it's that no matter what syntax you're dealing with, the subject of results in logic are collections of syntactic structures such as strings of symbols; formalizing any reasoning we do about these collections (such as inductive arguments) produces set-theory-like mathematics.
That said, I learned a few years ago that philosophers of computer science are happy to avoid the "holism" that the above assertion imposes. There may be no need in practice to make statements about the collection of all well-formed formulas. A proof by induction on the structure of syntax can be seen 'reductionistically' as a proof schema that allows us to prove some property only once we are provided with a specific instance of that syntax, rather than 'holistically' proving a statement about the collection of all strings all at once. (Here I am using a dichotomy/contrast that I first saw in Hofstadter's book GEB.)
Holism is so conceptually useful to me in my mathematical practice (indeed, it underlies the effectiveness of category theory imo) that I struggle to sympathise with the reductionist viewpoint, but it's clearly out there!
Vincent R.B. Blazy (Feb 12 2025 at 15:15):@Morgan Rogers (he/him) Yes, we agree on that! The circularity isn’t ontologically necessary, but indeed collections happen everywhere when conceptualising anything and so, that’s why holism is so useful in practice and set theories are so nice to analytically found mathematics, after all! :blush:
Mike Shulman (Feb 12 2025 at 20:10):@Zoltan A. Kocsis (Z.A.K.) I meant basically your first weaker version. By saying "set-theory-like" I meant that I think you need a general sort of mathematics in which you can talk about "collections of things". So I don't think your example of axiomatic projective geometry works, because I don't see how one could define variables and terms purely in terms of points and lines. Maybe there's a way, but it would be pretty artificial. I don't mean formal set theory, just the "informal" kind of set theory that most people learn in their first proof-based math classes.
Mike Shulman (Feb 12 2025 at 20:23):As you said with your example of first-graders, depending on how much logic you want to do, you may need more or less sophistication in this ambient informal mathematics, and for the very basic stuff you can get by with elementary-school math. But for more advanced logic you need to be able to talk about collections of things, functions between them, and so on -- the stuff that all mathematicians do, whether or not they understand a formal set theory like ZFC.
Mike Shulman (Feb 12 2025 at 20:37):I think the introduction to the book *Mathematical Logic: Part I" by Cori and Lascar does a good job describing the status of logic as a field of mathematics.
Alex Kreitzberg (Feb 13 2025 at 01:45):I'm going to have to sit with that introduction, that's quite a dramatic, and exciting, reframing of how I understand logic.
Evan Washington (Feb 13 2025 at 01:49):John Baez said:
I think in my childhood search for maximum certainty I should have learned about the Chomsky hierarchy and wondered how high up this hierarchy we need to climb, to get a formalism powerful enough to describe the set of provable sentences in some version of first-order logic. I liked the idea that ultimately to do math you just needed to understand some purely syntactic rules for manipulating strings of symbols, so I was curious about what exactly is a "rule for manipulating strings of symbols". I realized that a rule like "if the string is a true sentence, then..." is not purely syntactic (unless you have a syntactic definition of truth!), but I would have loved learning about the Chomsky hierarchy.
How far up do you need to climb in Chomsky's hierarchy to describe the theorems of first-order logic? The answer to this is actually rather straightforward: you need to climb all the way up! (to the recursively enumerable languages).
And to the original question:
John Baez said:
can you use BNF to describe the well-formed formulae in a language that has infinitely many function symbols of each arity 0,1,2,3,... ? Or can it only handle something less, like finitely (or infinitely) many function symbols of some finite collection of arities, which is already enough for the mathematics I do?
Well, in theory no, not really (unless you want to help yourself to infinitely long clauses in the BNF definition). In practice, though, you're going to presumably want to use those symbols to write down terms and formulas, so you'll probably use some nice computable/recursive definition of those symbols (like we do with numerals, for instance).
John Baez (Feb 13 2025 at 02:17):Thanks! Yes, it makes sense that to describe theorems you need the full power of a recursively enumerable language.
Vincent R.B. Blazy (Feb 13 2025 at 10:58):Mike Shulman said:
Zoltan A. Kocsis (Z.A.K.) I don't think your example of axiomatic projective geometry works, because I don't see how one could define variables and terms purely in terms of points and lines.
Well, that would introduce back a circularity, since points and lines already need syntax to deine and even talk about them at all? But,the point precisely was to avoid circularity, not to get it back... :thinking:
Vincent R.B. Blazy (Feb 13 2025 at 11:04):Evan Washington said:
John Baez said:
can you use BNF to describe the well-formed formulae in a language that has infinitely many function symbols of each arity 0,1,2,3,... ? Or can it only handle something less, like finitely (or infinitely) many function symbols of some finite collection of arities, which is already enough for the mathematics I do?
Well, in theory no, not really (unless you want to help yourself to infinitely long clauses in the BNF definition). In practice, though, you're going to presumably want to use those symbols to write down terms and formulas, so you'll probably use some nice computable/recursive definition of those symbols (like we do with numerals, for instance).
Well, that's pretty what I described here, right? After all, even in theory, metamathematical infinities can only be potential, so, finitely describable only with some kind of recursion; and that's precisely already the core of what BNFs allow :)