5 ms·

An amazing book that takes a clear and descriptive path to topos theory. If you want to take it a little slower, you can start with Lawvere's "Conceptual Math

An amazing book that takes a clear and descriptive path to topos theory. If you want to take it a little slower, you can start with Lawvere's "Conceptual Mathematics" https://api.pageplace.de/preview/DT0400.9780511590092_A23569066/preview-9780511590092_A23569066.pdf https://api.pageplace.de/preview/DT0400.9780511590092_A23569...

auggierose 2y ago
I've seen toposes declared as some fundamental notion, and I'd very much like to understand them. Is there a short definition somewhere out there of what a topos is in terms of first-order predicate logic? Something I can understand without reading through 200 pages of preliminary material first? I've seen statements that such a formulation in first-order logic would be misguided, because category theorists have their own notion of logic, but I'd like to understand it using my own notion of logic first.
- hackandthink 2y ago
  Makkai's work my fit: "First Order Logic with Dependent Sorts,with Applications to Category Theory" "For instance, the definition of elementary topos (with operations defined by universal properties up to isomorphism, not specified as univalued operations) can be given as a finite set of sentences in FOLDS." https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf
  - auggierose 2y ago
    Interesting find, but again an example of where you first need to learn some new logic FOLDS ("FOLDS has the first two of these, contexts and types (although the latter are called 'sorts'), but it does not have the third, terms (except in the rudimentary form of mere variables), and it has equality in a greatly restricted form only."). I wonder if it is impossible to describe a topos as a normal axiom system of first-order logic, or if people are just unwilling to do it.
- soist 2y ago
  The logic of toposes is higher order intuitionistic logic. The logic of higher toposes is presumed to be intensional dependent type theory. The best introduction to these logics is probably the homotopy type theory book.
  - auggierose 2y ago
    I cannot understand the homotopy type theory book. It just makes no sense to me, sorry. > The logic of toposes is higher order intuitionistic logic. Yes, I have read that a lot. Eventually, I would like to understand how toposes form a model of higher-order intuitionistic logic (which is what "The logic of toposes is higher order intuitionistic logic" probably means?). But first, I would like to understand what a topos is in first-order logic terms. You know, baby steps.
    - soist 2y ago
      The category of sets is a topos and can be expressed/presented with first order classical logic but the general logic of toposes is intuitionistic and non-classical. There is no single topos with a single logic, each topos has its own logic and the common thread is that they're non-classical and higher order.
      - auggierose 2y ago
        So are you saying that "T is a topos" cannot be expressed via first-order classical logic? Unlike something such as "G is a group", or "T is a topology" or "C is a category"?
        soist 2y ago
        None of your examples are expressible in first order logic either. Those are all instances of mathematical structures which can be formalized in different toposes with different logics. Groups in the topos of sets are different from groups in the topos of smooth sets. The structure of a group can be expressed as a diagram which can then be interpreted in any topos with the prerequisite mathematical structures. Toposes have products (finite limits) so every topos can potentially have group objects just like every topos can have a natural number object which is an initial algebra (colimit) for a certain diagram. In any case, there is no royal road and if you're not willing to spend the time and effort to learn what others have written about toposes then there isn't much I can help you with here. There are no royal roads in mathematics.
- GregarianChild 2y ago
  If you understand the STLC (= simply typed lambda calculus) and why it is also a HOL (= higher-order logic) then you understand most of topoi already (although the match is not perfect). Topos theory is a branch of mathematics which applies what programmers would call an aggressive refactoring to the category of sets and functions - a foundational workspace within which almost all of conventional math is conducted (whether the practitioners realise it or not). Math is refactored in a way reminiscent of how HOL refactors math (but constructively). Set theory is a legacy platform like MS-DOS (!) with many limitations and anomalies which topos theory can explain and perhaps alleviate. A topos is a "virtual machine, for math ... Definitions, constructions, theorems "run" in a topos just as apps run on a VM, or SQL statements run on a database. The promise of topos theory is to cleanly separate language from implementation (just as webdesigners separate HTML from business logic) A lot of math can easily be "refactored" to apply in a much wider context. The steps in building this refactoring are: • Define the concept of category, a workspace of dots and composable arrows between them • Identify the category Sets as fundamental • Abstract out the operations and laws that make Sets useful (think CCCs (= cartesian closed categories) with some extras) • Axiomatise a topos as a category equipped with operations obeying these laws • Find other naturally occurring examples of topoi • Via internal categories, understand topoi as a complete foundation for math • Specify a language for describing constructions and deductions in a topos Note, if you don't care about foundations, then topos theory gives you nothing new, except labour of re-learning what you already know in a new form that is awkward if you heavily rely on non-constructive reasoning.
  - auggierose 2y ago
    I understand HOL, because it is just sorted first-order logic. I also care about foundations, which is why I need to understand what a topos exactly is. So, it seems that the steps you describe, until and including "Find other naturally occuring examples of topoi" can all be done in first-order logic set theory, is that right? ps: for people saying topoi, do you also say thermoi as a plural for thermos?
    - deleted 2y ago
      [deleted]
