Maybe yes. I see sheaves as a comma category, basically.

OK

I know Coq. And I know type theory because it's the logic implemented in coq. And type theory is the internal logic of a topos. I read some books about category theory, because it's important for computer science. — Mephist

Thank you. That's what I suspected. It's a particular point of view. There is a much larger mathematical context in which these ideas developed, that you're not aware of. These ideas date from the 1930's and 40's. The CS people have discovered it recently and it's like a new toy. I have to admit I have spoken to other constructivists who learned math from Coq. Or was that you, a couple of months ago on this site.

So this is frustrating for me now, and probably for you.

OK, I'll drop this topic. Probably nobody is interested... :sad:

Maybe yes. I see sheaves as a comma category, basically. — Mephist

If you know the categorical definition of something but you can't explain the bottom-up concept, you should fill in the blanks in your knowledge. The math you don't know, is why you can't explain this stuff to me. Like I said I did some heavy sheaf-theoretic lifting last night and still can't understand you. We're working different sides of the street.

Can you give me some references?

OK, I'll drop this topic. Probably nobody is interested.. — Mephist

No not at all. I'm vitally interested. I wonder if you'd be willing to meet me halfway; and realize that what you've learned in the abstract does not constitute knowing a lot about math. You know categorical logic. That's not the same thing.

Well, OK, but I don't know which point is the halfway...

Can you give me some references? — Mephist

The Wiki page gives some clues as to the difficulties ahead.

https://en.wikipedia.org/wiki/Sheaf_(mathematics)

This is helpful:

https://math.stackexchange.com/questions/2642231/what-is-an-intuitive-concise-explanation-of-a-sheaf

I've been looking at these two pdfs:

https://mast.queensu.ca/~andrew/teaching/math942/pdf/2chapter1.pdf

https://tlovering.files.wordpress.com/2011/04/sheaftheory.pdf

I'm not saying you need to know any of this. Just that ... I don't know. If you can go slower, define your terms, take things one step at a time, that would be helpful to me.

Well, OK, but I don't know which point is the halfway... — Mephist

I'd like to understand what you mean when you say Prop is a subobject classifier; given that all I know is that a subobject classifier is {T,F} in elementary logic or defining a subset of a set.

If you are talking about type theory, that won't be helpful to me.

Here's how to visualize it. You and I have almost disjoint backgrounds in math. From the point of view of math, categorical logic is off to the side somewhere. Mostly of interest to the computer scientists these days and not mathematicians. I think that if you could explain your concepts to me, you'd understand them better yourself. A sheaf, for example is defined only on the open sets of a manifold. So my example earlier of $f(x) = x^2$ is a little off. I was taking the fibers over the points; but sheaves are defined only over open sets. That's something I'm confused about at the moment.

It must be interesting to understand all of what you know, but without any of the mathematical context. Pretty abstract but perhaps this is just a matter of modern conventions versus classical. I know a little category theory but my brain's not hardwired for it as it is for people learning their math from a categorical perspective to start with.

So that's the explanatory gap. But it's not hopeless. You said that a proof is a section of a fiber bundle made up of propositions, or something like that. I believe it's possible for me to understand this in terms of things I know. Tell me what space we're working in. Define some terms clearly. This can be done. And tell me why Prop is a subobject classifier. In what was is a set or category or type of proposition, analogous to {T,F}?

I'd like to understand what you mean when you say Prop is a subobject classifier; given that all I know is that a subobject classifier is {T,F} in elementary logic or defining a subset of a set. — fishfry

A subobject classifier is a pair of an object and an arrow {Omega, "true": T->Omega} with the following property: every monomorphism m: A->B in the category (in the topos) is the pullback of the morphism "true" along a unique morphism x:B->Omega. It is isomorphic to a set with two elements in the category of sets (that is a topos), but not in all topoi.

A sheaf, for example is defined only on the open sets of a manifold — fishfry

A sheaf, for example is defined only on the open sets of a manifold — fishfry

You don't need a manifold, you need only a topological space. A manifold is a topological space plus an atlas of continuous maps, right?

I was taking the fibers over the points; but sheaves are defined only over open sets. That's something I'm confused about at the moment. — fishfry

Yes, that's the central point of the whole story: open sets are "more important" than points. In the category of sets an object is "made of" points, but in a generic topos this is not the case. In a topos, a point (of an object X) is an arrow from the terminal object to X. In the category of sets the terminal object is the singleton set and the set of arrows from the terminal object to X is isomorphic to the set of points contained in X, but this is not true in general for a topos.

P.S. I think I know what's the main reason of confusion: you are talking about a sheaf in the category of sets (no category theory needed: only topological spaces defined in set theory), an I am talking about a sheaf defined on a generic topos (category theory needed, set theory irrelevant)

Yes, that's the central point of the whole story: open sets are "more important" than points. — Mephist

Ok. Consider this. Earlier I gave the example of the ring of continuous functions on $\mathbb R$, and the fact that the zero-set of a point is an ideal. And you responded by saying that's a fiber. Which I think it is.

But it's not actually a good example of a sheaf, because sheaves are only defined on open sets. So now you are saying, "Oh yeah it's about open sets," but earlier you didn't remember that you know that, and you were seduced by my example and didn't realize it was inaccurate.

Likewise my example of the inverse images of $f(x) = x^2$. I made the same error, taking inverse images of points. I think in differential geometry that's ok. But frankly I don't know much differential geometry either. My mathematical ignorance is vast.

That's what I mean by mathematical context. You are not being precise enough in your formulations, and that's making it harder for me to latch on to the ideas. So should I be thinking of a manifold with charts? Is the atlas the fiber bundle? I have no idea.

