# How do we arrive at stronger theories in mathematics/logic?

A reasonable aim of formal mathematics/logic is to build systems which can "interpret" many things. As an example, ZFC can interpret a number of things. Incompleteness Theorems provide us with a conclusion that there are inherent limitations in formal systems. Turing's doctoral thesis (Systems of Logic based on Ordinals) explored this idea where we can overcome this inherent incompleteness by appending these unprovable formulae to existing system to arrive at a more complete system.

But it appears to me that there is nothing much remarkable in employing this strategy for arriving at more general system/stronger theory. Ideally, we should be making system much more general not by adding stuff piece by piece, but by "expanding" the system more generally. I read somewhere Godel suggested looking for stronger axioms of infinity.

My question is the following: how do mathematicians/logicians devise more general systems? What kind of things do they keep in mind when they step out to expand their systems? What are the ground rules to build general systems (or stronger axioms?) which can interpret my current system (and much more)?

• Regarding ur "I read somewhere Godel suggested looking for stronger axioms of infinity", can u elaborate which source or paper recorded this suggestion? I found a paper which may be relevant for ur interest (logic.harvard.edu/EFI_Woodin_StrongAxiomsOfInfinity.pdf) Apr 30 at 20:11
• Since any first oder theory is not just incomplete but incompletable there is no difference between "expanding the system more generally" and "appending unprovable formulae piece by piece". New large cardinal axioms are just such unprovable formulae, and the theory stays incomplete no matter what is appended. For motivations and informal heuristics that drive mathematicians, including Godel, to devise new axioms see Maddy, Believing the Axioms I and II. Apr 30 at 21:01
• Yay for mentioning Turing's all-but-forgotten doctoral thesis. What I heard is that he didn't like Princeton and didn't like working w/Church, and returned to England and never went back to the fascinating topic of his thesis. Apr 30 at 21:20
• @DoubleKnot I am unable to recall the paper right now. shall post the link if I do.
– Ajax
May 1 at 5:23
• @Conifold, I agree that effectively there is no difference, but I am interested in the task because expanding more generally is not a trivial task (unlike appending Godelian formulae -we now know how to do that, and therefore it has a more mechanical nature to it and hence nothing much remarkable). It is the possibility of a non-trivial jump that has caught my attention, and the general heuristics one may keep in mind should one attempt anything of that sort.
– Ajax
May 1 at 11:17

Maybe you should begin by acknowledging the much that has already been done, since we are not reinventing the wheel. Relative to this, your question is not an open question as such, since the subject of category theory, usually described as the mathematics of mathematics, already exists. Firstly, I will make a point clear, that set theory is just a special kind of category and so are many (if not all) other branches of math, it is the universal language of mathematics. We should take the lessons learnt from category theory seriously, that everything is necessarily described by duality as has been captured by famous category theory quotes like "adjoint functors arise everywhere" or "every concept is a Kan Extension". Category theory is the theory of duality and there rests its power and the generality of adjoint logic which subsumes most (if not all) other logics. Mathematics is necessarily formalized in other mathematics, and the best way to see this is via the lens of type theory. That is, all formalization is not arbitrary but follows a fixed template

``````1. formation rules
2. Introduction rules
3. Elimination rules
4. Computation rules
``````

These are rules in type theory that define how syntax is to be manipulated and their stipulation consists the metatheory which is usually treated implicitly in less formal math like an ordinary treatment of set theory. For instance, normal set theory treats the background first order logic informally but type theoretic formalization is mechanical enough to be executed on a computer. This universal template is exactly duality in category theory and by the proposition above "Category theory is the theory of duality", it follows then that the best shot at universal mathematics is the formalization of category theory in-itself or the template in-itself. Not easy for non-mathematicians but Voila !! I wouldn't however fix anyone's thinking, this answer is open to criticism for the better.

• Elementary topos is the basic category of sets and working within this topos is equivalent to using traditional set-theoretic mathematics. I guess to convince philosophers to use topos one needs to see its advantage over sets in terms of predicativisim (avoid self-reference) and completeness/compactness... May 5 at 18:16
• Not so, elementary topos is more general than the category of sets(not equal) and elementary topos is a special kind of category. I did not mention topos theory anywhere, just category theory. Besides that, the OP asked for generality and that doesn't consist in arbitrarily taking sides to avoid anything. May 6 at 5:57
• "More recent work in category theory allows this foundation to be generalized using topoi; each topos completely defines its own mathematical framework. The category of sets forms a familiar topos, and working within this topos is equivalent to using traditional set-theoretic mathematics." (from topos wikipedia) I'm just curious if category theory can show some concrete advantage over ZFC or type theories via concrete philosophical example(s) since it as a formal system has same restrictions as others such as incompleteness. Predicate (logic) is also the theory of duality and arise everywhere. May 6 at 6:12
• ...every quantified variable in FOL is also a restricted extension within its universe. And your last paragraph seems suggest a hybrid of some type theory (HoTT or simply typed?) and category theory given their intimate relations, however, still seems abstract and vague at this level to show its universal philosophical advantage over traditional foundations. (Of course it showed its advantage in some specific area such as algebraic geometry and certain other math fields.) May 6 at 6:25
• Here's the point you are missing, whenever one studies a mathematical theory they are only deducing the theorems that follow from that particular theory and its sub-theories and cannot reach the theorems of weaker theories, e.g tourists exploring at ground level have limited scope of view (particularised theory), but if they raise their altitude, say in a hot air balloon, they get a wider perspective (less particularised theory). Deduction is comparable to line of sight and they cannot see more than their altitude allows them to. May 6 at 11:55

It's very simple. Take a mathematical system where a statement S cannot be proved to be true, or proved to be false. You can then add either S or (not S) as an axiom to your mathematical system and get a stronger system in which S is trivially proven right, or trivially proven wrong.

As far as Gödel's theorem is concerned, this doesn't make the slightest difference. There will be another statement that cannot be proved true and cannot be proved false. We can create stronger systems all day, they still have the same fundamental problem.