- jesuslop 2y ago
  Yep an elementary ("Lawvere-Tierney") topos is crafted to be just first order logic. 100% standrad FOL, as Category Theory is. An elementary topos is a cartesian closed category, with finite limits and a subojbect classifier. Cartesian closedness means that for objects A and B there is an exponential object A^B of functions from B to A. Cartesian closedness is the right intuition on functions being first class citizens and is at the center of the equivalence CCC-lambda calculus-functional programming. Limits are bread and butter categorical stuff, and the pesky subobject classifier is sort of a pain of what Category Theory understands as classifying things. In Set, monos into X (inyections into X, subsets of X), determine the characteristic function of the subset, subset of say, U. The characteristic function is U->Bool={True, False}. Summing up, the subobject classifier in Set is Bool and provides the correspondence of functions U->X and X->Bool. In an arbitrary elementary topos, the subobject classifier would be an Ω such that monic arrows ?->X corresponds to arrows X->Ω. I would agree that this has bad digestion, maybe delving in applications one just grow accustomed. There is an idea of one doing mathematics in an "ambient" set theory, and categorists want to look at that as an ambient category of sets. But then they asked, what are the miminum features I am really using of this ambient category of sets? The list is the requirements of a category to be an elementary topos. So the category of sets is a topos (the topos of sets) very by design. But other categories also do. When one changes Sets to other topos is when weird intepretations emerge. Topos requirements don't let you recover the axiom of choice, for instance. Excluded middle is not available anymore.
  - auggierose 2y ago
    Ok, thank you. I think I will just have to sit down and write up what these conditions mean explicitly as axioms in my logic. In general I feel category theory is a somewhat clumsy way of encoding higher-order things in a first-order way, but on the other hand I think the various type theories are not the right way to declumsify this. But that's just an impression, hopefully I will know more soon.

auggierose 2y ago

I've seen toposes declared as some fundamental notion, and I'd very much like to understand them. Is there a short definition somewhere out there of what a topos is in terms of first-order predicate logic? Something I can understand without reading through 200 pages of preliminary material first? I've seen statements that such a formulation in first-order logic would be misguided, because category theorists have their own notion of logic, but I'd like to understand it using my own notion of logic first.

hackandthink 2y ago
Makkai's work my fit: "First Order Logic with Dependent Sorts,with Applications to Category Theory" "For instance, the definition of elementary topos (with operations defined by universal properties up to isomorphism, not specified as univalued operations) can be given as a finite set of sentences in FOLDS." https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf
- auggierose 2y ago
  Interesting find, but again an example of where you first need to learn some new logic FOLDS ("FOLDS has the first two of these, contexts and types (although the latter are called 'sorts'), but it does not have the third, terms (except in the rudimentary form of mere variables), and it has equality in a greatly restricted form only."). I wonder if it is impossible to describe a topos as a normal axiom system of first-order logic, or if people are just unwilling to do it.
soist 2y ago
The logic of toposes is higher order intuitionistic logic. The logic of higher toposes is presumed to be intensional dependent type theory. The best introduction to these logics is probably the homotopy type theory book.
- auggierose 2y ago
  I cannot understand the homotopy type theory book. It just makes no sense to me, sorry. > The logic of toposes is higher order intuitionistic logic. Yes, I have read that a lot. Eventually, I would like to understand how toposes form a model of higher-order intuitionistic logic (which is what "The logic of toposes is higher order intuitionistic logic" probably means?). But first, I would like to understand what a topos is in first-order logic terms. You know, baby steps.
  - soist 2y ago
    The category of sets is a topos and can be expressed/presented with first order classical logic but the general logic of toposes is intuitionistic and non-classical. There is no single topos with a single logic, each topos has its own logic and the common thread is that they're non-classical and higher order.
    - auggierose 2y ago
      So are you saying that "T is a topos" cannot be expressed via first-order classical logic? Unlike something such as "G is a group", or "T is a topology" or "C is a category"?
      - soist 2y ago
        None of your examples are expressible in first order logic either. Those are all instances of mathematical structures which can be formalized in different toposes with different logics. Groups in the topos of sets are different from groups in the topos of smooth sets. The structure of a group can be expressed as a diagram which can then be interpreted in any topos with the prerequisite mathematical structures. Toposes have products (finite limits) so every topos can potentially have group objects just like every topos can have a natural number object which is an initial algebra (colimit) for a certain diagram. In any case, there is no royal road and if you're not willing to spend the time and effort to learn what others have written about toposes then there isn't much I can help you with here. There are no royal roads in mathematics.