Re comma categories. I checked out a pdf book on categorical logic. In the table of contents they get to comma categories right away. In mathematically oriented category theory books, they get to them much later, and I have read the definition once but didn't understand enough to remember it.

In general, categorical logic seems to be taking a huge leap that bypasses several years of serious math study. So as I say, our knowledge is virtually disjoint. But a bridge can be built I'm sure.

By the way, I saw an Awodey video. I started to read his book but it was too oriented to logic for my taste so I spend more time looking at Leinster. So you see even by inclination I have remained ignorant of categorical logic. I'm trying to work my way up from the example of the ideals of continuous functions defined on open sets, not zero sets of points. That I believe is accurate. Now how do I shoehorn logic into that?

A subobject classifier is a pair of an object and an arrow {Omega, "true": T->Omega} with the following property: every monomorphism m: A->B in the category (in the topos) is the pullback of the morphism "true" along a unique morphism x:B->Omega. — Mephist

That is a brilliant explanation. Totally lost on me.

I explained that what I know about subobject classifiers is this:

* {0,1} is a subobject classifier. That means if I have a set, say, I can define a subset by its characteristic function. That is, the function that maps the elements of the subset to 1 and everything in its complement to 0.

* In general you can use any interesting set as a subobject classifier, generalizing true and false.

* I can imagine that if we had a collection of propositions, and the {0,1} set, we could label propositions true or false.

Now that is what I know. Why don't you start from there.

By the way, when you quote chapter and verse of the technical definition of subobject classifier but don't say a word about what it means; is it because you don't relate to the meaning in some way? Or think the meaning is obvious from the jargon? Or know the words but not the meaning? Or think too much of my knowledge of category theory? I could unpack that definition if I wanted to. I know that much. But I'd have to work at it, and in the end I still wouldn't know what's a subobject classifier. I need to know how you are shoehorning logic into sections and fibers.

Please tell me if I'm being rude. Your communication style is very ... confusing to me. You lay down that paragraph as if you think you answered my question. You didn't. That's the mystery I want to clear up. Maybe it's just a style. You have all the textbook defs memorized but you are not telling me what they mean or what the ideas are.

but earlier you didn't remember that you know that, and you were seduced by my example and didn't realize it was inaccurate — fishfry

It wasn't inaccurate, it was a particular case, as you usually do when you give an example..

That's what I mean by mathematical context. You are not being precise enough in your formulations, and that's making it harder for me to latch on to the ideas. — fishfry

Yes, but you can easily find the precise definitions on Wikipedia. I usually don't think in terms of precise definitions.

Re comma categories. Funny story. I checked out a pdf book on categorical logic. In the table of contents they get to comma categories right away. In mathematically oriented category theory books, they get to them much later, and I have read the definition once but didn't understand enough to remember it. — fishfry

That's the advantage of category theory in comparison with set theory: it's more general, but even more simple: it speaks only about the essential features that are needed for proofs to work, and ignore the particular "implementation" (sorry, again a computer-science term). You don't think about real numbers in terms of set-theory, right?

By the way, I saw an Awodey video. I started to read his book but it was too oriented to logic for my taste so I spend more time looking at Leinster. So you see even by inclination I have remained ignorant of categorical logic. But I see a thread. I know what right inverses are and that's basically fibers so I can get this. I just want to understand how that goes to propositions and proofs. — fishfry

OK. I have to go now..

That's the advantage of category theory in comparison with set theory: — Mephist

Yes but I haven't time right now to learn the category theory I'd need. I see a vertical thread of understanding from the idea of a fiber bundle over a manifold, to seeing how that idea generalizes to logic. You've pointed me in that direction several times. So it's not a matter of convincing me that your way is better. The only question is whether you want to explain this to me so I can understand it. I'm pretty close. Tell me the topological space, tell me the map from the open sets to some collection of algebraic structures, that represent propositions and proofs.

Right? A sheaf assigns to each open set of a topolgoical space, a data structure or algebraic object. Tell me the topological space, tell me the map, tell me which structures, represent propositions and proofs. I think that's a specific question we can meet halfway on.

I daresay one could put in a word for set theory as an antidote to too much abstract thinking! :-)

OK. I have to go now.. — Mephist

Time for bed here too. I feel hopeful because I just articulated a very specific mathematical goal we can achieve. Top space, mapping, algebraic objects or data structures being attached to the open sets. That will clarify a lot of things for me.

Yes but I haven't time right now to learn the category theory I'd need. I see a vertical thread of understanding from the idea of a fiber bundle over a manifold, to seeing how that idea generalizes to logic. You've pointed me in that direction several times. So it's not a matter of convincing me that your way is better. The only question is whether you want to explain this to me so I can understand it. I'm pretty close. Tell me the topological space, tell me the map from the open sets to some collection of algebraic structures, that represent propositions and proofs.

Right? A sheaf assigns to each open set of a topolgoical space, a data structure or algebraic object. Tell me the topological space, tell me the map, tell me which structures, represent propositions and proofs. I think that's a specific question we can meet halfway on. — fishfry

Hmm... :chin: You want a topological space for classical logic. OK, a topological space is a set of all subsets of an "universal" set.
- The elements of the universal set are tuples of elements of our model (the things that we are speaking about: real numbers, for example).
- The subsets are our propositions: they represent the set of all tuples of elements for which the proposition is true (an example here: the proposition "3x + y = 6" is the set of (x,y) such that the equation is true).
- Inclusion between the subsets represents implication.
- Functions are represented in set theory as particular sets of pairs (surely I don't have to explain this to you).
- Relations are sets tuples of elements of our domain.
- There are some distinct points that correspond to the constants of the language.
- The set operations of Intersection, Union and Complement form a Boolean algebra on the subsets of the topology. ( no problem until here, I hope ).

Only in this case, what for is a topology needed? All subsets of this topology are both open and closed. This is a discrete topology (the most particular case of all).

And then the main problem: what about quantifiers? (forall and exists).
You don't want category theory, right? The quantifiers are naturally defined as adjoint functors in category theory, but you said you want only set theory. :roll: so I should reformulate the condition of adjunction of categories in terms of set theory... at first sight it will be a definition that will have to include in itself the algebraic structure of... a category! ( I don't know how to do this :gasp: )
P.S. of course you cannot allow infinite expressions (such as "forall" is an infinite intersection...), since our language is made of strings of symbols.

