Based on the dictionary given at 6:26 would it be accurate to think of a "logical system" as being a choice of class of categories, such as the class of monoidal categories, or Cartesian categories, for instance?
Yes because a "logical system" is not a mathematically defined term. Everything involving a set of primitives and composition on those primitives will be a "logical system" - a system whereby "logic"(deduction) can be done to express propositions in terms the primitives. The discussion tries to make it seem as if logic is some closed mathematical structure but logic is a general structure and a category is a logical structure where the objects are the primitives and morphisms is the composition. All abstract infinite logical structures are equivalent as there is a theorem in logic that says any logic is equivalent to a specific countable logic. Ultimately what people consider as "logics" are just variations on a theme and only different in some minute theoretical aspects. What happens is people learn one variation and believe it to sort of be a foundational thing then go learn something different and never realize it's actually the same thing. E.g., all mathematics, all programming, all science, at is just propositional logic. The only difference is that levels of abstraction are built. These levels of abstraction allow abstract out common and/or complex things. What is going on though, at the core, is logic... simple and straight forward composition and decomposition of things using and and not(or any variation). It's all binary at the end of the day. Even though a programmer might write a program in a high level language, he's still twiddling bits at the end of the day. What are bits? they are real numbers, ultimately, in reality, they are rational numbers... and what are rational numbers? Integers. What are integers? Strings of bits. Essentially one has a spectrum from most concrete(binary and computational logic) to least concrete(abstract mathematics and the theory of logic). Because of peoples ignorance(not an insult, just a fact, no one knows it all, not even close) they will "discover new things" which are not new but just a different perspective or interpretation. Sometimes it offers a new insight, sometimes it's just obfuscation. Category theory is an abstract recursive structure that is ideal for abstract representation of structure. Hence it can be used to describe virtually anything that has structure(anything can be an object and if we can do anything with those objects then there will be some morphisms to "combine" them). Structure is essentially synonymous with composition. So before category theory we had logic from which a new perspective/language to describe "logics" evolved - category theory. Now one can use category theory as the foundation to describe "logics". Category theory is more effective because it's language is more abstract. it is hard to fit, say, the theory differentiation equations in to the terminology of 2nd order logic. It can be done but the "mapping" is very complex because logic was not designed to understand abstract structure. E.g., what is the equivalent of a proposition? A conjunction? If you say a proposition is some differential equation and "and" is addition then DE1 and DE2 = DE3. What is not? Subtraction? Ok, well, we are just dealing with a ring of differential equation(or a polynomial ring with a differential operator) and are sort of not thinking "logically" but "algebraically". Category theory, OTH, has an agnostic language to describe structure(well, the most agnostic language) and so is more adept at converting logics in to it's jargon. This helps tremendously relate various logics(e.g., find functors). So it is useful to convert the "theory of logic" in to a categorical form and to convert other instances of logic in to such a categorical form so that we can see the common overlap of all these various instances of logic that humans have created. Then by having that common denominator we can see what we are really doing when we create these various logics and see something deeper going on. Ideally category theory would have been thought and learned first, but then all our math would likely just be category theoretic. This may have allowed for even deeper abstract theories to develop by now though. What it would have done is gave us all a common language(but humans love inventing languages so surely there would have been many others too). Ultimately we are trying to find the right way to frame things so be able to avoid introducing spurious junk in to "logic"/"structure"/"meaning"/"understand"/etc. It would be analogous to humans having only one spoken language. While it might be limiting in some ways it would allow everyone to speak the same language and so maybe less wars and arguments because of miscommunication because people have two different concepts of the same word. The only real question is "is this it". Essentially does category theory provide pretty much a "complete" and "general" framework for all intellectual discourse or will it just become another "outdated theory" supplanted by something else more powerful and more abstract? I believe that it's all the same thing and that our languages are created and designed to deal with the current level of abstraction that we can handle(including the masses that it eventually trickles down to to some degree) and as we are able to comprehend and build higher levels of meaningful abstraction those concepts and jargon will become our current theoretical language to use. This allows us to dive deeper and deeper in to the structure of the universe. There may or may not be a limit to this process and category theory might become the dominant language for the next century or two but it is likely once it becomes established enough(assuming that human intelligence and existence can keep up) humans will use it to create a new theory that can dive even deeper in to understanding the mathematical universe(which, remember is all binary... but we need a way to deal with the vast(infinite, think of the permutation group and all it's symmetries)) complexity in which we can combine 0's and 1's). E.g., even though we, relatively speaking, are creating very complex structures, they are, say, only on the order of 2^32 or 2^64... but eventually, if humanity doesn't collapse/exterminate itself, we will be at 2^120, 2^43245, etc. (of course we do run out of atoms to store information but by then we will probably discover ways to overcome that but to do that requires a level of abstraction we do not have right now. Remember though that if we have 2^10 binary objects then there are 2^2^10 representations they can contain. A typical 1TB drive has 2^64 objects and so one HD can represent one 2^2^40 binary object out of all 2^2^40 possibilities. The point is that as we figure out ways to store information the number of possibilities that we can store grows exponentially off that so we will never run out of having to try to "compress" down the complexity of what we are having to deal with(that is, we will always need some way to abstract complexity to be able to comprehend it... unless one day we run out of room)
Indeed, such would be a decent informal description. More formally, the notion you're looking for is the notion of "doctrine." Patterson, the speaker here, has worked on a notion of doctrine as what is called a "Cartesian Double Theory," although there are competing notions. Also interesting, the general idea of a doctrine is to do for categories what theories do for sets - a categorification of the idea of a theory.
Elementary toposes interpret higher-order logic, not just first-order logic (which is more closely linked to pretoposes) (see 19:00)
Based on the dictionary given at 6:26 would it be accurate to think of a "logical system" as being a choice of class of categories, such as the class of monoidal categories, or Cartesian categories, for instance?
Yes because a "logical system" is not a mathematically defined term. Everything involving a set of primitives and composition on those primitives will be a "logical system" - a system whereby "logic"(deduction) can be done to express propositions in terms the primitives.
The discussion tries to make it seem as if logic is some closed mathematical structure but logic is a general structure and a category is a logical structure where the objects are the primitives and morphisms is the composition. All abstract infinite logical structures are equivalent as there is a theorem in logic that says any logic is equivalent to a specific countable logic. Ultimately what people consider as "logics" are just variations on a theme and only different in some minute theoretical aspects.
What happens is people learn one variation and believe it to sort of be a foundational thing then go learn something different and never realize it's actually the same thing. E.g., all mathematics, all programming, all science, at is just propositional logic. The only difference is that levels of abstraction are built. These levels of abstraction allow abstract out common and/or complex things.
What is going on though, at the core, is logic... simple and straight forward composition and decomposition of things using and and not(or any variation). It's all binary at the end of the day. Even though a programmer might write a program in a high level language, he's still twiddling bits at the end of the day. What are bits? they are real numbers, ultimately, in reality, they are rational numbers... and what are rational numbers? Integers. What are integers? Strings of bits.
Essentially one has a spectrum from most concrete(binary and computational logic) to least concrete(abstract mathematics and the theory of logic). Because of peoples ignorance(not an insult, just a fact, no one knows it all, not even close) they will "discover new things" which are not new but just a different perspective or interpretation. Sometimes it offers a new insight, sometimes it's just obfuscation.
Category theory is an abstract recursive structure that is ideal for abstract representation of structure. Hence it can be used to describe virtually anything that has structure(anything can be an object and if we can do anything with those objects then there will be some morphisms to "combine" them). Structure is essentially synonymous with composition. So before category theory we had logic from which a new perspective/language to describe "logics" evolved - category theory. Now one can use category theory as the foundation to describe "logics". Category theory is more effective because it's language is more abstract. it is hard to fit, say, the theory differentiation equations in to the terminology of 2nd order logic. It can be done but the "mapping" is very complex because logic was not designed to understand abstract structure. E.g., what is the equivalent of a proposition? A conjunction? If you say a proposition is some differential equation and "and" is addition then DE1 and DE2 = DE3. What is not? Subtraction? Ok, well, we are just dealing with a ring of differential equation(or a polynomial ring with a differential operator) and are sort of not thinking "logically" but "algebraically".
Category theory, OTH, has an agnostic language to describe structure(well, the most agnostic language) and so is more adept at converting logics in to it's jargon. This helps tremendously relate various logics(e.g., find functors). So it is useful to convert the "theory of logic" in to a categorical form and to convert other instances of logic in to such a categorical form so that we can see the common overlap of all these various instances of logic that humans have created. Then by having that common denominator we can see what we are really doing when we create these various logics and see something deeper going on.
Ideally category theory would have been thought and learned first, but then all our math would likely just be category theoretic. This may have allowed for even deeper abstract theories to develop by now though. What it would have done is gave us all a common language(but humans love inventing languages so surely there would have been many others too).
Ultimately we are trying to find the right way to frame things so be able to avoid introducing spurious junk in to "logic"/"structure"/"meaning"/"understand"/etc.
It would be analogous to humans having only one spoken language. While it might be limiting in some ways it would allow everyone to speak the same language and so maybe less wars and arguments because of miscommunication because people have two different concepts of the same word.
The only real question is "is this it". Essentially does category theory provide pretty much a "complete" and "general" framework for all intellectual discourse or will it just become another "outdated theory" supplanted by something else more powerful and more abstract? I believe that it's all the same thing and that our languages are created and designed to deal with the current level of abstraction that we can handle(including the masses that it eventually trickles down to to some degree) and as we are able to comprehend and build higher levels of meaningful abstraction those concepts and jargon will become our current theoretical language to use. This allows us to dive deeper and deeper in to the structure of the universe. There may or may not be a limit to this process and category theory might become the dominant language for the next century or two but it is likely once it becomes established enough(assuming that human intelligence and existence can keep up) humans will use it to create a new theory that can dive even deeper in to understanding the mathematical universe(which, remember is all binary... but we need a way to deal with the vast(infinite, think of the permutation group and all it's symmetries)) complexity in which we can combine 0's and 1's). E.g., even though we, relatively speaking, are creating very complex structures, they are, say, only on the order of 2^32 or 2^64... but eventually, if humanity doesn't collapse/exterminate itself, we will be at 2^120, 2^43245, etc. (of course we do run out of atoms to store information but by then we will probably discover ways to overcome that but to do that requires a level of abstraction we do not have right now. Remember though that if we have 2^10 binary objects then there are 2^2^10 representations they can contain. A typical 1TB drive has 2^64 objects and so one HD can represent one 2^2^40 binary object out of all 2^2^40 possibilities. The point is that as we figure out ways to store information the number of possibilities that we can store grows exponentially off that so we will never run out of having to try to "compress" down the complexity of what we are having to deal with(that is, we will always need some way to abstract complexity to be able to comprehend it... unless one day we run out of room)
Indeed, such would be a decent informal description. More formally, the notion you're looking for is the notion of "doctrine." Patterson, the speaker here, has worked on a notion of doctrine as what is called a "Cartesian Double Theory," although there are competing notions. Also interesting, the general idea of a doctrine is to do for categories what theories do for sets - a categorification of the idea of a theory.
I'm curious how Category Theory views the Langlands Program and vice versa
thank you! this was very insightful and useful, although the sound sometimes kinda fails; ❤️❤️