The standard foundation we have in mathematics today is ZFC set theory and classical logic. But there have been a number of theories, whose proponents criticize ZFC. There are ultra finitists, who criticize pretty much everything about ZFC. Other people just criticize the Axiom of Choice. Then there are advocates of intuitionistic logic, who despise using the Law of Excluded Middle.
When I hear these mathematicians speak about their views, the question I've always had is: "Yes, but what do we actually gain by weakening our system?" If the reasons to reject ZFC are philosophical, I'm not persuaded. I choose pragmatism over philosophy since I'm an anti-realist and so choosing my axiomatic system doesn't violate some kind of objective, holy laws of the universe.
But if considering weaker systems have actually interesting implications, that's an another story. So, I would like to know whether there are actually any interesting theories developed in a weaker framework than ZFC that one can't have in ZFC. I do know that constructive mathematics is very useful, when writing theorem provers, but I'm more interested in the pure maths side of things.
Thank you!
The most classical way of $A$ being weaker than $B$ is $A⊢φ⇒B⊢φ$ (and, of course, strictly weaker is when the converse is false).
When we look at it like this, we may think that this means that a weaker theory is less interesting, as the weaker theory cannot prove anything new.
Interestingly enough, another equivalent) way to look at it is $\mathcal M⊨B⇒\mathcal M⊨A$.
This point of view actually gives us the opposite, $A$(the weaker theory) looks actually more interesting, as there exists models of $A$ that are not model of $B$.
Because of the first formulation, I, personally, find it boring to just assume less. But I do find it interesting to see what happens in those models of $A$ where $B$ fails.
To explore those models, instead of just taking just a weaker theory, we also add a new axiom which contradicts the original theory.
For example, instead of looking at ZF instead of ZFC, we can look at ZF+¬AC. Those 2 theories are not stronger nor weaker from one another and both contains rich* structures that the other one doesn't have**.
For me, exploring ZF is, among other things, exploring both ZFC and ZF¬C.
* We need to actually be a bit more careful about what we mean here, as ¬AC is deceivingly uninteresting. We usually explore stronger "anti choice" axioms, or combining the 2, like "ZF+¬CC" and "ZF+DC+AD".
** Like I said in my previous point, ¬AC by itself is deceivingly uninteresting, we don't actually know much about what kind of new structures it has, we know, for example, that there is a vector space without a basis, but we don't know a lot about this vector space itself.
Because we are mathematician, it would be too simple if we would simply leave it at this, so we invented few other ways to "measure" strength. The 2 most known other methods is consistency strength(which I am talking about bellow) and proof theoretic ordinal(which I am not familiar with).
We say that $A$ is weaker than $B$ if $Con(B)⇒Con(A)$, by this definition ZF and ZFC are both the same strength, but Z, for example, is weaker.
This view about strength has more philosophical view but it does open up a new tool in our toolbox. The most obvious result is Gödel second incompleteness theorem: No (sufficiently strong) consistent theory $T$ proves it's own consistency.
In other words: $T\nvdash Con(T)$. This is, apart from a huge deal breaker in philosophy of mathematics, a very interesting result about formal theories and what we can and can't do with our theories(one of those theories is ZFC, but not limited to it)