Remind me of the defs. A section is a right inverse as I understand it. There can be a lot of right inverses to a function, you just keep choosing different elements in the preimages of points. Is that the bundle? — fishfry

Yes! I should have added a formal definition, but I have an aversion to writing symbols on this site :confused: I added a link with a clear picture, I think.

there is no definition of the "meaning" of a theorem, and many mathematicians (starting from Hilbert, I guess) think that there is no point in trying to identify the "meaning" as something different from a list of symbols. — Mephist

This must be a significant difference between what you do and what a research mathematician does. Recently I've proven theorems related to compositions of functions in the complex plane, and with each I have a deep feeling, a strong sense of meaning, about the result and how the result comes about. A lot of geometrical mental imagery coupled with the essence to which the symbols point - much like reading literature and realizing all those symbols describe something that stirs the imagination.

However, my theorems are not profound - strictly what Wikipedia calls "Low" interest! :cool:

Yes.

Yes! I should have added a formal definition, but I have an aversion to writing symbols on this site :confused: I added a link with a clear picture, I think. — Mephist

I think when I grok how fiber bundles can be likened to proofs, I'll be enlightened.

Did you learn all this from the CS viewpoint? Just wondering.

Yes. — Mephist

I have no idea what question is was a response to. But if you agree with me, you have excellent taste!

I agree with you. But now I am too curious: which theorems did you prove?

May I ask you a question? How does one come to know this material and not have heard of measure theory? — fishfry

Where does measure theory (surely not taught in high school) intersect any of this? I've used it in various integration processes, the most interesting being functional integration. And Feynman constructed his sum of paths integral in more or less that concept.

Did you learn all this from the CS viewpoint? Just wondering. — fishfry

No, I like "normal" mathematics: no computers involved. But having a theorem-prover as Coq to be able to verify if you can really write a proof of what you think is provable is very helpful.

But now I am too curious: which theorems did you prove? — Mephist

I write math notes now as a hobby. Here's a couple :cool:

https://www.researchgate.net/publication/319057086_A_Primer_on_the_Elementary_Theory_of_Infinite_Compositions_of_Complex_Functions

https://www.researchgate.net/publication/324017489_A_Short_Note_Compositions_of_Linear_Fractional_Transformation_Forms

No, I like "normal" mathematics: no computers involved. But having a theorem-prover as Coq to be able to verify if you can really write a proof of what you think is provable is very helpful. — Mephist

I'm reading the data science paper you linked. They teach sheaf cohomology to data scientists. That is so fascinating. To me, with my math background, sheaf cohomology is something that would take someone a long time to learn, at least a couple of years of grad school or more. But at the application level, the concepts have filtered down and you don't have to actually know any of the original mathematical context in which these ideas evolved. It's yet another illustration of the applicability of highly abstract math. The "unreasonable effectiveness" all over again. Category theory dates from the 1940's but it's only peeking its head into the real world in the past twenty years.

Where does measure theory (surely not taught in high school) intersect any of this? I've used it in various integration processes, the most interesting being functional integration. And Feynman constructed his sum of paths integral in more or less that concept. — jgill

Oh, it doesn't. I mentioned that the computable numbers have measure zero in the space of bitstrings, and @Mephist asked me how that's defined mathematically, so explained it a little. Then he responded by saying he's known about this since high school. So @Mephist I apologize if I misunderstood you.

The subject came up in the context of my perennial hobbyhorse that there aren't enough computable numbers to make up a decent continuum; and why aren't the constructivists ashamed of themselves. I have never gotten an answer to this question that satisfies me. At some point they say "Martin-Löf type theory" and I know I've lost the argument. It's a cult. [mild humor intended].

Remind me of the defs. A section is a right inverse as I understand it. There can be a lot of right inverses to a function, you just keep choosing different elements in the preimages of points. Is that the bundle? — fishfry

Yes.

