It is a bad model, that's true. The point is there isn't a theory of the chemical bond in physical terms that can reduce the understanding of chemistry to physics. Such a project was the foolhardy venture of physicists in the 20th century that's been pretty much abandoned. The point is, we have chemistry understanding of chemical bonds, and we have quantum mechanics understanding of the chemical bond, separate, and probably won't be breached into any cohesive theories, and can't be extended into each other. The theories we have are super limited, and we can't do much to move past them.



As above: you can't exorcise axiomatic set theory. You can call it defunct and historical, but we don't have anything better or more capable. Virtually all proofs in math still depend on the assumptions and theorems of axiomatic set theory, that's not changing or going away any time soon.

I'll admit I didn't go far enough into real analysis to really appreciate this point, but: do we really depend on the axioms of set theory that much? How much in real analysis and measure theory really rests upon axioms in set theory to really clarify what's going on, in practice, when analysts use theorems involving infinite sets? Did mathematicians really doubt their results before they settled questions about them in axiomatic set theory? I would be willing to accept this, but in some cases would find it hard to believe.

At any rate, is there much of a difference in just completely ignoring the axioms of set theory (so long as contradictions don't turn up in the naive, non-axiomatic layers of real analysis), versus the kind of ignoramus et ignorabimus that Godel forced mathematicians into, so that they now simply accept that there might be contradictions in set theory, but that we may never find them? I mean, in both cases we simply have to remain vigilant for contradictions, so it seems to me merely a matter of taste and convenience when we choose whether to face up to this at the level of axiomatic set theory as opposed to somewhere "above" it.

Oh, but there are great minds trying quite hard to do just that: exorcise axiomatic set theory. In particular, somebody I mentioned in this thread when we were talking about types.

https://mathoverflow.net/a/9428

[quote=Paul Taylor]
On the subject of categorical versus set-theoretic foundations there is too much complicated discussion about structure that misses the essential point about whether "collections" are necessary.

It doesn't matter exactly what your personal list of mathematical requirements may be -- rings, the category of them, fibrations, 2-categories or whatever -- developing the appropriate foundational system for it is just a matter of "programming", once you understand the general setting.

The crucial issue is whether you are taken in by the Great Set-Theoretic Swindle that mathematics depends on collections (completed infinities). (I am sorry that it is necessary to use strong language here in order to flag the fact that I reject a widely held but mistaken opinion.)

Set theory as a purported foundation for mathematics does not and cannot turn collections into objects. It just axiomatises some of the intuitions about how we would like to handle collections, based on the relationship called "inhabits" (eg "Paul inhabits London", "3 inhabits N"). This binary relation, written ϵ
, is formalised using first order predicate calculus, usually with just one sort, the universe of sets. The familiar axioms of (whichever) set theory are formulae in first order predicate calculus together with ϵ

.

(There are better and more modern ways of capturing the intuitions about collections, based on the whole of the 20th century's experience of algebra and other subjects, for example using pretoposes and arithmetic universes, but they would be a technical distraction from the main foundational issue.)

Lawvere's "Elementary Theory of the Category of Sets" axiomatises some of the intuitions about the category of sets, using the same methodology. Now there are two sorts (the members of one are called "objects" or "sets" and of the other "morphisms" or "functions"). The axioms of a category or of an elementary topos are formulae in first order predicate calculus together with domain, codomain, identity and composition.

Set theorists claim that this use of category theory for foundations depends on prior use of set theory, on the grounds that you need to start with "the collection of objects" and "the collection of morphisms". Curiously, they think that their own approach is immune to the same criticism.

I would like to make it clear that I do NOT share this view of Lawvere's.

Prior to 1870 completed infinities were considered to be nonsense.

When you learned arithmetic at primary school, you learned some rules that said that, when you had certain symbols on the page in front of you, such as "5+7", you could add certain other symbols, in this case "=12". If you followed the rules correctly, the teacher gave you a gold star, but if you broke them you were told off.

Maybe you learned another set of rules about how you could add lines and circles to a geometrical figure ("Euclidean geometry"). Or another one involving "integration by parts". And so on. NEVER was there a "completed infinity".

Whilst the mainstream of pure mathematics allowed itself to be seduced by completed infinities in set theory, symbolic logic continued and continues to formulate systems of rules that permit certain additions to be made to arrays of characters written on a page. There are many different systems -- the point of my opening paragraph is that you can design your own system to meet your own mathematical requirements -- but a certain degree of uniformity has been achieved in the way that they are presented.

We need an inexhaustible supply of VARIABLES for which we may substitute.

There are FUNCTION SYMBOLS that form terms from variables and other terms.

There are BASE TYPES such as 0 and N, and CONSTRUCTORS for forming new types, such as ×

, +, /, →

, ....

There are TRUTH VALUES (⊥
and ⊤), RELATION SYMBOLS (=

) and CONNECTIVES and QUANTIFIERS for forming new predicates.

Each variable has a type, formation of terms and predicates must respect certain typing rules, and each formation, equality or assertion of a predicate is made in the CONTEXT of certain type-assignments and assumptions.

There are RULES for asserting equations, predicates, etc.

We can, for example, formulate ZERMELO TYPE THEORY in this style. It has type-constructors called powerset and {x:X|p(x)} and a relation-symbol called ϵ

. Obviously I am not going to write out all of the details here, but it is not difficult to make this agree with what ordinary mathematicians call "set theory" and is adequate for most of their requirements

Alternatively, one can formulate the theory of an elementary topos is this style, or any other categorical structure that you require. Then a "ring" is a type together with some morphisms for which certain equations are provable.

If you want to talk about "the category of sets" or "the category of rings" WITHIN your tpe theory then this can be done by adding types known as "universes", terms that give names to objects in the internal category of sets and a dependent type that provides a way of externalising the internal sets.

So, although the methodology is the one that is practised by type theorists, it can equally well be used for category theory and the traditional purposes of pure mathematics. (In fact, it is better to formalise a type theory such as my "Zermelo type theory" and then use a uniform construction to turn it into a category such as a topos. This is easier because the associativity of composition is awkward to handle in a recursive setting. However, this is a technical footnote.)

A lot of these ideas are covered in my book "Practical Foundations of Mathematics" (CUP 1999), http://www.PaulTaylor.EU/Practical-Foundations Since writing the book I have written things in a more type-theoretic than categorical style, but they are equivalent. My programme called "Abstract Stone Duality", http://www.PaulTaylor.EU/ASD is an example of the methodology above, but far more radical than the context of this question in its rejection of set theory, ie I see toposes as being just as bad.
[/quote]

In case you missed this lovely bit:

[quote=Paul Taylor]
The crucial issue is whether you are taken in by the Great Set-Theoretic Swindle that mathematics depends on collections (completed infinities). (I am sorry that it is necessary to use strong language here in order to flag the fact that I reject a widely held but mistaken opinion.)
[/quote]

I could also mention the hyperreals as a competing foundation for real analysis (which, in fact, formalizes a model for doing calculus that has a lot more to do with the way Leibnitz and Euler used calculus than what became popular from Cauchy's textbook).

Also, if I am to understand the above passage of Paul Taylor, you likewise can't exorcise category theory!

[quote=Paul Taylor]
Lawvere's "Elementary Theory of the Category of Sets" axiomatises some of the intuitions about the category of sets, using the same methodology. Now there are two sorts (the members of one are called "objects" or "sets" and of the other "morphisms" or "functions"). The axioms of a category or of an elementary topos are formulae in first order predicate calculus together with domain, codomain, identity and composition.

Set theorists claim that this use of category theory for foundations depends on prior use of set theory, on the grounds that you need to start with "the collection of objects" and "the collection of morphisms". Curiously, they think that their own approach is immune to the same criticism.
[/quote]

Now, if we're going to have to choose, which is the more useful foundation? Sets, or categories / types?

Which one is written in a language that mathematicians actually use outside of measure theory and infinite combinatorics?

I mean, naive set theory is a convenient / intuitive tool to reach for, but we also have the category of sets for that!

Paul Taylor continues, clarifying a question of his use of the term "completed infinity".

[quote=Paul Taylor]
Since Tom Leinster queries my reference to actual/completed versus potential/incomplete infinities, maybe we should ask a philosopher whether I am using these terms in the standard way.

In any case, I am not doing metaphysics. I am just describing the way in which it appears to me that mathematicians actually work, in contrast to the way they say they work because they have been trained to say such things. When you compare my remarks with the others on this page, please note that they are based on thinking about these things for myself over 25 years, originally from a categorical perspective but increasingly influenced by symbolic logic, and not on reciting bits of textbooks.

To do ordinary arithmetic, you may need very (arbitrarily) large numbers, but you don't all of them together. So far as I can gather from history, mathematicians up to the mid-19th century managed very well to deal with things in this way, for example defining functions as expressions.

Post-Cantor, 20th century mathematicians got into the habit of introducing the completed infinity before the structure. For example, we say "a group is a set with...", relegating the essence of symmetry to second place. This is like saying that humanity is a collection of pieces of flesh, onto which faces are painted as an afterthought.

Categorists, being part of the pure mathematical culture, did the same thing, in the vast majority of cases with great profit. However, when it comes to foundations, treating the universe first as a completed infinity (and only afterwards containing products, function-spaces, powersets or whatever other structure you require) inevitably leads into the set-theoretic trap.

By contrast, type theoretic methods build up the universe by means of the actual operations that you actually want to consider, just as the symmetry group of the Rubik cube is built up from individual rotations. Moreover, despite the fact that type theory looks completely different from category theory or algebra, it is an accurate underpinning of the actual methods of reasoning of mathematics. See, for example, my discussion of the idiom "there exists" in my book.

This is not dogmatic Finitism or Logicism and is readily adaptable to considering the object N
along with individual natural numbers, an internal category Set

along with individual types, and so on.

Now let me consider the other approaches to this question.

First order logic. This was the first usable general technique in mathematical logic. Like other disciplines, it starts with the completed infinity and adds properties to it. Does it presuppose a set theory? Well, yes, in the same sense that a boot-loader presupposes a primitive operating system. I would be more convinced that first-order logic is independent of set theory if there were a branch of model theory that had examples of structures whose carriers were topological spaces or algebraic varieties.

In fact, first order logic can be set up in the type-theoretic way that I have described above. But if you're going to do that, you may as well set up the type theory that you actually want to use.

If we're looking for a metalanguage specificaly for categorical logic (say, in which to construct toposes) then first order logic is not the right structure. It is easy to describe an internal category in a category with all finite finits, and, by adding more diagrams, we can talk about internal toposes too. However, it's much more interesting to consider free internal structures, for which we need an arithmetic universe, although unfortunately there is next to zero literature on this topic.

Fibrations, 2-categories, etc. None of what I have said contradicts the use of these categorical techniques. I personally consider that fibrations, and especially hyperdoctrines, are obfuscation, but other people find them useful. However, they organise the world, but they do not bring it into existence, which was the thrust of the original question.
[/quote]

I dunno man, but it looks to me like he's doing a pretty darn good job of using type theory to exorcise axiomatic set theory.

Fascinating discussion beginning with a post by a type theorist (and homotopy type theory contributor) and computer scientist (for fun take a peek at his Programming Language Zoo), continued into the comments section, with some splendid tidbits from the likes of Paul Taylor:

[quote=Paul Taylor]
Miha, are you outraged that there could be triangles whose angles don’t add up to 180∘ or that −1 could have a square root?

Are you going to add codicils to the obvious definition of a triangle to prevent Riemann, Bolyai, Lobachevsky and Einstein from subverting your preconceptions about geometry?

Why should computer scientists and algebraic geometers whose spaces are not Hausdorff accept your codicil requiring compact subspaces to be closed? (Or, indeed, Bishop’s that they should be overt?)

As for metric spaces, the symmetric axiom is not needed for the essential development and would seem to be a matter of prejudice. Eric Goubault has shown how to develop directed homotopy theory and apply it to computational processes.

The relativist or pluralist ideas that are controversial now will be accepted as part of the mainstream in due course, exactly as non-Euclidean geometry was by the end of the 19th century.

There is an economic reason for this: Non-classical mathematics is useful in computer science, which is useful to the economy and so attracts funding, which classical pure mathematics increasingly does not. Eventually this message will get through to the best 18 year old mathematicians, who will choose to study modern computer science instead of fuddy-duddy mathematics. Then the latter will die.

Nor is this new. The tradition of mathematics has gone under many names (geometry, astronomy, ballistics) in the past, so it will come to be called computer science in the not too distant future. “Mathematician” will once again mean an astrologer.
[/quote]

I don't necessarily agree with this extreme prognostication, but it certainly is amusing.

Nevertheless, I imagine that Rota would probably count the notion of completed infinity among the wilting myths of mathematics. And axiomatic set theory has completed infinity baked into it, making it an "albatross hanging from our necks".

Incidentally, the thought crossed my mind that by likening axiomatic set theory to the Bohr model of quantum mechanics, Reid had tacitly admitted that axioms can be "wrong", after all.

But then I thought about it further, and I actually don't think this is the case after all. No, the axioms of set theory are not "wrong", but they verge on being not even wrong... and this is much worse, because it swindles people into perpetuating theories that can't easily be exorcised (as Reid said!), no matter how much pathological behavior is being secretly smuggled in by introducing things that are well behaved only insofar as we have thus far detected.

In physics, if we have two competing models for some intuitive understanding of a theory that give divergent results, we presume that one of them is wrong, and use experiment to verify that one is wrong, or is not as broadly applicable as previously thought. But in math, apparently we merely shrug our shoulders and cross out the classes of poorly behaved objects (like non-measurable sets) until we can't see any inconsistencies in our assumptions. Of course this doesn't seem very much like science at all! And after all it's not, since we can't rely on experiment like physics does, but instead were using intuitive perception all along to formulate our axioms.

Now, at this point, if we don't simply throw up our hands and go the pluralist / type theory / category theory route, do as Paul Taylor, and try to simply encode how mathematicians actually use mathematics, we end up falling back to what mathematicians got mired into in the late 19th and early 20th centuries: vaguely conflating intuitive notions that are merely consistent with the axioms. But then, having encoded intuition about infinity formally in something like axiomatic set theory, you end up losing enough precision, so that your choice of axiom system now determines the truth of the same mathematical statements! Whereas in intuitionist logic, no such conflating takes place, because the diverging meanings actually come out to be from different statements! So in a nutshell, axiomatic set theory simply isn't precise enough to avoid unpredictable results.

tl;dr: you most certainly can exorcise axiomatic set theory as formulated by classical mathematicians (with constructivists being the most ardent proponents of doing so), but classical mathematicians don't feel like bothering, because they are comfortable in Cantor's paradise, having built a large, sufficiently consistent edifice inside of it that has had a good track record of helping them produce results. But the fact that something merely works is neither the same thing as being universal or even necessary, and the pluralist point of view shows how the definitive air perpetuated by classical mathematicians is no more than historical convenience and inertia. In religion we call this dogma, and if we acknowledge the historical connection between completed infinity and notions of God, we start to see how axioms encoding notions of completed infinity start to look like commandments written in stone tablets handed down to mankind by a god of the gaps: a vestigial linguistic curiosity encoding early conceptions of the unknown or the infinite, which is by now ever shrinking in scope, as we learn more and more about how nasty its supposedly elegant and pure nature turns out to be in practice.

Interestingly enough, computer programming has experienced the exact same psychological trap of trying to prematurely cram intuitive conceptions of the unknown into some intuitively immediate and supposedly universal machine for thinking about the universe, which turned out to be pathological in practice in many of the most important cases, which was nevertheless was still defended with a religious fervor, but eventually lost to a competing formulation that better reflected correct ways of thinking about the problem, rather than intuitive conceptions of it.

I am talking about object-oriented programming, and its loss to functional programming.

Interestingly, not only did object-oriented programming lose to functional programming, but formal theories of functional programming are more or less the same as those of constructive mathematics, which threaten the dogma of classical mathematics!

Whimsically, we even see that analogies to religious scripture can crop up in object-oriented programming (although of course one can certainly still wind up with similar monstrosities in functional languages by trying to encode the universe into a giant type).

I did put airquotes around wrong, which should suggest something (I'm not admitting mathematical axioms can be wrong, in a strict binary sense). The point I'm trying to get at, and what's the core issue, is when it comes to scientific theory, there's far less binary "right" or "wrong" than our language permits us to allow. Elementary atomic theories you learn in chemistry are "wrong", but they're a good kind of "wrong", in that they serve a useful short hand approximation that's satisfactory for most applications. Scientific theories permit more of these kinds of allowances than we readily admit, quantum theories of the chemical bond are "better" in some sense, they conform more closely to experimental results, but they're useless if your objective is to synthesize a polymer.

So how does that relate to mathematics? Well, mathematics has qualitative differences from any physical science. That being that we don't have experimental data. So we don't have to make that compromise, about the applicability/accuracy of the theory. Instead, we worry about consistency like scientists do, but I can only think the thing we care about is how robust the theory is to explain everything. Moreover, we want the minimal amount of assumptions. Once we do this, though, we find down the pipeline we get undesirably weird/awkward results, just like how some scientific theories are useful approximations for common phenomenon, but then break down on more extreme cases. They're still qualitatively different, because the mathematical theories are never invalidated by weird results (unless an inconsistency is shown), but there is something of an analogy in pushing a theory to its limits.

Maybe something can be gained from using another theory for the foundations of mathematics. Maybe. Maybe homotopy type theory leads to less counter-intuitive results. My suspicion is, there's a bit of a pipe dream among it's advocates, and that if we actually tried reformulating much of math under those auspices, we would run into tons of weird, counter-intuitive results at the periphery. My suspicion is that it's inevitable no matter what axiomatic system you pick that you can get weird things out at the end.

I guess I don't see the necessity in telling mathematicians they need to begin reformulating mathematics entirely differently. I'm not against other people trying and doing mathematics that way, either. It's rather that I'm skeptical of the bombastic rhetoric: history shows that people who seek reductionism in scientific fields are humbled.



Let me make one thing very, very clear: every single physical theory we have is wrong. Every theory has failings, doesn't conform to experimental data, leads us into error. Every one of the top theories we have today will hopefully one day be scrapped. I'm opposed to this idea that, in the past, people's theories were "wrong", because the corollary is that ours are "right". A more accurate statement is that we have new theories which are better at serving particular purposes in science, or that we have more refined, accurate models.

I'm pushing very hard a pragmatic theory of truth here.



Just because there are subjects we don't look at now, doesn't mean they won't be avenues of future, exciting research. Take, for instance, the existence of continuous but nowhere differentiable functions. At the time, they were thought to be a mere curiosity, a weird scourge mathematicians had to push through and accept while they worked with "important" functions.

It wasn't until IIRC the 1970's, over 100 years later, that Mandelbrot began investigating fractal curves as a theory itself. And out of it we were given an absolutely beautiful theory, which has also been taken and used with mathematical modeling techniques to get cool applied math results.

The point is, weirdness in theories seems abhorrent prima facie, but can also be really cool avenues of exploration that lead to total understanding and neat theories later on. The "weirdness" is relative to the observer, and there's no reason to dislike them other than out of some personal bias about what "ought to be". And we all know that people who whine about things based on what they feel "ought to be" make conservative, generally poor researchers.



That seems fine to me, I don't see what the problem is.



Oh, I see. Yes, there's no force in the universe telling us axiomatic set theory is the necessary formulation of the foundations of mathematics, but there's also no force telling us it isn't, and I find the complaints against it generally weak to enforce the proposed result (essentially, restructuring mathematics itself).

lol

Yeah, this is not the case.

Closures And Objects Are Equivalent

The venerable master Qc Na was walking with his student, Anton. Hoping to prompt the master into a discussion, Anton said "Master, I have heard that objects are a very good thing - is this true?" Qc Na looked pityingly at his student and replied, "Foolish pupil - objects are merely a poor man's closures."
Chastised, Anton took his leave from his master and returned to his cell, intent on studying closures. He carefully read the entire "Lambda: The Ultimate..." series of papers and its cousins, and implemented a small Scheme interpreter with a closure-based object system. He learned much, and looked forward to informing his master of his progress.
On his next walk with Qc Na, Anton attempted to impress his master by saying "Master, I have diligently studied the matter, and now understand that objects are truly a poor man's closures." Qc Na responded by hitting Anton with his stick, saying "When will you learn? Closures are a poor man's object." At that moment, Anton became enlightened.

Reid, nobody is telling you how you ought to think about mathematical foundations. The pluralist account says that it doesn't even matter.

I kind of read your long-winded analogy about how axiom systems that pretend to understand completed infinity are somehow immune from criticism because "it's like physical science". (Which in my mind is pretty darn funny, considering how hard you railed against my conception of mathematics as a modelling activity, but I digress.)

I'm still reading your reply, but so far I don't think you've done a good job of defending your claim that any project to exorcise the pathologies of completed infinity in mathematics is going to be futile (you said: "you can't exorcise axiomatic set theory"), whereas I just gave you a bunch of evidence that people are doing just that.

Also, can you clarify how functional thinking hasn't usurped object-oriented programming as the hot new thing? Or do you disagree that the constructivist-leaning mathematicians who are working on both homotopy type theory and programming language semantics prefer category theory over set theory?

I've seen this. Of course it's true.

I'm sure that object-oriented programming as practiced in industry is fine as far as it goes. But don't try to play down the massive amount of hype that it received circa 2000 as a panacea, whereas now we're finding that the functional idiom is far more appropriate for concurrent programming.

Of course, the correct solution in both mathematics and programming is pluralism. What I am arguing against is dogmatic reductionism around the shibboleth of tired panaceas like axiomatic set theory (and this or that programming language paradigm... and yes, functional programers are just as culpable here), which makes ridiculous claims like, "you can't exorcise axiomatic set theory", or that some of its pathologies aren't removed by succeeding in (say) an intuitionistic formulation (they often are).

It sounds like you missed my point that uncontrolled conceptions of completed infinity baked into axiomatic set theory lead to unpredictable results. If your formulation of a vague, intuitive idea gives divergent answers depending on whether or not you assmue this or that axiom isn't a loud and clear message from the universe that your theory isn't really modelling anything at all, but haphazardly enumerating different possible universes of mathematics, I don't know what would be. At best this sort if activity is a waste of time, unless all intuitive interpretations involving infinity are completely jettisoned, and it is seen as a formal game. But at that point, why not just do actual mathematics, rather than pretend that this complex monstrosity you're managed to iron the bugs out of deserves some kind of special status in interpreting mathematical statements?

The pluralist point if view says that, sure you can do axiomatic set theory as practiced by classical mathematicians, but it's really not anything special, and doesn't deserve the preferred status it enjoys, simply because mathematicians have told us to look the other way so many times when it gives unexpected results.

I'm saying you might want to be more humble about this sort of thing.



Nobody's going to start doing analysis over the rationals, dude. I'm kind of surprised after all of this your only course of argument is finitist, given its fringe nature in the mathematics community. I'm not even sure where to begin, but you're going to drop a huge amount of mathematics by trying to exorcise completed infinities. And there's not much to gain except the irrational wanking of a fringe few in mathematics.

Voevodsky may have hoped one day ZF will be shown to be inconsistent, and that may be, but when that happens it happens, I'm not clinging to fringe theories because you can find working mathematicians who would prefer them.



I mean that constructivist mathematics is not going to usurp non-constructive mathematics or usurp the axiom of infinity.

That's all mathematics ever is or ever was. You can reformulate mathematics in another foundation and get rid of completed infinity. That's just as arbitrary and pointless as selecting set theory and rolling with it. There's no substance to what you're saying right now.

The primary difference is axiomatic set theory is more robust, you can formulate and make more claims in it, and say more things. In that capacity, it's a nicer theory, and it's why we use it.



Doing mathematics with completed infinity isn't inferior to mathematics without it, and the "bugs" are not a problem.



A) All foundational theories have unexpected results, b) I am a pluralist, I don't privilege axiomatic set theory intrinsically, c) the preferred status is not a problem, and the "unexpected" results are not a problem.

The criticisms you're making of axiomatic set theory are hubristic. Yes, there are some concerns, some valid things to think about regarding them, but they don't amount to a significant indictment of the current modes of mathematics, nor are they any "threat" or "danger" to the current mode of mathematics, nor are people about to revolutionize mathematics in a way that actually gets rid of the "problems".

Look, I may have oveestated my case here and there to embellish my point, but I think that what I am asking to be considered here isn't much. It's mostly a challenge to dogma, rather than to asset new dogma.

If you just want to get along with mathematics, there's nothing wrong with papering over wonky foundational things that you depend on as working myths, but ultimately don't matter to you. And of course none of means that that work is any less "true". I am only asking that you refrain from perpetuating church dogma that what happens to work for you is somehow universal, preferred, or without blemishes, and isn't worthy of being replaced by brave souls who can actually see a use for a more precise and well behaved theory.

It's hard to be humble when it takes so much effort to get across an important but apparently subtle point!

Saying "mathematics depends on the axiom of infinity" is not really important to me, it's something I grasped and dealt with a while back. I'm concerned though that you're apparently sucked into the finitist conspiracy theory arena of mathematics. Hopefully you don't wander too far down that path and become a Wildberger.

I don't think the goal of homotopy type theory was to show that ZF was inconsistent, but I could be wrong.

A large motivating source of his work in type theory was to help mathematicians find mistakes in their proofs by giving them a formalism that more closely matched the semantics of how mathematics works in practice, rather than wasting time encoding it into low level set theory stuff that is a poor fit for anyway for mathematics (as far as proof checkers go).

And hopefully you don't one day find that your obsolete choice of formalism lets hard to find bugs slip away from you and cause you embarrassment decades later when you realize you had failed to fully formalize what you thought you were proving.

You can pretend that this is just me tilting at windmills here, or you can acknowledge the burgeoning industry of type theoretic proof checkers in mathematics.

Look, I think classical mathematics is a fantastic playground to find new results, and that it is well adapted to intuition. It would be a mistake to give this up just because it can cause you to believe non-sense.

What I am saying is that when you perpetuate dogma about axiomatic set theory and belittle efforts to improve on this, you do so at your own risk.

The pluralist point of view says that you can have the best of both worlds.

lol

FTFY

Voevodsky said once during a talk he hoped ZF would be someday proved inconsistent. That wasn't the intent of HTT, to show it was inconsistent, but Voevodsky himself had some biases.

That's not even a problem. People like him are necessary, new formulations are good. I've had talks with professors in related fields and am considering doing some stuff in HTT. It's not at all something I'm opposed to, in fact, theorem checkers and the topics involved are something I think is important and new.

All I'm resisting is your rhetoric that this is going to be a "revolution" of some sort which overthrows the previous paradigm of mathematics. And I'm resisting the rhetoric of mathematicians who set their sights against the "mainstream" of mathematics. Maybe there's some value in being so pathologically opposed to the mainstream you create cool new results, but generally I see the opposition as needless and wasteful.

Or maybe that's part of the dream of a young scientist, the wishful fantasy best left for the novelization of history: convicted and hardheaded individuals stick to a new theory in opposition to the mainstream and revolutionize a field.

It's a romantic tale, and has happened (we should hope it has), but historically leads more often to crankery, wasted breath and pointless fighting.

Nobody's talking about revolutionizing mathematics, and the criticisms I've made of axiomatic set theory are not mine, and they're not even Zeilberger's. Look at the immense amount of work that Paul Taylor has done to actually improve foundations to be more ergonomic and amenable to writing proofs that are less likely to let non-sense slip in.

I am surprised that you say you are a "pluralist". I am not too familiar with the term, having only learned it from Andrej Bauer's blog post, and am mostly making use of the term in deterence to the view expressed there. If I am not mistaken, though, it is rather uncommon for a mathematician to adopt this point of view, since it means rejecting a lot if the dogma that your initial posts about axiomatic set theory seems to show.

I didn't see it as a revolution, but rather a counterexample to dogma. I agree that I may have started my case in overly strong language.

Having said that, now that I think about it, yes, I absolutely believe that computers will revolutionize mathematics, and that it will be type theory, not set theory, which will make such a revolution possible.

Let me put it this way, if you find this so hard to imagine: was the introduction of Cantor's set theory not a revolution?

I'm not sure I would characterize a comprehensive vision to formulate a more precise language in the interest of squashing bugs as no more than a romantic dream!

While I am not sure I would go so far as to use the word inferior (in many was, classical mathematics is superior, since it is easier), but this really is the crux of our disagreement. And I can't say that I'm at all convinced at your assertion here. Paul Taylor seemed to disagree in some capacity when he called completed infinity a "great swindle" of set theory. Is he a crackpot? His scholarship is impressive enough that I trust he has thought about this more than most apologists for axiomatic set theory have.

Finitism itself is a dogma. People like Paul Taylor are driven out of a dogmatic persistence on the topic. They aren't necessarily wrong, either, because this isn't a right or wrong stance to have, mathematically speaking. The differences amount to something of a philosophical difference about what constitutes mathematics, and of all people in mathematics, finitists are by and large the most dogmatic that their preferences on the topics are the best ones.

Most mathematicians don't care that much, because it is not very useful or important.

Visions never become the realities they strive to be.

This paragraph is merely crypto-apologia for mainstream assumptions about the state-of-the-art in foundations. Foundations is most certainly an active topic of research, and arguing against its vigorous development is basically lazy conservativism.

There is no reason to feel that new foundations pose any kind of threat, or that they will require new kinds of thinking. At best, if they become mainstream, they will simply require a new language for you to learn when encoding what you already believe, and you may then find some bugs or ambiguity that you hadn't been paying attention to before, possibly leading to divergent statements of things that had previously been presumed to be indistinguishable (can the Hahn-Banach "paradox" happen in intuitionistic logic? I doubt it).

Bull****.

The person who set out to write Coq (or Agda, or HOL, or ACL2, or ...) had a goal, and they formulated a strategy to implement a path toward that goal that they implemented in software, and which have delivered on their stated objectives of formulating mathematics in precise enough language to uncover bugs that had hitherto been difficult to find.

Of course there have been revolutions. Homotopy Type Theory could conceivably be one. I don't deny these possibilities.

Have you ever heard the adage "don't count your chickens before they hatch"? Or "don't fix what ain't broke"? Classic wisdom applies here. I'm not dogmatically against HTT or finitism, nor am I dogmatically for ZF, on the contrary, it seems you don't recognize the blatant dogmatism of the people who are writing these rants about ZF.

Oh yeah, maybe Coq will be a revolution. Maybe. I'm not writing down the future based on a possibility, one that's historically rare. I'll leave that dogmatism for you to explore, for now, I'm comfortable where I am.

We get it, you've become sort of a crank about mathematics. I'm not sure there's anything much more to say on the subject.

So mathematicians have their own private dogmas that drive their own research.

I can hardly be sympathetic toward people who would equivocate personal beliefs that drive research programs to conservative apologia for mainstream dogma about old technology being "good enough".

Your last sentence applies to almost all of mathematics. It's also factually wrong, because the reason they don't care has more to do with the immaturity of the state-of-the-art art proof checkers, poor ergonomics, and a mismatch with existing mathematical language. Give it 50 years and then look around and see if people are still clinging to axiomatic set theory as a way to dismiss a formulation that happens to be better at finding bugs in proofs.

Also, if we're going to be casting aspersions on research projects because of private philosophical motivations, I'll have you know that Godel was a hard-core Platonist.