Arghhh!!! :grimace: This is an example of intuitionistic dependently typed theory, corresponding to a non-trivial topological space. The previous one was an example of first order logic with set theory, since you didn't want type theory. And THERE IS NO NON-TRIVIAL TOPOLOGICAL SPACE CORRESPONDING TO FIRST ORDER LOGIC WITH SET THEORY. Than in that example, the topology was irrelevant! fdrake, did you understand?
If yes, can you please try to explain this in a better way? I don't even have much time for this, sorry. I have even to go to the hospital for a couple of days next week. — Mephist

I'm sorry to hear of your personal health issues.

Have you ever heard it said that if you can't explain something clearly, you don't actually understand it? That's the sense I get from your posts. I could be wrong. Hope your health issues turn out well.

The underlying set is the set of all propositions. The fibers are sets of elements of our model. — Mephist

Exactly not what you said the other day, when you started out by saying that the underlying set consisted of all n-tuples of real numbers then chose not to respond to any of my questions. That's why I"m trying to get you to nail down your definition. If you say you have a fiber bundle I'm entitled to ask what is the base set, what is the total space, what is the map? It's a perfectly sensible question.

Which model? You haven't said anything about models.

Is your previous claim now retracted and you are now making this different claim? The one with the clock?

This starts looking suspiciously like a correspondence is in play between the algebra of sets on the product topology of ×KΩ×KΩ, and the production rules on the propositional symbols. The possible "propositional assignments" that satisfy an interpretation maybe float above an interpretation as an algebra (algebraic structure, anyway).

Maybe it doesn't help though, it's very scattered. — fdrake

I haven't worked through this yet but it looks very promising.

OK, I understand what you want to do. But in the case of fiber bundles you don't define the topology of the total space in terms of the topology of the base space. You assume a preexisting topological space E (the total space), and a preexisting topological space B (the base space), and a continuous function P from E to B, and then you define the fibers as inverse images of P. — Mephist

Oh you DO know this material. It must just be your exposition that I can't understand. I'm happy to see this paragraph. I understand it, I agree with it, and I'm hopeful you'll frame the logic argument in terms like this. Maybe you already have. I'll work at this some more.

would the pre-image of any open set of ΩΩ with the discrete topology be a type, and thus a proposition? Or a collection of propositions which co-satisfy/are equivalent? — fdrake

EXACTLY a question I put to @Mephist the other night. That's identical to my understanding of what's being proposed, but I don't entirely believe it till I work through fiber bundles from the bottom up, which I'm working on. I'm gratified to find agreement on our interpretation of this idea.

The underlying set is the set of all propositions. The fibers are sets of elements of our model. — Mephist

I'm not sure I'm seeing that yet. I'm working on getting a bottom-up understanding of fiber bundles and this will take a couple of days or more for me to sort out a coherent argument. My general idea is to start with the Cartesian product of sets as an example of the fiber bundle idea; then work through the definition of a manifold, which (ignoring all the technical details) is an example of a Cartesian product. From there to sheaves is easy.

Now having laid out carefully a bottom-up understanding of fiber bundles, I'm going to want you to be very specific in putting your ideas in this context. I may or may not be successful in pulling this together because my knowledge of manifolds is weak but I think adequate to the task once I review some things.

Meanwhile I'll probably stay out of this for a while.

The underlying set is the set of all propositions. The fibers are sets of elements of our model. — Mephist

Honestly there's much less here than meets my eye, at least, from the standpoint of knowing what a fiber bundle is in topology. You are not making any connection with the fundamental definitions and you're not supplying the details. My wild-assed guess is that your Coq teacher mumbled something about fiber bundles and you haven't thought the details through. Is that uncharitable? If not, and you do know how to drill your idea down to the definition of a fiber bundle, let's just say I wish you'd work harder on exposition. Hopefully I'll pull my idea together and that will give us something specific to work with.

Did I say I hoped for this? — Noah Te Stroete

Perhaps nature will take care of it for us with a new type of plague — Noah Te Stroete

I'll quit while I'm behind here but this is what you wrote. You said "nature will take care of it," as if there's an "it" that billions of death would make better. I oppose that kind of radical environmental thinking. If you're not actively hoping for a plague then ok, I'll take you at your word. In my opinion plagues are bad things and never the solution to any problem we have.

