Negating fundamental axioms

Question

It is commonplace to consider standard axiomatic systems (e.g. $ZF$) with one of the 'less essential' axioms negated, like infinity, 'less essential' here having some ambiguous definition related to an individuals intuition and philosophical preferences.

Has there been any work done exploring what happens if we negate 'essential' axioms?

For example, what about $ZF$ with the axiom of extensionality negated?

My vague understanding of type theories is that axioms do not play such a central role, replaced largely by rules of inference (which are essentially axioms about reasoning instead of the objects of the theory, as far as I can tell? [*cue dunce cap]). But even in this setting, I think it is a coherent question to ask 'what if we take the negation of one of the 'essential' rules of inference as the rule instead?'.

This question is asked mostly as a lark; I am curious what the mathematical universe looks like when we explore a version of it with core pieces of our intuition 'reversed'. Any pointers are appreciated.

---

In my original edit, I claimed that just negating outright for universal axioms 'wouldn't have any interesting consequences' (which is wrong, see Noah's answer), and also that we might instead negate something like extensionality by claiming that equal sets never have the same elements, which is always wrong (see Wojowu's and Naïm's comments).

Answer 1

In my limited experience (which may soon be changed! :P), merely negating "fundamental" axioms does not yield strong in-system consequences. The word "merely" is doing some work here, though, since of course we can do more than simply add the negation of an axiom; e.g. Boffa's antifoundation axiom implies that every theory has a transitive model which is rather amusing, and similarly if we think of the axiom of determinacy as a strong anti-choice axiom then of course ZF+AD proves interesting new facts.

However, the resulting systems themselves may have surprising properties. In the particular case of extensionality, Scott showed that $\mathsf{ZF-Ext}$ (phrased using $\mathsf{Replacement}$ rather than $\mathsf{Collection}$) is equiconsistent with $\mathsf{Z}$, so adding extensionality to $\mathsf{ZF}$ results in a huge increase in consistency strength; one consequence of this (which I can't elaborate on, not being familiar with Scott's proof) is that there must be models of $\mathsf{ZF-Ext+\neg Ext}$ which are "much simpler to build/verify" than any models of $\mathsf{ZF}$. This doesn't contradict the previous paragraph, though, since this interesting result isn't a new theorem of $\mathsf{ZF-Ext+\neg Ext}$ but about $\mathsf{ZF-Ext+\neg Ext}$.

(If you shift from $\mathsf{ZF}$ to $\mathsf{NF}$, we get another example in Specker's theorem that $\mathsf{NFC}$ is inconsistent while $\mathsf{NFUC}$ - which is to say, $\mathsf{NFC-Ext}$ - is consistent.)

Answer 2

I just wanted to point out as a comment that there is some ambiguity, already mentioned by Joel David Hamkins, about what it means to "negate fundamental axioms" (there is some further discussion here). The issue is not with the negation per se, but rather with what it means to "subtract" axioms from a theory.

Let me try to give a toy example of what can go wrong. A strict partial order $<$ on a set $X$ may be defined as a relation on $X$ satisfying the following three axioms:

1. Irreflexivity: there does not exist an $a\in X$ such that $a<a$.
2. Asymmetry: for all $a,b\in X$, if $a<b$ then it is not the case that $b<a$.
3. Transitivity: for all $a,b,c\in X$, if $a<b$ and $b<c$, then $a<c$.

It turns out, however, that the asymmetry axiom is redundant, in the sense that if a relation $<$ on $X$ is irreflexive and transitive, then $<$ is asymmetric. Thus, we could have defined a strict partial order to simply be a irreflexive and transitive relation.

Now, if someone speaks about "the theory $T$ of strict partial orders without the irreflexive axiom", then what could they mean? If we axiomatise strict partial orders as being relations satisfying (1)-(3), then $T$ is identical to the theory of strict partial orders, since irreflexivity can be deduced from asymmetry (take $a=b$ in (2)). On the other hand, if we axiomatise strict partial orders as being irreflexive and transitive relations, then $T$ is simply the theory of transitive relations, which is clearly not the same as the theory of strict partial orders.

If we go further and consider "the theory $S$ of strict partial orders with the irreflexive axiom replaced by its negation", then either $S$ is an inconsistent theory, or $S$ is the theory of transitive relations $<$ for which there exists an $a$ such that $a<a$, depending on what is exactly meant by $S$.

Similar problems arise in set theory. In a number of set theory texts, the axiom of pairing is omitted from the $\mathsf{ZFC}$ axioms, since it can be deduced from replacement. But this presents an issue when we want to consider Zermelo's theory $\mathsf Z$, since we want $\mathsf Z$ to have pairing, but not replacement. Describing $\mathsf Z$ as "$\mathsf{ZFC}$ with replacement and regularity removed" can easily lead to confusion.

Answer 3

At the very bottom of logical strength, there is the following example.

Julian Hook's PhD thesis with title A Many-Sorted Approach to Predicative Mathematics, written under the supervision of Ed Nelson (and available from ProQuest) explores the development of weak arithmetic/analysis assuming the negation of the axiom

the exponentiation function is total on the natural numbers. (*)

Of course, the negation of (*) is consistent with e.g. bounded arithmetic.

I believe people later showed that the same results can be obtained without assuming the negation of (*). This is discussed in Buss' book on Ed Nelson's research, if memory serves.

My experience in reverse math is the same: Dag Normann and I have shown that fairly strong systems are consistent with

there is an injection from the real numbers to the naturals. (**)

However, the axiom (**) does not yield any interesting results/alternative development of math/faster proofs, et cetera, as far as I know.