And then the subobject classifier is the usual set {"true", "false"} plus an evaluation function that for each proposition (subset) returns a value of the set {"true", "false"}

What about sheaves? In this case sheaves are unnecessary too, because we are in a discrete topological space.. I don't know if this program would bring some useful insight really, even if I am able to figure out how to find an algebraic structure on our "topological space" that includes quantifiers :sad:

I need at least the category of sets to be able to include logic, but sheaves are not really related to boolean logic, for what I know.

P.S. I forgot about proofs. Proofs in standard logic are not objects of the model (sets in our case), but it's only a partial order relation between our propositions determined by the rules of logic. Different situation in type theory, where they are represented as objects of our category - meaning: you cannot speak about proofs in standard logic; instead, you can speak about proofs in dependent type theory. And that's why the subobject classifier is not a simple set of values: you have to say not only if a proposition is true or false, but even what is it's proof.

Certainly some sort of goals, but not necessarily physical ends. To a large extent it's curiosity about "what comes next?" — jgill

Suppose we distinguish between "what comes next" in the physical world, meaning what happens in the next moment of time, and "what comes next" when you're counting 1,2,3,4,5..., meaning "6" is what comes next. The latter is really just a form of the former, you saying "six" is just an instance of what happens next in the physical world. One could argue that there are differences between natural, and artificial, in what comes next in the physical world due to intention and free will. But if such a difference is a real difference, we would have to validate the reality of the difference through some dualist principle like "the soul", which reaches in from some non-physical world to interfere with "what happens next" in the physical world. Otherwise "ends' are nothing other than physical ends.

So Platonism comes back on us, as 'the good", meaning what is intended, striven for. If we situate this "object", the end, the goal, in the non-physical, such that "what comes next" is a creation from the non-physical, rather than a natural process, then we cannot avoid dualism. However, we must maintain respect for the fact that the natural physical world imposes restrictions on what is possible, as a goal, object, or end. So for instance, the idea of "infinite possibility" is really an impossibility, due to those restrictions, and is therefore a contradictory idea. One might define "possibility" as a sort of logical possibility to avoid such a contradiction, but since what is possible and what is impossible is ultimately dictated by the physical circumstances, such a move would be an act of self-deception, telling yourself that "logical possibility" is not limited by "physical possibility'.

Or do you mean that the use of irrational numbers is conceptually inaccurate with respect to a first-principles analysis of physics? If the latter, as I said, I don't think that it matters for mathematics. — simeonz

I think that this is the more accurate representation of what I was saying. I don't agree with your conclusion though, because it requires that we make a complete separation between physics and mathematics. Suppose we assume such a separation. Mathematicians just dream up their axioms and principles for no apparent reasons, just because they are beautiful or something, so that the mathematical principles are somewhat arbitrary in this way, pure mind art. They leave these principles lying out there, and the physicists pick and choose which ones they want to use. It's like a smorgasbord of tools lying on the table, which the physicists can choose from. That's a fine start, but we must respect the fact that the process is reciprocal. So once the physicists choose their preferred tools, and start using them, then these are the principles that the mathematicians are going to concentrate on improving and fine tuning. Evidence of this is the fact that the real numbers came from the use of rational numbers, and the use of geometrical principles which created irrational numbers. Mathematicians did not have to allow irrationals into their numerical principles, but they were being used, so the mathematicians felt compelled to incorporate them . Therefore I think it is incorrect for you to say that a first principles analysis of physics is irrelevant to mathematics. .

I think that this is the more accurate representation of what I was saying. — Metaphysician Undercover

I will then answer under the assumption that we are not questioning the efficiency of algebraic numbers as they are used in the design and analysis of numerical algorithms for daily and industrial use.

I don't agree with your conclusion though, because it requires that we make a complete separation between physics and mathematics. Suppose we assume such a separation. Mathematicians just dream up their axioms and principles for no apparent reasons, just because they are beautiful or something, so that the mathematical principles are somewhat arbitrary in this way, pure mind art. — Metaphysician Undercover

I am not saying that it necessarily has to be pure mind art, but it wouldn't change the assessment we make of the final product. Even if our improvements in the scientific method (the philosophy of mathematics) remove obstacles to its continuous development, it should not come at the cost of the numerical properties of the prescribed computations. Just as long as the scientific method produces a framework of computations and analysis for our varied conventional applications that conserves the known accuracy-complexity tradeoff, the improvement can venture in any desired direction. But exploring concepts and algorithms of computations whose conventional (daily and industrial) utility is inferior to the ones currently in use is not an option, no matter what methodological grounds we have for that.

They leave these principles lying out there, and the physicists pick and choose which ones they want to use. It's like a smorgasbord of tools lying on the table, which the physicists can choose from. That's a fine start, but we must respect the fact that the process is reciprocal. So once the physicists choose their preferred tools, and start using them, then these are the principles that the mathematicians are going to concentrate on improving and fine tuning. — Metaphysician Undercover