I think you’re “literally” delusional. This from someone who gets accused of being delusional by many all the time mind you, so take anything I say as you wish. — Noah Te Stroete

I'm delusional to argue with environmentalists, you're right about that.

I'm all for clean air and water. I'm not for radical depopulation. I regard that as a sensible stance.

Nobody wants to see billions of people dying horrible, or even pleasant deaths. — Bitter Crank

At least one poster in the past hour did want exactly that. A plague.

If billions die, it won't be because environmentalists wanted that to happen. It will happen because the carrying capacity of the planet failed to produce enough of what the added billions of people need. It isn't in human hands! We will all be subject to nature's culling operation. It won't be just "those people" it will be "us people". — Bitter Crank

Malthus was wrong. Paul Erlich was wrong. You population pessimists never see that we crawled out of caves and built all this. I'd bet on humanity.

The Chinese program did work -- fewer children. The problem is that it produces a mushroom-shaped population distribution -- a large cap of elderly people supported on a narrow stem of working-age people, — Bitter Crank

That's exactly what I warned about when a poster suggested how nice it would be if we halved the world population. To do that you either kill the old or prevent the young from being born. If you do the latter, you end up with a planet of impoverished geezers. Since I'm getting old, I prefer not to consider the former.

The Chinese program was deliberate, but other countries have ended up with the same problem without imposing any such imitations. — Bitter Crank

Right. Most Western countries are not reproducing at replacement rate. Instead of staying barefoot and pregnant, women have careers and abortions. The result is an aging population with too few workers to support them.

It's just an unavoidable problem of shrinking populations. As young people become more affluent they have fewer children. That's all it takes. — Bitter Crank

Agreed. So must we make the problem worse by trying to halve the population by discouraging births or, as one poster just suggested, hoping for a plague to kill billions? This is what passes for liberal thought these days? I object.

Adaptations can be made. Many people work in jobs manufacturing superfluous products or providing services people can do without. Providing services to elderly people will have to become a more dominant paid job activity. — Bitter Crank

I'm sure the young of the world will gladly give up their hopes and aspirations to change the bedpans of the elderly. You sure you can get the kids to agree to this plan?

As for reducing excess population, nature will provide solutions as human capacity to deal with global crises decreases. Remember: Nature bats last. — Bitter Crank

Another anti-human. I hope you at least glanced at the two links I gave, and would consider the possibility that perhaps our problem, counterintuitive as it may seem, is actually underpopulation.

I'm so tired of hearing "caring" environmentalists long for mass death.

Perhaps nature will take care of it for us with a new type of plague. — Noah Te Stroete

Overpopulation is a myth. I hope you at least glanced at the two links I gave, which make the case that the real problem is underpopulation. You illustrate the problem I have with many environmentalists. You dream of billions of people dying a horrible death. The other poster wants the population halved in fifty years. Environmentalism is literally a death cult.

One woman, one child, half the population in 50-80 years. — Lif3r

I was prepared to apologize for misunderstanding your remark, but now I see that I have to reiterate my objection to your philosophy. The Chinese government had a one child policy for a long time and the result was a disaster.

It can be fairly argued that the biggest demographic problem is not too many people, but too few.

https://www.edge.org/response-detail/23722

https://www.cato.org/publications/commentary/reverse-handmaids-tale-just-horrifying-get-facts-straight-population-growth?gclid=EAIaIQobChMIsPG085WU5wIVdR-tBh1v1w7CEAAYAiAAEgJUYvD_BwE

If you didn't call for active murder, then I apologize for imputing that stance to you. But on your overall idea of a one-child policy and halving the world population. you could not be more wrong. My criticisms of radical environmentalism stand. Your "ideal" world of 50 years hence would consist of billions of old people with nobody to support them. Active extermination would be less cruel.

Part one: C is a category ( like A is an abelian group )
Part two: for each pair of objects of A, B there is a "product object" P ( like for each pair of elements (a,b) of A there is a product element: A is a ring ) ( omitting other needed properties, of course... )
Adding properties to the category I add structure! For example, each pair of objects has a product, the set of objects has to be infinite (pairs made of other pairs recursively). In general, without this requirement, a category may even be made of 3 objects and 4 arrows... — Mephist

ok

without this requirement, a category may even be made of 3 objects and 4 arrows... — Mephist

And why would that be a problem? A group is a category with one element.

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!) — Mephist