GregarianChild 2y ago
If you understand the STLC (= simply typed lambda calculus) and why it is also a HOL (= higher-order logic) then you understand most of topoi already (although the match is not perfect). Topos theory is a branch of mathematics which applies what programmers would call an aggressive refactoring to the category of sets and functions - a foundational workspace within which almost all of conventional math is conducted (whether the practitioners realise it or not). Math is refactored in a way reminiscent of how HOL refactors math (but constructively). Set theory is a legacy platform like MS-DOS (!) with many limitations and anomalies which topos theory can explain and perhaps alleviate. A topos is a "virtual machine, for math ... Definitions, constructions, theorems "run" in a topos just as apps run on a VM, or SQL statements run on a database. The promise of topos theory is to cleanly separate language from implementation (just as webdesigners separate HTML from business logic) A lot of math can easily be "refactored" to apply in a much wider context. The steps in building this refactoring are: • Define the concept of category, a workspace of dots and composable arrows between them • Identify the category Sets as fundamental • Abstract out the operations and laws that make Sets useful (think CCCs (= cartesian closed categories) with some extras) • Axiomatise a topos as a category equipped with operations obeying these laws • Find other naturally occurring examples of topoi • Via internal categories, understand topoi as a complete foundation for math • Specify a language for describing constructions and deductions in a topos Note, if you don't care about foundations, then topos theory gives you nothing new, except labour of re-learning what you already know in a new form that is awkward if you heavily rely on non-constructive reasoning.
- auggierose 2y ago
  I understand HOL, because it is just sorted first-order logic. I also care about foundations, which is why I need to understand what a topos exactly is. So, it seems that the steps you describe, until and including "Find other naturally occuring examples of topoi" can all be done in first-order logic set theory, is that right? ps: for people saying topoi, do you also say thermoi as a plural for thermos?
  - deleted 2y ago
    [deleted]
jesuslop 2y ago
Yep an elementary ("Lawvere-Tierney") topos is crafted to be just first order logic. 100% standrad FOL, as Category Theory is. An elementary topos is a cartesian closed category, with finite limits and a subojbect classifier. Cartesian closedness means that for objects A and B there is an exponential object A^B of functions from B to A. Cartesian closedness is the right intuition on functions being first class citizens and is at the center of the equivalence CCC-lambda calculus-functional programming. Limits are bread and butter categorical stuff, and the pesky subobject classifier is sort of a pain of what Category Theory understands as classifying things. In Set, monos into X (inyections into X, subsets of X), determine the characteristic function of the subset, subset of say, U. The characteristic function is U->Bool={True, False}. Summing up, the subobject classifier in Set is Bool and provides the correspondence of functions U->X and X->Bool. In an arbitrary elementary topos, the subobject classifier would be an Ω such that monic arrows ?->X corresponds to arrows X->Ω. I would agree that this has bad digestion, maybe delving in applications one just grow accustomed. There is an idea of one doing mathematics in an "ambient" set theory, and categorists want to look at that as an ambient category of sets. But then they asked, what are the miminum features I am really using of this ambient category of sets? The list is the requirements of a category to be an elementary topos. So the category of sets is a topos (the topos of sets) very by design. But other categories also do. When one changes Sets to other topos is when weird intepretations emerge. Topos requirements don't let you recover the axiom of choice, for instance. Excluded middle is not available anymore.
- auggierose 2y ago
  Ok, thank you. I think I will just have to sit down and write up what these conditions mean explicitly as axioms in my logic. In general I feel category theory is a somewhat clumsy way of encoding higher-order things in a first-order way, but on the other hand I think the various type theories are not the right way to declumsify this. But that's just an impression, hopefully I will know more soon.