Ever heard of Ludwig Wittgenstein, the guy who popularized truth tables? Check out his little known work "on the foundations of mathematics." beautiful stuff.

-- an analytic philosopher

Yes, I believe undergrads(!) cover this in Honors Advanced Truth Tables at UChicago.

Well,

I don't think it really matters whether he's talking set theory or category theory because the way he talks about set theory implies to me he'd have similar problems with category theory.

For example, he describes the result of Godel and Kohen, who together showed the continuum hypothesis is independent of ZFC, as being a failure/problem of ZFC. It's not. That you have significant theories that are independent of a given axiom system is a product of Godel's theorem. Modern mathematics operates with the assumption that most theories are true, false or unprovable.

But the situation also isn't specific to set theory. Any formal system is going to be subject to this "problem"

The thing is this state of affairs isn't appealing to the intuition. Godel himself was unhappy with his result. But it is basically inevitable if you get to the level of rigor of a formal system.

>But the situation also isn't specific to set theory. Any formal system is going to be subject to this "problem"

I think that part of the author's point can be read generously as, "no formal system can satisfy philosophy's pseudo-religious search for truth evident in itself."

Well, that's a problem for the pseudo-religious search, not for mathematics.

My hope is type theory will be the future adopted foundational system as it allows easier computer-checked proofs and a marriage of mathematics and computation. Category theory can then be formalized within type theory.

Intuitionistic logic and intuitionistic type theory follow essentially the same set of rules, so how does type theory allow for a "marriage of mathematics and computation" any more than logic, which everyone already uses?

Because conventional mathematics, whether based on set theory or some categorical alternative, has (usually classical) logic as a background theory. In type theory, that's all you need. It is a theory of computation that has a "built-in" logic. And there's more than just intuitionism. There are type theories that model non-constructive/classical logic and are yet still computable programming languages. So we can write computable code and prove properties about that code in the same theory.

> There are type theories that model classical logic and are yet still computable programming languages.

Thanks, but this seems absurd to me. Please elaborate!

I'm not an expert, so please take the following with the grain of salt.

One of the examples of computation formalisms providing the classical logic at the type level is the Parigot's [λμ-calculus](https://en.wikipedia.org/wiki/Lambda-mu_calculus). λμ-calculus adds μ-abstraction to the classical λ-calculus.

μ-abstraction resembles the notion of continuation. With that addition Peirce's law of classical logic becomes deductible without any modifications (e.g. double-negation translation). The program that proves Peirce's law is just call/cc function.

This topic seems to be an ongoing research, so you may find lots of articles in public internet space. Many interesting introductory articles are among the advanced materials of [this course](https://www.cs.ru.nl/~freek/courses/tt-2011/), including the original Parigot's paper.

There are a number of different type theory models for classical logic. The first to my knowledge was a model that uses the call-with-current-continuation (call/cc) control flow operator. While this does model classical logic, some say it is not particularly useful as a practical programming construct, which is perhaps why it does not seem to be adopted by any major proof assistant. More recently I've seen a few papers showing that type theoretic models of concurrency can also model classical logic, e.g. see "Classical Proofs as Parallel Programs" < https://arxiv.org/abs/1809.03094 >. The original idea that the Curry-Howard correspondence only applies to intuitionist logic is wrong.

> Since it is being gradually replaced by category theory as a more modern, practically better, and a more powerful foundation of mathematics

i don't see this. set theory is very practical and is a good thing to use to build things up in a granular manner. category theory is useful to connect and relate things. they're at two different ends of the spectrum. category theory isn't "replacing" anything.

The truth is, at least since the early 1960s category theory has been a much, much more powerful tool in many branches of modern mathematical research than set theory. (By the way, it can be an enlightening exercise, to try and restate the simple notions about sets purely in terms of maps - notions like 'B is a subset of A', 'C is a union of A and B', 'map f is injective/surjective', 'C is a Cartesian product of A and B', etc. Highly recommended!) Category theory is very deep and easily subsumes much, if not all, of set theory. The difference in power is staggering. Sets in general are now considered just one of many categories and play a subordinate role. I agree that set theory is more useful when studying math at an elementary level, but the sooner one starts getting used to categorical ways of reasoning, the better one's chances to make progress in understanding modern mathematics.

you're missing the argument i made. i didn't say category theory isn't useful or powerful. i said it isn't replacing set theory in practice.

you can make it through the lion's share of a ph.d. in math without using category theory, but you'll use set theory ubiquitously up until you start doing categorical things. of course category theory is a powerful relator. but it is awkward for when simple sets do just fine. loring tu's manifolds book is a good example of this. set theory is used throughout with categorical concepts sprinkled about to show there's power of relation there.

and that's what i said. set theory is helpful as a brick. category theory is helpful as an architect.

In their attempt to remain relevant, (amateur) philosophers will take anything and run with it, sometimes totally incorrectly.

There's a special place in face-palm hell for philosophers who've argued that Godel's Incompleteness Theorems place a fundamental limit on human understanding.