I have recently read some stuff about type theory and category theory. But I still find it hard to imagine what it practically means for type theory or category theory to be the foundation for mathematics rather than set theory, so here is a question that might make it more concrete for me:
Where does predicate logic stand in this "mexican standoff"?
Option 1. Predicate Logic is firmly on the side of Set Theory, and would die with it. That is, category theory and type theory as foundations of mathematics don't need predicate logic at all.
Option 2. Predicate Logic is completely neutral, and would survive the fight unscathed no matter the outcome. That is, all three of them rely on predicate logic.
Option 3. Something more complex entirely.
Answer
tl;dr Other than classical versus constructive, which is somewhat orthogonal to set theory versus category theory versus type theory, first-order logic is a common denominator upon which nearly everyone agrees, and so it is not going anywhere.
I suspect the reason you find "hard to imagine" different foundations is because you expect dramatic difference whereas, in practice, for most mathematicians almost nothing would change. With the amount of fudging that is going on in most mathematical arguments, it would likely be about as difficult to formalize them into set theory as it would to formalize them into type theory. For example, technically if you wanted to prove something like the Fundamental Theorem of Arithmetic in set theory you have to explicitly define the natural numbers (and everything else) as a specific set, prove the result, and then prove that the result doesn't doesn't depend on the specific definition of "natural numbers" that you used, i.e. that it is isomorphism-invariant for a suitable notion of isomorphism. This is rarely done. In practice, mathematicians usually work in a way that is quite natural from a type theoretic perspective and they only work with an "interface" to the naturals from which isomorphism-invariance readily follows. On the other hand, basic set theoretic notation and ideas are often used and those don't always map trivially to type theoretic notions. So something like $x\in A\land x \in B \implies x \in A\cap B$ would "really mean", from a type theoretic or categorical perspective, something like "we have an $x:C$ and given an injective $i : C \to A$ and $j : C \to B$, then there is an injective $k : C \to A\cap B$ such that $\iota_1(k(x))=i(x)$ and $\iota_2(k(x))=j(x)$". However, this suppression of implicit conversions is present in set theoretic reasoning. Von Neumann naturals are not equivalence classes of Cauchy sequences so $\mathbb N \not\subseteq \mathbb R$.
A switch from classical logic to constructive logic would be more impactful, but this is technically orthogonal to set theory versus type theory. There are constructive set theories and classical type theories. Even then, most of the time constructive logics are compatible with classical logics, so constructive proofs are classical proofs and classical proofs are embeddable into constructive logics and still have some relevance. There's also not going to be some flag day where all mathematicians cast aside their classical or set theoretic proofs and and only accept constructive type theoretical proofs. Instead, any shift in what the "foundations" of math are will occur as a shift in focus and interest. Set theory will never die.
In an answer to a recent question I cover some other misconceptions related to this, though that's by no means exhaustive. Some aspects more directly worded toward your question is: There is no "Mexican stand-off" between set theory, type theory, and category theory. It's not a zero-sum game. Indeed, they often feed into each other. For example, Cohen's technique of forcing used to prove the independence of the Continuum Hypothesis from ZFC has been recast using topos theoretic techniques.
To finally start getting around to your actual question, I'm going to take "predicate logic" to mean "classical first-order logic" (FOL). Clearly, as presented, ZFC and other common set theories are built on classical first-order logic. They are first-order theories. You could take a philosophical position that set theory "really exists" in some Platonic way and that the ZFC axioms are just a wan description of this Platonic "reality", and then logic derives, presumably, from model theory and so set theory is prior to logic. I personally find such lines of thought completely uncompelling. On the other hand, one could say that the ability to manipulate logical syntax already presumes set theoretic notions. While it is clear that what it takes to manipulate formal syntax is at least as complicated as what it takes to manipulate natural numbers, and so it makes little sense to talk about logic providing the "meaning" of natural numbers, say, what is necessary is not set theory. Even cast into set theoretic terms, only a very weak fragment of set theory would be required. So, in my opinion, the only reasonable position to take is that part of the definition of ZFC set theory is FOL, but FOL doesn't need ZFC set theory.
Category theory is usually presented as being built from set theory and with no foundational pretensions. For example, Mac Lane starts "Categories for the Working Mathematician" with a discussion of set theoretic foundations and the definition of a category in terms of them. The theory of categories is a first-order theory, in fact, even more narrowly an essentially algebraic theory. However, we're interested in models of the theory not the theory itself which is where the set-theoretic issues come in. This is exactly analogous to, say, group theory. We can axiomatize as first-order theories, narrower and narrower classes of categories. In particular, elementary toposes (with NNO) which enable modeling constructive set theoretic reasoning and even more particularly ETCS which is comparable to ZFC (a little weaker) though presented quite differently. Often when one speaks of "categorical foundations" in a way that's actually on par with set theoretic foundations, they actually mean topos theoretic foundations (or possibly closely related classes of categories such as list-arithmetic pretoposes). Lambek's and Scott's Reflections on the Categorical Foundations of Mathematics(draft) is an excellent illustration of how these various approaches to foundations interact and an excellent illustration of these approaches feeding off each other. It discusses the free topos which is an extremely natural object categorically and is intimately related to intuitionistic type theory. Adding a few axioms will give you basically ETCS, a classical set theory. However, some important results about the free topos require a classical meta-theory, i.e. a set theory! I highly recommend this paper. At any rate, ETCS, for example, relies on FOL in exactly the same way as ZFC.
Type theory, on the other hand, is not a first-order theory. Instead, type theory is better thought of as an extension of logic itself. Most type theories put forward as systems in which we might be able to do "all of math" are usually effectively some form of higher-order logic. All of these systems (which is not all type theories by any means) don't replace so much as subsume intuitionistic first-order logic. If they are classical, then they subsume (classical) FOL. I don't know if you'd view this as "predicate logic dying". Certainly all the intuitionistic/classical FOL reasoning would remain valid. It would still be interesting to know about systems that can be described in purely first-order terms and the nice meta-theoretical properties of FOL would still be valuable for systems so expressible, just like it is interesting nowadays to know whether a first-order theory can be expressed as an algebraic theory or not. Set theory is in some sense an "implementation" of higher-order logic in first-order logic. These type theories deliver such features much more directly. As for category theory, my view is roughly that category theory is to type theory as model theory is to logic (though this wasn't by design, unlike model theory).
No comments:
Post a Comment