This is true. But mathematics is not focused only on fundamental physics. It serves economics, construction engineering, software design and electronics, government, etc. All those fields are served on equal footing by mathematics. Physics is undoubtedly the most fundamental of sciences. But that does not mean that mathematics is physics oriented. It serves any situation involving computing and conceptualizes theories that unify as many applications as feasible. If a given field requires specific axiomatic framework, it needs to engage the mathematical community deliberately and the other fields do not have to be impacted.

Evidence of this is the fact that the real numbers came from the use of rational numbers, and the use of geometrical principles which created irrational numbers. — Metaphysician Undercover

Yes, but this happened in times when people believed the earth was flat. How irrational numbers were originally conceived is irrelevant to their contemporary meaning.

Mathematicians did not have to allow irrationals into their numerical principles, but they were being used, so the mathematicians felt compelled to incorporate them . — Metaphysician Undercover

The way I interpret irrational numbers today is as a property of the process you use to compute approximate quantity when a diagonal, perimeter, the intersections, etc, of various objects of various shapes are involved. The question is not what best explains the underlying physics, but how can we compute economically and socially interesting factors - the amount of material necessary to manufacture a part in the desired shape, the heat transfer occurring at the surface of a container, the sliding resistance a material with a given shape has, etc. We are not investigating the underlying physics, or trying to achieve precision in excess of what we need, but merely seek an efficient method for computing values within the desired accuracy. Irrational numbers are our "design" of this method, not our "interpretation" of the objects involved. We can still investigate the physical fundamentals, but this is not a concern for our procedures.

Hmm... :chin: You want a topological space for classical logic. OK, a topological space is a set of all subsets of an "universal" set.
- The elements of the universal set are tuples of elements of our model (the things that we are speaking about: real numbers, for example).
- The subsets are our propositions: they represent the set of all tuples of elements for which the proposition is true (an example here: the proposition "3x + y = 6" is the set of (x,y) such that the equation is true).
- Inclusion between the subsets represents implication.
- Functions are represented in set theory as particular sets of pairs (surely I don't have to explain this to you).
- Relations are sets tuples of elements of our domain.
- There are some distinct points that correspond to the constants of the language.
- The set operations of Intersection, Union and Complement form a Boolean algebra on the subsets of the topology. ( no problem until here, I hope ). — Mephist

I have many questions. Let me first say exactly where I'm coming from, and what I'd eventually like to understand.

You said a while back, in a remark that started this convo, that you can do logic in a topos. I'm curious to understand that in straightforward terms. It doesn't seem that difficult once you know how the mathematical structures are set up.

So we start at Wiik:

In mathematics, a topos (UK: /ˈtɒpɒs/, US: /ˈtoʊpoʊs, ˈtoʊpɒs/; plural topoi /ˈtoʊpɔɪ/ or /ˈtɒpɔɪ/, or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much like the category of sets and possess a notion of localization; they are a direct generalization of point-set topology.

Ok. So I need to find out what a category of sheaves of sets on a topological space is. But it can't be too complicated, because "Topoi behave much like the category of sets" and of course I happen to know a lot about the category of sets. So let's go read up on sheaves.

Wikipedia has a decent article but I find this Stackexchange quote very simple and clear:

A sheaf on a topological space is something that associates to every open set an object F( ), e.g. an abelian group. Elements of F( ) are usually called sections on U.

It's ok if this isn't fully general or there are various other ways of looking at it. What we're trying to do is simply begin the process of developing some intuition about the subject.

So now you tell me you can use a topos to do logic. Of course I'm perfectly well aware this is true, but what I'm looking for is a straightforward exposition of how you tie your ideas to these definitions.

So, if a topos is like a category of sheaves, you must have some sheaves lying around. So what is the underlying set, what is its topology, what algebraic or other objects are being associated with open sets, and what is the mapping?

You say it's the discrete topology but you didn't convince me. Let me make some specific points.

Hmm... :chin: You want a topological space for classical logic. OK, a topological space is a set of all subsets of an "universal" set. — Mephist

There is no universal set, so this needs clarification.

- The elements of the universal set are tuples of elements of our model (the things that we are speaking about: real numbers, for example). — Mephist

Oh ok you are using "universal set" to mean the universe of discourse or the base set. Ok. So you have a set, which consists of tuples of elements. 1-typles, 2-tuples, 3-tuples? Need to be specific so I know what this set is.

But since we want to be able to do n-ary predicates in logic, maybe you want all possible finite n-tuples. So we have a set, let's call it $S = \mathbb R \cup \mathbb R^2 \cup \mathbb R^3 \cup \dots$. That ok with you? It's all the 1-, 2-, 3-, etc. tuples of real numbers.

- The subsets are our propositions: they represent the set of all tuples of elements for which the proposition is true (an example here: the proposition "3x + y = 6" is the set of (x,y) such that the equation is true). — Mephist

Ok. Interesting. Question. How do you know what the propositions are? Suppose I have the subset {(1), (2), (3)} where those are three 1-tuples. What proposition is that the answer to? There are infinitely many for each tuple I'd think. For example "x = 1 or x = 2 or x = 3" is one such proposition: and "x is an integer strictly between 0 and 4" is another.

Also I think you have a "type error" in the sense that if you have a subset {(12), (3, 4, 5)} then you are conflating binary propositions with ternary ones. Does that cause trouble? Is this the model you are intending to communicate here?

- Inclusion between the subsets represents implication.
- Functions are represented in set theory as particular sets of pairs (surely I don't have to explain this to you).
- Relations are sets tuples of elements of our domain.
- There are some distinct points that correspond to the constants of the language.
- The set operations of Intersection, Union and Complement form a Boolean algebra on the subsets of the topology. ( no problem until here, I hope ).[/quote]

Ok. So you give the set of tuples the discrete topology, so that all sets are open. And to each set, you assign ... what was it you assign? Did you say?

Only in this case, what for is a topology needed? All subsets of this topology are both open and closed. This is a discrete topology (the most particular case of all). — Mephist

We need a topology because that's how we define a sheaf; and a topos is "category that behaves like the category of sheaves of sets on a topological space." In the end I need to understand this example in terms of the definitions of topos and sheaf. This is my mission.

And then the main problem: what about quantifiers? (forall and exists).
You don't want category theory, right? The quantifiers are naturally defined as adjoint functors in category theory, but you said you want only set theory. :roll: so I should reformulate the condition of adjunction of categories in terms of set theory... at first sight it will be a definition that will have to include in itself the algebraic structure of... a category! ( I don't know how to do this :gasp: ) — Mephist

I'm not asking you to explain adjoint functors. I just want the broad outlines first of the sheaves involved and how topoi are "like" sheaves and what that means. You have the discrete topology on the set of all n-tuples of (say) real numbers; and a set of tuples represents (some, all, a random example of) the propositions that the subset satisfies. Modulo the confusion of 2-tuples and 3-tuples in the same subset.

P.S. of course you cannot allow infinite expressions (such as "forall" is an infinite intersection...), since our language is made of strings of symbols. — Mephist

Ok.

And then the subobject classifier is the usual set {"true", "false"} plus an evaluation function that for each proposition (subset) returns a value of the set {"true", "false"} — Mephist

This is confusing. I believe that {T,F} is a subobject classifier, it's the only one I know. But then you say "for each proposition(subset)". I'm confused right there because subsets correspond to infinite collections of propositions. Are you perhaps equivalencing them? Or some other detail needs to be clarified?

What about sheaves? In this case sheaves are unnecessary too, because we are in a discrete topological space.. I don't know if this program would bring some useful insight really, even if I am able to figure out how to find an algebraic structure on our "topological space" that includes quantifiers :sad: — Mephist

Well, you said you can do logic in a topos. A topos is "like a category of sheaves," and a sheaf assigns algebraic objects to open sets of a topological space. So in order to make your exposition legitimate, you have to say how you are using the topos/sheaf model to represent propositions.

So far we've got the set of n-tuples and some questions. Progress.

I need at least the category of sets to be able to include logic, but sheaves are not really related to boolean logic, for what I know. — Mephist

Topoi are "like categories of sheaves" so if there aren't actually any sheaves around, maybe that should be clarified.

.S. I forgot about proofs. Proofs in standard logic are not objects of the model (sets in our case), but it's only a partial order relation between our propositions determined by the rules of logic. Different situation in type theory, where they are represented as objects of our category - meaning: you cannot speak about proofs in standard logic; instead, you can speak about proofs in dependent type theory. And that's why the subobject classifier is not a simple set of values: you have to say not only if a proposition is true or false, but even what is it's proof. — Mephist

Ok. I believe you are correct as far as it goes. I'm just trying to drill down these ideas to things I know. You said that proofs were fibers or sections or something like that; and that remark evokes manifold theory, and manifolds with charts seem like sheaves, to each open set you assign a copy of Euclidean space through a chart. So I believe there's an opportunity to flesh out this story from the bottom up as it were.

Discrete topology on the collection of n-tuples. So far that's what I've got, plus questions. But that's progress.

Mathematicians just dream up their axioms and principles for no apparent reasons, just because they are beautiful or something, so that the mathematical principles are somewhat arbitrary in this way, pure mind art. — Metaphysician Undercover

Lots of wiggle room in that "something." "Pure mind art" is good! :cool:

Mathematicians just dream up their axioms and principles for no apparent reasons, — Metaphysician Undercover

There are most definitely reasons. Penelope Maddy, the foremost authority on the philosophy of set theory, has a pair of papers, Believing the Axioms I and II, that describe the historical context and philosophical principles behind the adoption of the ZFC axioms. You might find these of interest.

https://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf

https://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms2.pdf

Lots of wiggle room in that "something." "Pure mind art" is good! :cool: — jgill

Sure, but the problem is that it does not actually exist as "pure mind art". The scientists, engineers, and others who use the mathematics force the existence of conventions which form the artist's medium. Then the mathematicians work with the existing conventions, and those conventions are a pollution to the notion of "pure mind art". Notice for example, that artists work with accepted (conventional) media, paint on canvas, music, etc.. The use of such conventions is a self-imposed restriction on the artistic expression, the artist chooses a medium. So if an artist chooses "mathematics" as a form of artistic expression, then by the very fact that it is mathematics and not some other art form which has been chosen, the artist has already restricted oneself to the use of certain principles, as the medium.

There are most definitely reasons. Penelope Maddy, the foremost authority on the philosophy of set theory, has a pair of papers, Believing the Axioms I and II, that describe the historical context and philosophical principles behind the adoption of the ZFC axioms. You might find these of interest. — fishfry

That's what I am arguing, there are always reasons for such choices. If we insist that a true relation between the axioms and the reality of the physical world is not necessary in such choices, then I believe we restrict our capacity to properly understand the reality of the physical world.

Thanks for the references, I'm going to try to read some of that material. it looks interesting.

The scientists, engineers, and others who use the mathematics force the existence of conventions which form the artist's medium. Then the mathematicians work with the existing conventions, and those conventions are a pollution to the notion of "pure mind art". — Metaphysician Undercover

"Conventions" ? Can you be more specific?

Although the physical sciences have influenced quite a bit of mathematics, the intervention in the artistic process of mathematics as a medium that necessarily pollutes "pure mind art" is debatable. How does pure mind art make it to the public domain? Must it always involve sculpturing with one's bare hands? Or painting with colored oils that are extracted from plants? Or wait, for a novelist, does it entail writing out one's work with a pencil?

You said a while back, in a remark that started this convo, that you can do logic in a topos. I'm curious to understand that in straightforward terms. It doesn't seem that difficult once you know how the mathematical structures are set up — fishfry

Here's the explanation in straightforward terms: a topos is an "extension" of the category of sets.
( probably it should have been called "setos" :grin: )
First of all, then, you have to know how you can do logic in the category of sets.

The category of sets is the category that has as objects ALL the sets and as arrows ALL the possible functions from any set to any set.

We just know how to do logic in ZFC set theory ( :confused: or should I start from the standard first order logic in ZFC? ), so we could do exactly the same thing here, but there is a problem: there are no "elements" inside an object ( the sets are represented by objects, but objects in category theory are a primitive notion: they are defined axiomatically, and not by describing how to build them starting from elements ).
However, there is a way to "represent" all the the logical operations of set theory ONLY in terms of the objects and arrows of a category. Here's the mapping:
- The empty set is represented by the initial object of the category
- The singleton set (all singleton sets are isomorphic, so there is only one singleton set, up to isomorphism) represented by the terminal object of the category
- An element of an object A is represented by an arrow from the terminal object to A.
- The the cartesian product of two objects A and B (the set of all ordered pairs of elements (a,b)) is represented by the categorical product of A and B
- The disjoint union of two objects A and B (the set that contains all the elements of A plus all the elements of B) is represented by the categorical coproduct of A and B
- The set of all functions from A to B is represented by the categorical exponential of A and B (notice that the set of all functions from A to {1,2} is isomorphic to the set of all subsets of A)
.....

There is a way to represent EVERY operation in set theory in terms of an universal property ( https://en.wikipedia.org/wiki/Universal_property ) in category theory, and the two representations work exactly in the same way... except for a detail: we cannot distinguish isomorphic sets between each-other. Meaning: we can distinguish them using the language of set theory (meaning: the set { {}, {{}} } is different from the set { {}. {{},{}} } in set theory, but in terms of universal properties, all sets that contain two elements are indistinguishable: you cannot even say how many two-element sets there are.
The arrows, instead, are assumed (by the axiomatic definition of a category) to be all distinguishable from each-other.

So, that's it! Category theory can be used to "represent" the operations used in ZFC set theory (except for this last limitation).

OK, so what for is the "topos"? The point is that WE DON'T WANT TO ALLOW THE USE OF EVERY POSSIBLE UNIVERSAL PROPERTY. We are looking for the MINIMAL SET OF UNIVERSAL PROPERTIES that are enough to be able to represent the operations used in set theory.

Well, it turns out that the minimal set is the following one:
(taken from Wikipedia: https://en.wikipedia.org/wiki/Topos )
"
A topos is a category that has the following two properties:

All limits taken over finite index categories exist.
Every object has a power object. This plays the role of the powerset in set theory.
"
There are a lot of equivalent definitions, but this is the simplest one that I found.
A topos is a category that contains the minimal set of universal properties necessary to encode all the operations required by the language of first order logic (including quantifiers).

Now, the most important point: the derivations that you can produce using this limited set of constructions are not all the derivations of classical logic. And you can build A LOT of different categories with the property of being a topos, by adding different requirements to the basic set of requirements called "topos".

At the same way, you can say that a given mathematical object is a "group" by giving the minimal set of operations and properties that a group must have (you have to be able to take inverses, to form products and to distinguish an element called "unit"), but then there are a lot of different additional requirements that you can add to restrict the set of mathematical objects that match your requirements.

Well, if you want to recover classical logic, you have to use a topos with the additional requirements:
- there are exactly two arrows from the terminal object to the subobject classifier
- there is an initial object (in general, by definition, there is no equivalence of empty set in a topos)
- ... I don't remember now .... Just look at the properties of the category of Sets here: https://ncatlab.org/nlab/show/Set

The category of Sets is the topos that has the additional properties required to make the logic work as the standard classical logic.

And that was only the first question :cry:

I don't think I have time for everything, but we'll see. Sheaves will be for the next time!

P.S. I re-read this and just realized that the correspondence between categories and logic theories that I described is not correct: here's the right correspondence: https://ncatlab.org/nlab/show/internal+logic (ZFC is not even in the list, but higher order logic can be used as an extension of ZFC where even iteration over subsets is allowed, and the corresponding category is called ELEMENTARY topos)

Conventions" ? Can you be more specific? — jgill

When numerous people use the same principle, it's a convention. So when we learn how to produce art, we are taught in the existing conventions. Do you not agree that to produce "pure art", "pure creativity", one would need to free oneself from the influence of such conventions?

Although the physical sciences have influenced quite a bit of mathematics, the intervention in the artistic process of mathematics as a medium that necessarily pollutes "pure mind art" is debatable. How does pure mind art make it to the public domain? Must it always involve sculpturing with one's bare hands? Or painting with colored oils that are extracted from plants? Or wait, for a novelist, does it entail writing out one's work with a pencil? — jgill

Yes, art always requires a medium, otherwise it cannot be in the public domain, just like communication requires a medium. If not for the medium it would just be ideas in someone's mind. So words and symbols are just another medium. And the accepted symbols and words form the conventions of mathematics. But symbols are not the only medium for mathematics. For example, many mathematical ideas are expressed as music, rhythm, harmony, etc.. This is a completely different way of expressing mathematical ideas, distinct from putting symbols and geometrical figures on paper. But music is a very adept way of demonstrating some principles of division. The medium being divided is a temporal medium. What we can observe, is that the principles for dividing a temporal medium are completely different from the principles for dividing a spatial medium. So these two distinct forms of division require distinct mathematical systems

However, there is a way to "represent" all the the logical operations of set theory ONLY in terms of the objects and arrows of a category — Mephist

OK, now I see a real "use" for category theory. Nice presentation.

For example, many mathematical ideas are expressed as music, rhythm, harmony, etc.. This is a completely different way of expressing mathematical ideas, distinct from putting symbols and geometrical figures on paper — Metaphysician Undercover

You don't use symbols to express music? Well, one can play an instrument by ear I suppose.

You don't use symbols to express music? Well, one can play an instrument by ear I suppose. — jgill

Right, the symbols simply facilitate understanding of the expression which is the music itself, allowing others to join in the expression. The artist produces the mathematical expression as a composition of music, the symbols are not the expression, but represent the expression. In more conventional "mathematical expressions", the symbols represent the mathematical ideas. In music, the music represents the mathematical ideas (dealing with temporal extension), and the symbols represent the music

Thank you for your reply. This post isn't nearly as long as it looks, most of it's your quoted text.

I have some specific comments, but first I want to say that I realize it may be an unreasonable expectation on my part to get the specific exposition I'm looking for.

On the other hand since last night I've been perusing a beautiful resource, Sheaves in Geometry and Logic by Saunders Mac Lane and leke Moerdijk, who isn't nearly as famous as Mac Lane. (Spelled with a space between Mac and Lane). Mac Lane invented category theory in the 1940's; and is very attuned to the philosophical implications of his work as well as being a brilliantly clear expositor.

Just reaing the first few pages of the Prologue, along with perusing the table of contents and some random reading, has given me a nice overview of categorical logic.

One thing that really got my attention was his presentation of a sheaf-theoretic version of Cohen's proof of the independence of the Continuum hypothesis. And his pointing out that Cohen's own proof, and his invention of the revolutionary method of forcing, is essentially sheaf-theoretic in nature. This was all a real revelation to me and gave me the high level view that I've been trying to get hold of. He pointed out that Cohen's approache relates to Kripke's work on intuitionist and model logic.

This all ties together a lot of amazing stuff. So Mac Lane made me a believer.

Unfortunately I still don't have the detailed technical example that I want to nail down; but perhaps that may have to wait.

Here is one really cool nugget that makes sense to me:

In a topological space the complement of an open set U is closed but not usually open, so among the open sets the "negation" of U should be the interior of its complement. This has the consequence that the double negation of U is not necessarily equal to U. Thus, as observed first by Stone and Tarski, the algebra of open sets is not Boolean, but instead follows the rules of the intuitionistic propositional calculus.

That is news I can use. It explains why if you consider the category of the open sets of a topological space, you get intuitionist set theory. That's the kind of insight I'm looking for. I never thought of it this way but now it's perfectly obvious. That's why I like reading Mac Lane. And that's only the prologue! The book is 629 pages. I imagine one could dive in and pretty much never come out, but be constantly enlightened on every page.

Now to your post.

Here's the explanation in straightforward terms: a topos is an "extension" of the category of sets.
( probably it should have been called "setos" :grin: ) — Mephist

My latest understanding is that a topos is like a generalize universe of sets. You can have one kind of universe or a different kind of universe depending on the rules you adopt, but all set-theoretic universes fit into the topos concept.

In fact the category of sets IS a topos. That's very helpful. Sometimes the simplest examples are the ones to start with.

First of all, then, you have to know how you can do logic in the category of sets. — Mephist

Ok but I fear you're going off on a theoretical tangent again. What I was hoping for was specific clarification on things you've said. You've said proofs and propositions are like fiber bundles or sections. And at one point you used the word "fibration," which is a very specific thing in topology. I was hoping you would either explain those remarks with laserlike clarity, as if you were writing an exam; or else agree that for whatever reason we can't do that.

Likewise you claimed that the collection of n-tuples of real numbers with the discrete topology can be associated with propositions. You have my attention with that example, I just need to see the rest of it.

I will say for the record that it's ok if I never get clarity on these things. I'm more than happy discovering Mac Lane's Sheaves book, so I got my money's worth from the convo.

The category of sets is the category that has as objects ALL the sets and as arrows ALL the possible functions from any set to any set. — Mephist

I've read different points of view. For example the question arises, is the category of sets the same as the proper class of all sets? Well, not exactly. I've heard it expressed that the category of sets has "as many sets as you need" for any given application. But it's not exactly synonymous with the class of all sets. That's my understanding, anyway.

We just know how to do logic in ZFC set theory ( :confused: or should I start from the standard first order logic in ZFC? ), so we could do exactly the same thing here, but there is a problem: there are no "elements" inside an object ( the sets are represented by objects, but objects in category theory are a primitive notion: they are defined axiomatically, and not by describing how to build them starting from elements ).
However, there is a way to "represent" all the the logical operations of set theory ONLY in terms of the objects and arrows of a category. Here's the mapping:
- The empty set is represented by the initial object of the category
- The singleton set (all singleton sets are isomorphic, so there is only one singleton set, up to isomorphism) represented by the terminal object of the category
- An element of an object A is represented by an arrow from the terminal object to A.
- The the cartesian product of two objects A and B (the set of all ordered pairs of elements (a,b)) is represented by the categorical product of A and B
- The disjoint union of two objects A and B (the set that contains all the elements of A plus all the elements of B) is represented by the categorical coproduct of A and B
- The set of all functions from A to B is represented by the categorical exponential of A and B (notice that the set of all functions from A to {1,2} is isomorphic to the set of all subsets of A)
.....

There is a way to represent EVERY operation in set theory in terms of an universal property ( https://en.wikipedia.org/wiki/Universal_property ) in category theory, and the two representations work exactly in the same way... except for a detail: we cannot distinguish isomorphic sets between each-other. Meaning: we can distinguish them using the language of set theory (meaning: the set { {}, {{}} } is different from the set { {}. {{},{}} } in set theory, but in terms of universal properties, all sets that contain two elements are indistinguishable: you cannot even say how many two-element sets there are.
The arrows, instead, are assumed (by the axiomatic definition of a category) to be all distinguishable from each-other. — Mephist

I already noted a few posts ago that I'm familiar with ECTS, Lawvere's elementary theory of the category of sets. So most of this I'm aware of.

So, that's it! Category theory can be used to "represent" the operations used in ZFC set theory (except for this last limitation). — Mephist

To be fair, that's not it. I feel like you didn't address my specific question or expand on your remarks about fiber bundles, fibrations, and the n-tuples of real numbers taken as synonymous with propositions. Those are the kind of "bread and butter" things I'm trying to understand. But like I say I'm perfectly ok with that, because I got my money's worth from discovering Mac Lane.

OK, so what for is the "topos"? The point is that WE DON'T WANT TO ALLOW THE USE OF EVERY POSSIBLE UNIVERSAL PROPERTY. We are looking for the MINIMAL SET OF UNIVERSAL PROPERTIES that are enough to be able to represent the operations used in set theory. — Mephist

Minimal set of universal properties. That might be over my head. I know what universal properties are in terms of defining things like free groups, tensor products, and the like. I'm ignorant of what it would mean to select for certain universal properties. Or I'm not understanding you.

Well, it turns out that the minimal set is the following one:
(taken from Wikipedia: https://en.wikipedia.org/wiki/Topos ) — Mephist

Ok. Not getting your point but it's on me to understand what you mean.

A topos is a category that has the following two properties:

All limits taken over finite index categories exist.
Every object has a power object. This plays the role of the powerset in set theory.
"
There are a lot of equivalent definitions, but this is the simplest one that I found.
A topos is a category that contains the minimal set of universal properties necessary to encode all the operations required by the language of first order logic (including quantifiers). — Mephist

Ok.

Now, the most important point: the derivations that you can produce using this limited set of constructions are not all the derivations of classical logic. And you can build A LOT of different categories with the property of being a topos, by adding different requirements to the basic set of requirements called "topos".

At the same way, you can say that a given mathematical object is a "group" by giving the minimal set of operations and properties that a group must have (you have to be able to take inverses, to form products and to distinguish an element called "unit"), but then there are a lot of different additional requirements that you can add to restrict the set of mathematical objects that match your requirements.

Well, if you want to recover classical logic, you have to use a topos with the additional requirements:
- there are exactly two arrows from the terminal object to the subobject classifier
- there is an initial object (in general, by definition, there is no equivalence of empty set in a topos)
- ... I don't remember now .... Just look at the properties of the category of Sets here: https://ncatlab.org/nlab/show/Set

The category of Sets is the topos that has the additional properties required to make the logic work as the standard classical logic.

And that was only the first question :cry:

I don't think I have time for everything, but we'll see. Sheaves will be for the next time!

P.S. I re-read this and just realized that the correspondence between categories and logic theories that I described is not correct: here's the right correspondence: https://ncatlab.org/nlab/show/internal+logic (ZFC is not even in the list, but higher order logic can be used as an extension of ZFC where even iteration over subsets is allowed, and the corresponding category is called ELEMENTARY topos) — Mephist

Ok. But just to save you some typing, I find that sometimes you tell me generalities about things I know, or that I consider tangential to the conversation, and we're missing each other that way.

And I think I'm winding down at my end because like I say, I think my expectation of clear answers to my questions might be unreasonable in this instance. I should just go read six hundred pages of Mac Lane, that would keep me out of trouble.

My latest understanding is that a topos is like a generalize universe of sets. You can have one kind of universe or a different kind of universe depending on the rules you adopt, but all set-theoretic universes fit into the topos concept.

In fact the category of sets IS a topos. That's very helpful. Sometimes the simplest examples are the ones to start with. — fishfry

Yes!

You've said proofs and propositions are like fiber bundles or sections. And at one point you used the word "fibration," which is a very specific thing in topology. I was hoping you would either explain those remarks with laserlike clarity, as if you were writing an exam; or else agree that for whatever reason we can't do that. — fishfry

Yes, but that correspondence is evident only in a dependent type theory, where you can make sense of the topology defined on your set of propositions (only open sets are propositions). In standard logic you cannot make sense of the topological structure of the space: no distinction between open and closed sets. All sets are both open and closed. That's the reason why taking the complement of the complement is an identity (boolean logic!). How can I show you the correspondence with dependent type theory without explaining dependent type theory?

Likewise you claimed that the collection of n-tuples of real numbers with the discrete topology can be associated with propositions. You have my attention with that example, I just need to see the rest of it. — fishfry

That's pretty standard old-fashioned model theory and first order logic (the topology is irrelevant: forget about open sets and take simply the set of all subsets of a given set R). I noticed that other people on this site were starting some kind of "introduction to first order logic" thing. Maybe they can help to make clear this part.

I've read different points of view. For example the question arises, is the category of sets the same as the proper class of all sets? Well, not exactly. I've heard it expressed that the category of sets has "as many sets as you need" for any given application. But it's not exactly synonymous with the class of all sets. That's my understanding, anyway. — fishfry

Yes, well, the point is that you cannot "count" the objects of a category. You cannot distinguish between isomorphic objects. There is no "equality" relation defined on the set of all objects. How can you decide what's the cardinality of the set of all objects if you cannot associate them with another set? (no one-to-one correspondence possible between elements. Only equivalence makes sense, not equality!)