We're talking past each other. And this is not about cardinalities at all since neither proper classes nor categories (in general) have cardinalities. But I think between what you know and what you're able to explain, and what I know and what I'm able to understand of what you're saying, we have a gap that's not getting bridged.

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. — Mephist

This is not about introduction to first order logic. This is about an explanatory gap. The topology is not irrelevant if you claim to have a sheaf. Perhaps we're done.

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? — Mephist

Well, I know what a fiber bundle is so if you claim something is a fiber bundle you could just explain what it is that's the fiber bundle. What is the underlying set, what are the fibers above each point, etc. But maybe there's too much of an explanatory gap and we're at a point of diminishing returns.

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.

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

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.

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, 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.

If the past is infinite, then time has no beginning. If time has no beginning how can any point in the temporal sequence be attained? — TheMadFool

I don't think I can logically argue against strongly held metaphysical beliefs. Many people find it impossible to accept, even for sake of argument , that there was no first moment of time or first cause. For me, I find myself in 2020 and can clearly remember having once been in 2010. I got here just fine, took me ten years. I don't know how I got here. I was born and found myself at a certain point on the number line; and now lo these many years later, I'm in 2020. That's how it works.

How can you imagine that this somehow proves that causality had a beginning? You are here. That's a given. And later you'll be in the future, though when you get there it will feel like the present. You're just making metaphysical assumptions based on your Western upbringing. God was there "in the beginning." Buddhists don't believe that.

You're perfectly right that you can go as far as you like to the right on the number line and never reach the end, because there is no end. Likewise you can move as far as you like to the left, because there's no end in that direction either.

That's beautifully symmetric. Why do you think the past and the future are asymmetric? There's no evidence for it. Even if you take the big bang, I'll just consider an endless succession of big bangs. Nobody knows the truth about these things.

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}?

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.

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.

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.

Nat is the type of natural numbers. Types are represented by objects of the category, derivations are represented by the arrows. That's in the book from Awodey that you said you have read — Mephist

I don't know a freakin' thing about type theory. I think it's time to drop this.

Well, if you want the exact definition of sheaf I can copy it from the book on category theory that I posted you yesterday. I don't know all possible examples (algebraic structures) of sheaves, that's for sure! I was thinking that we were speaking about the relation between topology and logic. My background is mainly in logic and computer science. — Mephist

I get that. So when you use jargon from categorical logic you don't know the greater mathematical context; and that's making it harder for you to explain your ideas.

OK, fair point. Sorry for the intrusion! — Mephist

Thanks.

Let me just give you just some examples: "x >= 3" is a fibration from the object Nat to the subobject classifier Prop. — Mephist

As far as I know, Nat is a natural number category and not an object. Or maybe it's an object. Why don't you explain yourself more clearly. You jump in with jargon and frankly it makes me wonder how much you know. That's why I asked.

I really want to understand what you have to say, so I am not trying to give you a hard time. I'm asking you to write me some decent exposition. Start at the beginning.

* What's Nat?

* What is Prop? Is it the category of propositions? Is it an object in some other category? And in what way is it a subobject classifier, analogous to {T, F} in ordinary logic?

* What's a fibration? We've talked about fibers and sections and fiber bundles. I know about the Hopf fibration.

Can I ask your background again? Now I'm thinking that maybe you learned Coq but don't know the larger context of all these ideas. Or read a lot of Wiki pages. I don't mean to be provocative but in some vague way you are not convincing me that you know what you know.

I'm not saying that to give you a hard time. I'm saying that because I really want to understand what you're saying. If you tell me what you know and how you came to know this particular vertical slice of categorical logic, I can better understand where you're coming from.

I dumped on fishfry with my stupid mistake - really just an ignorant mistake - and he dumped back in language that reason forced me to accept - because I had added dumbness to ignorance. But I've been forgiven and I learned from someone who does indeed know what they're talking about. — tim wood

I appreciated your gracious response. In the end that was a productive interaction.

Sorry, I thought it was easier: I wanted to show you the complete structure of the category representing the proof of the proposition "2 > 0" derived from "forall x, s(x) > x" and "forall x, x > 0" but I didn't realize that it would take me ages to describe it in this way... and at the end it will be impossible to read. In Coq this is several lines of code, but is build automatically from a couple of commands. In reality, I never look at the real terms representing the proofs: they are built automatically. But I see that it would be a pain to build them by hand in this way! — Mephist

