Yes but mathematics needs computations for proofs, and computations are physical processes. — Mephist

I was reading through the thread and this caught my eye. Why does mathematics need computations? Because before there were computers, the humans did the computations. In math we still do. Computations with pencil and paper are no different in principle than the same computations done on a supercomputer, and vice versa.

So in fact mathematics itself, defined as everything mathematicians have written down or even thought about -- since thought is a physical process too -- is a "physical process." The work of mathematicians takes energy; and therefore it should be possible to study the nature of math as a physical process.

Or as the saying goes: Mathematicians are people who turn coffee into theorems! I think that pretty much captures the spirit of the idea.

and even Martin-Löf type theory has a lot of variants (too many to be something important, right? :smile: ) — Mephist

(Eyes glaze).

But I think that now the picture is becoming quite clear (even thanks to Voevodsky's work): — Mephist

Name drops Voevodsky. Didn't we do this last week? Or was that someone else?

there is a very strict correspondence between topology and logic. — Mephist

Perfectly well known before Vovoedsky.

But you have to "extend" the notion of topology to the one of topoi (a category with some additional properties). ZFC is the logic corresponding to the standard topology (where lines are made of uncountable sets of points). But ZFC and the "standard" topology are not at all the only logically sound possibility! (that in a VERY short summary) — Mephist

Do you know topos theory? Can you "explain like I'm five" to someone who knows a little category theory?

But when did I ever say standard math is the only logically sound way of doing things? I don't think I hold the view you're trying to dispel.

So in fact mathematics itself, defined as everything mathematicians have written down or even thought about -- since thought is a physical process too -- is a "physical process." The work of mathematicians takes energy; and therefore it should be possible to study the nature of math as a physical process. — fishfry

Yes, exactly! (well, I don't understand what energy has to do with this, but more or less...) However, that's only MY idea (and it's more about philosophy than mathematics). So, even if there are lots of mathematicians that have similar ideas (as I believe), no serious mathematician is so courageous to say this loudly! :yikes: (just take a look at arXiv.org and try to find any word about philosophy!).

The correspondence between topology and logic instead, that's one of the most popular and ideas of today's mathematics! :cool:

Yes, of course practically all "normal" proofs are short and all the computing power needed is a pen and a peace of paper. But in reality all computations can be considered to be proofs, right? You reduce an expression in a normal form following some rules (if it's a multiplication between integers the "proof" can be made automatically with a calculator). — Mephist

It depends upon what you mean by "short." Or "normal." In the area I'm most familiar with theorem proofs vary from a few lines to a number of pages in length. And a short proof may be of an extension of a theorem which required many pages of reasoned articulation. I would rather use a pencil than a pen, however, so I can erase my errors or scribbling along non-productive paths of thought!

When you say computations can be considered proofs I'm not sure where you are going. Proofs of what? And "reduce an expression in a normal form" - what's that? Mathematical proofs are rigorously reasoned arguments in logic in which concepts and relationships play significant roles.

There are occasional exceptions in which computers are essential, like the Four Color Theorem in combinatorics. And then mathematicians attempting to verify the overall presentation of proof and conclusion are stuck with verifying computer algorithms and assuming the computers running them do not produce computational errors.

"The correspondence between topology and logic instead, that's one of the most popular and ideas of today's mathematics!"

I'll have to check this out. I've been out in the pasture too long I guess. :worry:

The correspondence between topology and logic instead, that's one of the most popular and ideas of today's mathematics! — Mephist

You mentioned topos theory in one of your posts. I read the Wiki page, or re-read it since I've looked at it before. It's abstract sheaf theory. What's sheaf theory? It's the idea of assigning an algebraic object to each point of a topological space or manifold. For example the set of continuous functions that vanish at a given real number is an ideal in the ring of continuous functions on the reals. So the ideals of the ring give you information about the points. This is a fairly sophisticated mathematical point of view.

And then topos theory is abstract sheaf theory. So mathematically, this is advanced grad student level. But apparently a lot of the terminology and concepts are trickling into computer science and other fields.

I was wondering in what context you'd seen topoi. I know there's a lot of category theory in computer science these days. But my sense is that topoi are fairly sophisticated mathematical objects, at least in their mathematical applications.

Name drops Voevodsky. Didn't we do this last week? Or was that someone else?

there is a very strict correspondence between topology and logic.
— Mephist

Perfectly well known before Vovoedsky. — fishfry

OK, I'll try to explain this point.
The fact that there is a relation between topology and logic (mediated by category theory) was well known even before, you are right. But Voevodsky's "homotopy type theory" (https://homotopytypetheory.org/) does not say simply that there is a relation between topology and logic: it says that "homotopy theory" (that is a branch of topology) ( https://en.wikipedia.org/wiki/Category:Homotopy_theory ) and Martin-Lof intuitionistic type theory with the addition of a particular axiom (the univalence axiom - https://ncatlab.org/nlab/show/univalence+axiom) ARE EXACTLY THE SAME THING (the same theory). Meaning: there is this axiomatic theory that speaks about homotopy between topological spaces, expressed in the language of category theory (and then in ZFC set theory - it is still valid in any topos, but I don't want to make it too complicated). So, the terms of the language are spaces, points, paths connecting points, equivalence classes between these paths etc...
Now, if you take whatever theorem from homotopy theory and RENAME all the terms of this theory, substituting the word "types" to the word "spaces", "proofs" to the word "points", "equalities" to the word "paths", etc... (lots of details omitted, of course), you obtain a theorem in type theory. And if you take any theorem in type theory you can reinterpret it as a theorem about topology.

At the end, something similar happens even with the usual set theory: a set can be interpreted as the set of all models that satisfy a given proposition, inclusion between sets can be interpreted as implication between propositions, intersections as "AND" operations, etc... But you know, the devil is in the details (expecially in "infinitary" details :wink:).
Well, in the case of topology and type theory all the details match exactly: it's "take two at the price of one". You prove something about topological spaces and you obtain a theorem about types, and vice-versa.

And then topos theory is abstract sheaf theory — fishfry

Thanks for saving me the effort of looking it up. That one sentence is enough for me. :brow:

Do you know topos theory? Can you "explain like I'm five" to someone who knows a little category theory? — fishfry

OK, I'll try. But I think it will be a long post anyway. So, I'll do it after answering the other posts before.

But I can give you the reference to a very good book (in my opinion) on this subject that is easy to understand for somebody that has some basis of category theory:
- Title: "TOPOI THE CATEGORIAL ANALYSIS OF LOGIC"
- Autor: Robert Goldblatt
( I found it even on Amazon: https://www.amazon.com/Topoi-Categorial-Analysis-Logic-Mathematics/dp/0486450260 )

When you say computations can be considered proofs I'm not sure where you are going. Proofs of what? And "reduce an expression in a normal form" - what's that? Mathematical proofs are rigorously reasoned arguments in logic in which concepts and relationships play significant roles. — jgill

OK, let's start from examples of normal forms:
"245 * 10" is a number that is not in normal form. "2450" is the same number in normal form (one of the possible normal forms)
"5/10" is not in normal form. "1/2" is the same number in normal form.
If two strings of characters that represent numbers (in a given formal language) are in normal form, the numbers are equal if and only if they are the same string of characters.
I searched in wikipedia and found this: https://en.wikipedia.org/wiki/Canonical_form . But if you read a book about formal logic this is usually called "normal" form, and not "canonical" form.

The "proofs of what" question is a little harder to answer (but the concept is very simple).
Normally you think of a computation (for example a multiplication of two integers) as an algorithm that takes some arguments as input and returns an output.
But you can think of the same computation as list of transformations that starts from an initial expression ( "12 * 12" ) and transforms it into a second expression ( "144" ) by applying at every step one of the possible "rewriting rules" allowed by the logic. For example, take a look at the section "Arithmetic" here: https://en.wikipedia.org/wiki/Rewriting . In other words, a computation can be seen as a special kind of "prove": the prove that the term "144" is the normal form of the term "12 * 12".

There are occasional exceptions in which computers are essential, like the Four Color Theorem in combinatorics. And then mathematicians attempting to verify the overall presentation of proof and conclusion are stuck with verifying computer algorithms and assuming the computers running them do not produce computational errors. — jgill

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: https://thephilosophyforum.com/discussion/6205/mathematics-is-the-part-of-physics-where-experiments-are-cheap

There are occasional exceptions in which computers are essential, like the Four Color Theorem in combinatorics. And then mathematicians attempting to verify the overall presentation of proof and conclusion are stuck with verifying computer algorithms and assuming the computers running them do not produce computational errors. — jgill

Probably you think that I completely missed the "meaning" of what a mathematical proof is. But that's the way computers (formal logic systems) see proofs. I agree that that's not all. Just take a look at this old discussion with Alcontali, for example: https://thephilosophyforum.com/discussion/6205/mathematics-is-the-part-of-physics-where-experiments-are-cheap

Yes, it seems very strange! Here's the "quick and dirty" explanation:

A sheaf S over a topological space X is a "fiber bundle", where the fibers over a point x in X are disjoint subspaces of S. 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.

The fundamental idea is the same: you have a map in which each input value is defined on a different domain, and that domain DEPENDS on the input value in a "continuous" way. In your example the ideals are the fibers (dependent on the point x) and the ring of continuous functions is the total space S.

The point is: what continuity has to do with formal logic, where we speak only about symbols and rules?
Well, "continuity" in this context means "parametric" function. A "continuous" (or parametric) function is a function that doesn't jump from a formula to the other when you change the point x:

| x = 20 ==> "x is a multiple of 2"
| x = 21 ==> "x is a multiple of 3"
| x = 22 ==> "x is a multiple of 4"
this IS NOT a "continuous" function, because it has different formulations for different values of x

| x = 20 ==> "x is a multiple of 2"
| x = 21 ==> "x is a multiple of 2"
| x = 22 ==> "x is a multiple of 2"
this IS a "continuous' function, because it has the same formulation for every value of x.

The fibers of this bundle are the following ones:
| "20 is a multiple of 2"
| "21 is a multiple of 2"
| "22 is a multiple of 2"

The first and the third fibers are not empty (because they contain some points: the points are the proofs of the respective propositions)
The second fiber instead is empty (there are no proofs of this proposition)

OK, I'll stop here for the moment, because I am a little afraid of the answer "that's all bullshit, I'll not read the rest of it..." :worry:

However, the point is the following: this is an axiomatic theory; the same axioms can have completely different meanings that relate to complete different mathematical objects. Only they happen to behave in a similar way. That's the typical for category theory: every collection of objects that are related to each other in the same way are the same category. It is completely irrelevant what they are "made of"!

And then topos theory is abstract sheaf theory. So mathematically, this is advanced grad student level. But apparently a lot of the terminology and concepts are trickling into computer science and other fields.

I was wondering in what context you'd seen topoi. I know there's a lot of category theory in computer science these days. But my sense is that topoi are fairly sophisticated mathematical objects, at least in their mathematical applications. — fishfry

Re-reading your question I just realized that probably my answer about homotopy type theory could be misleading: this is really a weird and interesting theory, but topoi and sheaves are NOT related to computer science only because of the use of type theory as a logic to prove theorems! On the contrary, I think the use of formal logic in proof assistents is only a very limited field of informatics, with not many practical applications. On the contrary, sheaves are mostly used in data-analysis applications that have nothing to do with formal logic!

It is true that they can be very abstract objects in mathematics, but for a data-science person a sheave is mostly a data-correlation tool. A sheave can represent a cellular-phone network and relate each cell of the covered area with the set of users that are connected to that cell. Finite-shapes topology is still topology, and computer-science is first of all used for big and discrete sets of data! (here's an example of what I mean: http://www.drmichaelrobinson.net/sheaftutorial/)

Do you know topos theory? Can you "explain like I'm five" to someone who knows a little category theory? — fishfry

OK, that's the "like I'm five" explanation: A topos is a category that "works" as the category of sets, but is not built using a set of rules that operate on symbols as a formal logic system: it's the formulation of set theory in terms of objects, arrows, and universal-mapping properties.

So, there is a main ingredient that is missing: points! Topos theory is a formulation of set theory where sets are not "built" starting from points. Sets (the objects of the category) and functions (the morphisms of the category) are considered as "primitive" concepts. The points are a "secondary" construction.
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?

Probably you think that I completely missed the "meaning" of what a mathematical proof is — Mephist

What you have said about proving mathematical theorems may be the way computers see the process, but most theorems are not proven by computer programs. I don't see the connection to anything I have encountered in theorem-proving. But I am retired and way behind the times in really abstract math. Maybe the world has changed in my absence. Maybe not. I appreciate your efforts to explain, however.

"I agree that that's not all."

Which has to take a prize as an understatement. Is most of your experience in computer science?

It is true that they can be very abstract objects in mathematics, but for a data-science person a sheave is mostly a data-correlation tool. A sheave can represent a cellular-phone network and relate each cell of the covered area with the set of users that are connected to that cell. — Mephist

OMG that sort of makes sense. Thank you for that example. I've been reading up on sheaf theory and every presentation that comes up on Google is heavily mathematical, so much so that I can't for the life of me understand how they're teaching this stuff to undergrads in non-mathematical fields. I will definitely read the link you supplied. Perfectly sensible ... to each individual cellphone you associate their call network. So it's an algebraic structure -- a network or graph -- assigned to each element of some set. Very nice example. And of course a great illustration of how wild mathematical abstractions so often end up being incredibly useful in the real world.

And a topos is an abstract sheaf? And what I read was that topoi are inherently intuitionistic. I haven't followed that chain of reasoning yet.

Thanks for saving me the effort of looking it up. That one sentence is enough for me. — jgill

I do not think this is so bad. I'm learning what a sheaf is and after that, topoi are the next step up. If I figure anything out I'll post it. What's interesting is that the highly super-abstract algebra has deep repercussions in logic. Even without any of the details, that's the takeaway.

OK, I'll try to explain this point.
The fact that there is a relation between topology and logic (mediated by category theory) was well known even before, you are right. But Voevodsky's "homotopy type theory" (https://homotopytypetheory.org/) does not say simply that there is a relation between topology and logic: it says that "homotopy theory" (that is a branch of topology) ( https://en.wikipedia.org/wiki/Category:Homotopy_theory ) and Martin-Lof intuitionistic type theory with the addition of a particular axiom (the univalence axiom - https://ncatlab.org/nlab/show/univalence+axiom) ARE EXACTLY THE SAME THING (the same theory). Meaning: there is this axiomatic theory that speaks about homotopy between topological spaces, expressed in the language of category theory (and then in ZFC set theory - it is still valid in any topos, but I don't want to make it too complicated). So, the terms of the language are spaces, points, paths connecting points, equivalence classes between these paths etc...
Now, if you take whatever theorem from homotopy theory and RENAME all the terms of this theory, substituting the word "types" to the word "spaces", "proofs" to the word "points", "equalities" to the word "paths", etc... (lots of details omitted, of course), you obtain a theorem in type theory. And if you take any theorem in type theory you can reinterpret it as a theorem about topology. — Mephist

Be advised that any paragraph containing the name Martin-Löf instantly glazes my eyes. I've had all these conversations too many times. I totally believe everything you say but can't actually figure out what point you are trying to make. I don't disagree with anything you say, and I'm aware in varying degrees with various aspect of the things you talk about. I just don't know why you're telling me this. I don't disagree with you on any of it and I can't relate this to whatever we are talking about.

Can you just remind me what is the point under discussion?

But I can give you the reference to a very good book (in my opinion) on this subject that is easy to understand for somebody that has some basis of category theory:
- Title: "TOPOI THE CATEGORIAL ANALYSIS OF LOGIC"
- Autor: Robert Goldblatt — Mephist

Thanks. I know Goldblatt as the author of Lectures on the Hyperreals. I'll add this book to my growing list of books to read someday. So far the list stretches into several of the next few lifetimes.

I am reading articles on sheaf theory (of the mathematical kind) and it's very straightforward, although most of the serious applications are beyond me. I will read the paper you linked about network topology, that example was very insightful. Steve Awody's book on category theory has a lot of applications to logic. Another book on my list.

Which has to take a prize as an understatement. Is most of your experience in computer science? — jgill

Yes, I work as a programmer. And yes, a formal proof completely misses the essence of a proof: it's "meaning". I don't beprove lieve mathematics is changed at all in that respect! Computers do not PROVE theorems: they VERIFY the formal correctness of a proof, that is a completely different thing!

But I even believe that this distinction is not clear at all in today's mathematics, and it has never been understood: 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.

I believe this fact is becoming evident, even thanks to artificial intelligence, and will be understood in a not very distant future. By the way, the effect of this misunderstanding of mathematical proofs is terrible for education: teaching only the formal part of mathematics completely misses the essence of mathematics!

it's the formulation of set theory in terms of objects, arrows, and universal-mapping properties. — Mephist

That's what EVERYTHING is in category theory! So that didn't tell me anything about topoi!

You wrote me two detailed technical posts that I'll try to catch up to later. But I'm actually on my own path. I found a nice paper on sheaf theory that I can understand and I'm working through that.

I've also in the past seen a video with Steve Awodey where he worked out the definition of a Cartesian closed category then applied it to logic. So I don't even think you have to go all the way to topoi to get to applications in logic. I'm probably going to spend a few days reading papers and see if I can get a hold on a vertical slice of understanding.

A sheaf S over a topological space X is a "fiber bundle", where the fibers over a point x in X are disjoint subspaces of S. 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

Now that is interesting, because fiber bundles are a big thing in differential geometry. It's interesting that they lead directly to type theory. Thanks for pointing that out.

As with your other technical post, I'll defer comment for now but I'll read through them.

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) = x^2$ 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?

And a topos is an abstract sheaf? And what I read was that topoi are inherently intuitionistic. I haven't followed that chain of reasoning yet. — fishfry

A sheaf is a topos at the same way as a set is a topos: it's the "trick" of the Yoneda embedding! :smile: do you understand now? (sorry: bad example.. let's say that a sheaf can make everything - more or less - "become" a topos)

A sheaf is a topos at the same way as a set is a topos: it's the "trick" of the Yoneda embedding! :smile: do you understand now? (sorry: bad example.. let's say that a sheaf can make everything - more or less - "become" a topos) — Mephist

I'm going to spend the next week working through this material. I'm encouraged that I can understand what a sheaf is and know a few examples; and I know enough category theory to get by.

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

Be advised that any paragraph containing the name Martin-Löf instantly glazes my eyes. I've had all these conversations too many times. I totally believe everything you say but can't actually figure out what point you are trying to make. I don't disagree with anything you say, and I'm aware in varying degrees with various aspect of the things you talk about. I just don't know why you're telling me this. I don't disagree with you on any of it and I can't relate this to whatever we are talking about.

Can you just remind me what is the point under discussion? — fishfry

OK, never mind. Sorry for continuing to repeat the same things!

OK, never mind. Sorry for continuing to repeat the same things! — Mephist

No problem, you've gotten me interested in sheaf theory and then on to topos theory. But I'm still probably more oriented to the mathematical applications than the logical ones.

So I don't even think you have to go all the way to topoi to get to applications in logic. — fishfry

Exactly! We are speaking about two different kinds of "representations" of logic.

OK, I'll stop here for the moment, because I am a little afraid of the answer "that's all bullshit, I'll not read the rest of it..." — Mephist

No this is totally fascinating, very clear writeup, worthy of study. I know what fiber bundles and sections are. I can't quite grok the application to proofs but it may come to me.

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?

So, there is a main ingredient that is missing: points! Topos theory is a formulation of set theory where sets are not "built" starting from points. Sets (the objects of the category) and functions (the morphisms of the category) are considered as "primitive" concepts. The points are a "secondary" construction. — Mephist

Ok now I know this idea as ETCS: The extended theory of the category of sets, which is an implementation of set theory on top of category theory. Is this the same thing as what you're talking about?

Yes it's wondrous that we can do set theory without talking about points! Deep philosophical implications since we no longer care at all what a thing is, only how it relates to everything else.

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

I know about measure theory since when I was at high school (I always liked that stuff), and I heard that sentence about the probability to find a rational among real numbers a thousand times :razz:
But then I realized that not everything that they teach you in high school has to be taken as the absolute truth :smile: