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.
Tomáš Jakl (Apr 03 2020 at 16:23):John Baez said:
I haven't gotten far enough to give a really clear explanation yet.
I have a question about first-order categorical logic, that @John Baez partially touches in his notes quoted above. I often see people mention that Lawvere solved a problem that people working in polyadic algebras or cylindrical algebras had, when he explained that quantifiers are just adjoints to the substitution map. For example, here is what Awodey says in his Category Theory textbook:
Traditionally, the main obstacle to the further development of algebraic logic has been the treatment of the quantifiers. Categorical logic solves this problem beautifully with the recognition (due to F.W. Lawvere in the 1960s) that they, too, are adjoint functors.
However, I never saw anybody explaining what is "the problem" that polyadic algebras couldn't solve. Any thoughts? Thank you!
John Baez (Apr 03 2020 at 20:12):I don't know what the problem was. Maybe they had trouble figuring out a good way to understand how quantifiers worked? Cylindric algebras do include a treatment of quantifiers and equality.
Tomáš Jakl (Apr 03 2020 at 21:13):From what I understand, they worked out the definition in the fifties and Henkin, Monk and Tarski published a book in 1971 encompassing the rich theory of cylindric algebras. This is still before Lawvere. I can't figure out what could be "the main obstacle to the further development" at the time of Lawvere.
Tomáš Jakl (Apr 03 2020 at 21:29):I found the explanation given by Marquis and Reyes in their "The history of categorical logic" satisfying. They wrote the following:
John Baez (Apr 03 2020 at 21:44):That makes sense to me. That may be the real obstacle: the lack of a visible connection between cylindric and polyadic algebras and other branches of math.
Tomáš Jakl (Apr 03 2020 at 21:52):Yes, I agree, it's a neat explanation. Still, I recall multiple sources claiming that algebraic logic was stuck when trying to capture quantification. Maybe, more politically correct would be to say that algebraic logic didn't capture quantifiers it in an "explanatory" way, so that we would learn something new we didn't know before.
John Baez (Apr 03 2020 at 21:53):Maybe. If they don't explain, and we don't talk to someone who was paying attention back then, we can only guess.
Ryan Wisnesky (Apr 03 2020 at 23:03):From a PL semantics point of view, cylindric algebras are not a 'syntax independent' semantics because they don't really 'get rid' of variables in the syntax, they just push them into the semantics. syntax independent and something called full abstraction are traditionally considered the two criteria for a 'good' denotational semantics of a programming language