Yah.

I have to find a better way to give you a description of how it's made without writing all the details.. — Mephist

Exactly what I was thinking as I read your exposition.

You know you still haven't told me exactly how you came by all this information and it's relevant to our problem. I spent last night reading through a couple of technical introductions to sheaf theory and (a) it is mathematically sophisticated, and (b) not that easy to get hold of. One viewpoint is that a sheaf is an abstraction of the charts and atlases of a manifold. Also it's an abstraction of differential forms and exterior algebra. That's the differential geometry point of view. It's connected with cohomology, which is a complicated subject in higher algebra and algebraic topology. A sheaf is a very sophisticated mathematical object.

You seem kind of glib about what you know, without actually convincing me that you know the mathematical aspect of what's going on. That's why I asked about your background. You sound like you know stuff but at some level you haven't convinced me. Not that you don't know stuff, but that you don't know the larger mathematical context sufficiently well to explain it.

Does that make sense? That the explanatory gap is because you know the logic but not the math. That is the sense I'm getting. I just trying to understand why your attempts to explain this stuff to me are so frustratingly opaque at my end.

But there is a second possibility, that I guess it what TheMadFool had in mind: just consider a new set of numbers, made of all the real numbers plus the symbol ∞∞, and then postulate as an additional axiom for your numbers that 1/∞=01/∞=0 and 1/0=∞1/0=∞.
Why can't this be done? — Mephist

I will give my opinion. I don't think this is appropriate for this thread, because @TheMadFool wishes to understand the standard real numbers. What you wrote potentially confuses the issue. Hijacking this particular thread is inappropriate in my personal opinion. I am sensitive to this because I've worked hard to understand @TheMadFool's point of view, and give mathematically correct information in a way that seems to have been understood and well-received. You're just making my job harder and obfuscating the OP's new and hard won understanding for no good reason.

My two cents, thanks for listening.

You originally said there was a lot of overlap between Sanders and Trump supporters, so now I'm not sure what "the point" is because it seems to have changed. — Maw

I still believe that. You quoted me a poll to the contrary. I said that I nevertheless still hold my opinion.

The problem is the numbers, the carbon emissions would increase vastly if all those people had air conditioners, white goods, cars etc. — Punshhh

Well that's the argument right there. The first world says to the third world: We've got ours. You can't have yours. In fact you should die or not be born.

That is elitist environmentalism in a nutshell. As I say, I support a clean environment AND call out the selfish elitists who jet around telling the third world to stay where they are. You know there are populist movements all over the world right now. This is exactly why.

But my response was primarily to your second paragraph. Firstly that the changes will wreck western economies and that it is a small increase in temperature. — Punshhh

