Yes but mathematics needs computations for proofs, and computations are physical processes. — Mephist
and even Martin-Löf type theory has a lot of variants (too many to be something important, right? :smile: ) — Mephist
But I think that now the picture is becoming quite clear (even thanks to Voevodsky's work): — Mephist
there is a very strict correspondence between topology and logic. — Mephist
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
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, 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
The correspondence between topology and logic instead, that's one of the most popular and ideas of today's mathematics! — 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. — fishfry
Do you know topos theory? Can you "explain like I'm five" to someone who knows a little category theory? — fishfry
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
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
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
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
Do you know topos theory? Can you "explain like I'm five" to someone who knows a little category theory? — fishfry
Probably you think that I completely missed the "meaning" of what a mathematical proof is — Mephist
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
Thanks for saving me the effort of looking it up. That one sentence is enough for me. — jgill
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
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
Which has to take a prize as an understatement. Is most of your experience in computer science? — jgill
it's the formulation of set theory in terms of objects, arrows, and universal-mapping properties. — Mephist
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
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) — 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? — fishfry
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
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
May I ask you a question? How does one come to know this material and not have heard of measure theory? — fishfry
Get involved in philosophical discussions about knowledge, truth, language, consciousness, science, politics, religion, logic and mathematics, art, history, and lots more. No ads, no clutter, and very little agreement — just fascinating conversations.