Remind me of the defs. A section is a right inverse as I understand it. There can be a lot of right inverses to a function, you just keep choosing different elements in the preimages of points. Is that the bundle?
— fishfry

Yes. — Mephist

Ok a fibre bundle is the collection of all possible right inverses to a function. And a section is one of those right inverses. Yes?

I may be off the mark here but I wonder if it's relevant that we have introduced a little bit of nonconstructivism. How do you know you can always take a section of a surjective function? That claim is equivalent to the axiom of choice. It makes sense. Take the cosine or sine functions. Each real number between 0 and 1 has infinitely many inverses, separated by 2 pi. For each point in [0,1] we choose an element from its inverse image. So you can see how the axiom of choice comes up. Of course in this particular case we could take the smallest positive inverse, so we don't need the axiom of choice. But in the general case we do.

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.

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.

think that you are ascribing to mathematics the kind of role that I don't think it has. At least, not directly. Or maybe I did walk into this when elaborating over my example. Its aim wasn't to model the structure of physical objects, but to illustrate how coarse structures not literally represented by mathematical ideals, can still be usefully approximated by those ideals. It was designed to have some similarity with the atomic structure of materials. — simeonz

I don't think I agree with your assumptions about the role which mathematics has. I believe that mathematical principles are always developed for purposes, goals, ends, and therefore utility in the physical world. Now, I discussed this to some extent in another thread, and I was shown that this is not necessarily the case. It was demonstrated that mathematical principles, as art, may be created purely for their beauty, without any intent to purposefulness, and then found to be purposeful posteriorly. Of course these arguments are still debatable, and we probably cannot get to the bottom of this. Even if a person creates a mathematical principle without intent or purpose, the demonstration of that principle to another person would be done with purpose. So the fact that we can argue that mathematical principles may be created without a purpose, is really just a demonstration of free will. When there is no necessary relation between the effect, and the cause, we have a demonstration of free will.

So I have a problem with your example, in the sense that it seems unrealistic. The purpose of the example is to illustrate something, to argue a point. But if you assume unrealistic "materials" to make that argument, how can the argument be acceptable? You have chosen a particular type of "material", one sufficient to make your argument, but one which is not real.

The idea was, that actual physical structures approximate the mathematical ideals, and our numerical algorithms approximate those same ideals, and thus, under certain assumptions of the magnitudes of the involved deviations, our numerical algorithms match the physical structures within the required precision. — simeonz

So my argument was that "actual physical structures" do not approximate the mathematical ideals, in your example, because the "materials" are completely different. So, further to your example, I think that this problem is widespread in physics. The physicist applying mathematical principles believes that the "materials" of mathematical ideals are a good approximation of the "materials" involved in actual physical structures, when in reality they are not. This mistaken notion is a holdout from Platonism. Platonism assumes that the mathematical materials 'are' the materials of physical structures. When we let go of Platonism, we have a desire to maintain some semblance of truth within our conceptual structures, so we maintain that the mathematical materials provide an approximation of the actual physical materials, but there is no justification for this. "It works" justifies the means to the end, but it does not justify "an approximation of the actual physical materials".

P.S. I want to clarify that I do actually think that our computational and logical ideals are naturally inspired. They are not literally representative of any particular physical structure, but they are "seeded" as concepts by nature, whether our sentience existed or not. — simeonz

This is the point we need to iron out then. Let's assume that human beings came into existence through evolution. The kernel to the concepts which are "seeded", are what is instinctual to us, but these must have been produced through evolution, therefore they are purposeful. If there is always a seed prior to the instinct, and that seed is not necessarily for a purpose, then we'd go right back to the first life form and ask where did that first seed come from. So it really doesn't seem to make sense to say that the concepts are "seeded" by nature, and they are not representative of nature.

How could we proceed from here? If the seeds are part of nature, then we fall into Platonism. If they are something other than natural, wouldn't they necessarily have to represent something natural in order to be at all useful? How would a concept which has absolutely no representation of anything real become useful?

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

OK, I'll start from the example:

1. Let's call Unit our terminal object.
2. Let's call Prop the object that is part of our subobject classifier (usually called Omega, but I prefer Prop, from Coq's convention).
3. Let's call "true" the arrow from Unit to Prop that is part of our subobject classifier.

4. Assume that there is another object, called Nat.
[ this is the set of natural numbers ]

5. Assume that there is an arrow "s" from Nat to Nat.
[ this is the "successor" function, from Peano arithmetic ]

6. Assume that there is an arrow from Unit to Nat called "zero"
[ this is the number zero ]

7. Let Nat->Prod be the exponential of Nat and Prod
[ this represents all propositions with a free variable of type Nat ]

8. Let Nat->(Nat->Prod) be the exponential of Nat and (Nat->Prod)
[ this represents all propositions with two free variables of type Nat ]

9. Let "x_is_greater_than_y" be an arrow from Unit to Nat->(Nat->Prop)
[ this is a proposition with two free variables of type Nat ]

10. Let's call "x_is_greater_than_zero" the arrow "x_is_greater_than_y" * "zero"
[ * is the operation of arrow composition from category theory's axioms ]
[ "greater_then_zero" will be then an arrow from Unit to Nat->Prop ]
[ this is a proposition with one free variable of type Nat ]

11. Let's call "s(x)_is_greater_than_zero" the arrow "x_is_greater_than_zero" * "successor"
[ this is still a proposition with one free variably of type Nat ]

12. Let's call "one_is_greater_than_zero" the arrow "s(x)_is_greater_than_zero" * "zero".
.......

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!
I have to find a better way to give you a description of how it's made without writing all the details... :worry:

.. . . believe that mathematical principles are always developed for purposes, goals, ends, and therefore . . . — Metaphysician Undercover

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

A section is a proof ... a section is a proof. I can't quite see that. I know that a section is a right inverse of a function. For example if f(x)=x2f(x)=x2 then a section is a function that, for each nonnegative real, picks out one of its plus or minus square roots. Is that about right? The section is the right inverse, so it's essentially a choice function on the collection of inverse images of all the points. Do I have that right? How does that become a proof? — fishfry

Let me just give you just some examples: "x >= 3" is a fibration from the object Nat to the subobject classifier Prop. The proposition "5 >= 3" is a fiber of this fibration. The elements of this fiber are the "proofs" that 5 >= 3. So, there will be a function F (built using the rules of logic) that allows you to build a proof of 3 >= 3, and a proof of 4 >= 3, and a proof of 5 >= 3, etc.. (meaning: to choose a proof for each proposition of the form "x >= 3"). This function is the section of the fibration from the space of proofs to the space of propositions of the form "x >= 3": it selects a proof (an element of the fiber) for each proposition of the form "x >= 3".
The function that generates all the proofs of the form "x >= 3", however, is not an algorithm that chooses a different list of rules for each value of x: it doesn't say "if x = 3, then apply the rule A to prove "3 >= 3";
if x = 4 then apply the rule B to prove 4 >= 3". Instead, it's a parametric program that says: if you have an x with such and such characteristics, then you can apply the rule A(x), where x is a variable of the rule. That means that the section of the fiber is "continuous".

Propositions containing variables (such as "x >= 3") are called "dependent" types because they are sets (of proofs) that depend on a parameter (x), and the function that is used to build the proof of "x >= 3" builds an element of a different type (a proof of a different proposition) for each value of x (builds the set and selects the point at the same time).

Fiber bundles of "normal" topological spaces (such as the famous Mobius strip - https://en.wikipedia.org/wiki/M%C3%B6bius_strip) are built in the same way: you choose a disjoint segment (set of points form a total space E) for each point of a circle (base space B) using a continuous function!

It's much more difficult to explain than I thought...

Some references:
https://ncatlab.org/nlab/show/subobject+classifier
https://ncatlab.org/nlab/show/type+of+propositions

P.S. notice that this form of the subobject classifier is typical only for type theories, where the propositions are represented by the collection of all their proofs:
( from https://ncatlab.org/nlab/show/type+of+propositions ):
"In type theory the type of propositions Prop corresponds roughly under categorical semantics to the subobject classifier. (To be precise, depending on the type theoretic rules and axioms this may not be quite true: one needs propositional resizing, propositional extensionality, and — in some type theories where “proposition” is not defined as an h-proposition, such as the calculus of constructions — the principle of unique choice?.)"

For classical (boolean) logic, instead, the subobject classifier is much simpler: it has only 2 incoming arrows (elements) from the terminal object: "true" and "false". That's because in classical logic, differently from type theory, the propositions are represented only by their truth value (true or false), and not by the list of derivations (or programs) used to prove them.

- We know that we cannot enumerate all halting Turing machines, so for every supposedly complete list of halting Turing machines I can find another halting Turing machine that is not in the list.
Does that mean that the set of halting Turing machines in uncountable? No! It only means that there is no way to enumerate that list!. — Mephist

Yet saying that there is no way to enumerate the total computable functions is somewhat ambiguous, for as previously mentioned we can use brute force to simulate every TM on every input and enumerate on-the-fly the algorithms that have so far halted on all their inputs. Furthermore, the classical logician with realist intuitions will go further to argue that there is a definite matter-of-fact as to the set of computable functions and will therefore believe in the independent existence of a 'finished' enumeration, interpreting the limitations of finite constructive arguments to produce such an enumeration as being epistemic limitations rather than metaphysical limitations. Instead they will simply appeal to the Axiom of Choice to claim the independent existence of completed enumerations of the computable total functions.

As we said earlier, this full enumeration cannot be used if the diagonal function d(x) is to be both computable and total; otherwise if the realist diagonalizes the hypothetical full enumeration of computable total functions, then d(x) cannot be computable, for the enumeration ensures that d(x) is total. That d isn't computable is obvious, since it involves running nearly every Turing Machine for an infinite amount of time and then diagonalizing, meaning that it's godel number g is infinitely long and that it assumes an infinite value when evaluated at d(g)=d(g)+1

The physicist applying mathematical principles believes that the "materials" of mathematical ideals are a good approximation of the "materials" involved in actual physical structures, when in reality they are not. — Metaphysician Undercover

Maybe I am not on the same page with you here. Before I try to answer in any detail, I have to get clear on the substance of our conversation. Are you saying that you imagine a system of computations which does not involve algebraic numbers, and either has the same utility for our industrial and daily applications at a discount computational cost, or enhances our conventional applications at no additional computational cost? 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.

OK, you are right!
What I wanted to point out is that the sentence "there is an uncountable number of sequences", when expressed in the forall-exists language, does not contain the word "uncountable". And you can't say it in an unambiguous way. This is our interpretation in natural language of the sentence "forall lists of functions Nat->Nat there exists a function Nat->Nat that is not on the list". So, there exists ONE missing function. You are adding one function at a time! The translation of this sentence in natural language with the word "uncountable" is arbitrary, in my opinion.
As the induction principle "(P(0) and (forall N, P(N) implies P(N+1))) implies (forall N P(N))" can be seen as part of the axiomatic definition of the world "forall", at the same way there should be a second axiom that can be seen as the axiomatic definition of the world "uncountable": the same is done in modal logic with the word "necessarily". Doesn't it make sense?

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.

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.

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.

* What's Nat? — fishfry

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

* 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? — fishfry

Prop is the type of propositions. It's an object of the category. {Prop, true} is the subobject classifier of the topos

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. This is frustrating at my end. I can't tell if you know what you're talking about or if you just read a lot of Wiki pages. That's not meant to be provocative. Only that you are not communicating to me at all. And like I say I know this because I did my mathematical homework last night re sheaf theory. — fishfry

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. I am interested in mathematics and physics as an hobby, and I often read new publications from arxiv.org

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.

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.