Without going into facts and figures (not my specialty on this issues, I don't follow environmental issues that closely) I stand by my opinions. Some of what I hear from the left these days is that they want to blow up our economic system because we only have 12 years to live because of climate change. A lot of serious people believe that. They're nuts.

6. Reductio ad absurdum. [1] is wrong. Time has a start — Devans99

I'm satisfied to agree to disagree.

According to a recent Emerson poll, only 4% of Bernie supporters will vote for Trump if Bernie doesn't get the election. Compare this with Buttigieg, Warren, and Biden at 12%, 10% and 9%, respectively. — Maw

That's a very interesting statistic. It's contrary to what I would guess. My sense is that if the DNC screws Bernie out of the nomination again (whether they did or didn't, the Bernie brigade believes they did) they will stay home in droves. That is my personal belief, polls notwithstanding. And for what it's worth, if 2016 taught us anything, it's that people no longer tell pollsters the truth; and that the respondents don't accurately represent the general population. It's not 1950 anymore when getting a phone call was a big deal and being asked your opinion by an authority figure an even bigger one. People are a lot more sophisticated now, not to mention cynical. We're all accustomed to random phone calls from scammers of all kinds. People don't even answer their phones anymore unless it's someone they know.

I say wait and see. Bernie is actually leading Biden in Iowa and New Hampshire. Just as Nancy Pelosi pulls him off the campaign trail to sit in Washington for the impeachment theater. Liz too. What a coincidence. Who could ever have seen that coming? Not Nancy, who stalled the process a month after telling us what an immediate emergency we were in.

Anyway, that's my opinion. The Bernie brigade played ball in 2016 but they won't play ball this time if, as is all but certain, the DNC screws Bernie. They don't want another 1972.

The question isn't whether they vote for Trump. They'll just stay home. Then your statistic would still be right yet miss the point. That pollster should have asked about the stay home factor.

Tulsi. You see what a dreamer I am. I also like Cory, even though he's out. Not his leftward-swerving self recently, but the centrist, business-oriented Democrat he's been for the 20 years BEFORE he decided to run for president. I always like him and thought he'd be a good president. His leftward move was perceived as inauthentic and that doomed his campaign.

Of the candidates with an actual shot: Biden, way too corrupt and represents everything wrong with DC. Wrong on every issue for the past 40 years. Drug warrior, supporter of the ruinous foreign wars. No Biden. Just no. He's Hillary 2.0. Liz, no. Mayor Pete, he's very likable, he might be the best of the bunch. I like Bernie's feistiness but I'm not a socialist. In fact the part of me that likes Bernie is the same part of me that likes Trump. Blow up the system because it ain't working. There's a lot of overlap between Bernie and Trump supporters.

To put this in context, I live in California which will go for whatever Dem gets nominated. So my vote doesn't count. I will be voting for Tulsi in the March primary as a show of support for the one genuinely anti-war Dem. And that vote won't matter either.

So, you can describe algebrically what is the intersection and the disjoint union of sets (as product and sum of objects), what is a subset, what is the powerset of a set (an exponential), etc.
The interesting part is that you can describe what are propositions and logical operators completely in terms of objects and arrows, only by assuming the existence of an object with some particular properties, called "subobject classifier". This is NOT the same thing as homotopy type theory, where you build a formal logic system in the usual way: by building strings of symbols with given rules. Here you describe logical operations and propositions in terms of universal mapping properties, as you do with operations between sets. The subobject classifier is the object that represents the "set of all the propositions", and the implications between these propositions are arrows that start and end in this object. Even the logical quantifiers forall and exists are only two particular arrows. Basically, everything is defined in terms of universal mapping properties.
I don't know which details should I add. What part of topos theory do you want me to explain? — Mephist

This is plenty for now! I understand parts of all that from various perspectives. One question, homotopies are equivalence classes of paths. It's a topological notion. Wasn't sure what you mean by strings of symbols in that context.

I understand a subobject classifier as the set {0,1} that characterizes a subset of a set, say, as a map from the subset to 1 and everything else in the set to 0; that is, the characteristic function of the subset.

I'm still not totally seeing the part about propositions and proofs. But I must be getting close.

Wait -- the subobject classifier is the set of ALL the propositions? Not sure I'm following that.

"the implications between these propositions are arrows that start and end in this object." -- Tht seems to imply that the propositions form a category, and the arrows are implications. That much I know from Awodey. You lost me on the subobject classifier in this context; and how this relates to a section of a fiber bundle as a proof of a proposition. But I feel like I must very close to getting this.

Now, a section of the fiber bundle (https://en.wikipedia.org/wiki/Section_(fiber_bundle)) is what in type theory is called a "dependently typed function", that from the point of view of logic is interpreted as the proof of a proposition with a free variable x: the fiber bundle is the proposition (that depends on x) and a section of that fiber bundle is a proof of that proposition. — Mephist

I can't see this. Can you give an example?

Probably you think that I completely missed the "meaning" of what a mathematical proof. But that's the way computers (formal logic systems) see proofs. I agree that the formal part is not all there is in it. Just take a look at this discussion, for example: — Mephist

I didn't understand which side you're agreeing with. Do you think that the meaning of a proof is to be found in its syntactic form? Or that mathematical meaning goes beyond formalization?

Ok back to the first point. Totally simplistic example. $f(x) = x^2$. The fiber bundle is all the pairs like $\{5, -5 \}$ and so forth, all the sets that are the inverse images under $f$ of the various points on the real line.

A section is one particular choice of elements, like always choosing the positive square root, or flipping a coin to determine which of the two square roots to choose.

Now I am squeezing my brain but I don't quite see how the collection of all sections is a proposition, and an individual section a proof.

I hope this example is detailed enough so that you can straighten out any misunderstandings I might have about what's a fiber or section, and what's a fiber bundle. And how proofs relate.