4
$\begingroup$

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).

$\endgroup$
7
  • 4
    $\begingroup$ Well, the thing is that negating a universal axiom only demands there to be one counterexample. So for instance when negating the axiom of extensionality the universe might look largely the same, except for some extremely high rank counterexamples. In particular, you probably shouldn't expect these negations to have many interesting consequences. This makes the question not that different from asking what can and can't be proven without extensionality whatsoever. $\endgroup$
    – Wojowu
    Commented Jul 7 at 19:42
  • 2
    $\begingroup$ Tim Button and I are currently writing a paper on this topic in the case of extensionslity, but it is too soon to share fuller details. $\endgroup$ Commented Jul 7 at 19:42
  • 1
    $\begingroup$ @Wojowu You beat me to it -- hopefully the edit addresses these concerns somewhat, albeit in an ambiguous fashion. $\endgroup$
    – Alec Rhea
    Commented Jul 7 at 19:43
  • 3
    $\begingroup$ Equal sets always have the same elements. That's a property of equality in classical logic way more fundamental than any axiom. $\endgroup$
    – Wojowu
    Commented Jul 7 at 19:45
  • 3
    $\begingroup$ Extensionality is the other implication: sets with the same elements are equal. $\endgroup$ Commented Jul 7 at 19:47

3 Answers 3

9
$\begingroup$

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.)

$\endgroup$
5
  • 2
    $\begingroup$ I take Scott's theorem mainly to show that that isn't what we should mean by ZF-Ext. He achieves replacement simply by ensuring that there is never a unique witness, since there will be plenty of automorphisms of the universe. So you can get a model of this by starting with Z and duplicating objects hereditarily. But you'll not get collection this way. So the situation is rather like ZFC- and ZFU with regard to the issues with replacement. To my way of thinking, collection is part of ZFC, and we don't intend to give it up just because we give up power set or allow urelements. $\endgroup$ Commented Jul 7 at 21:56
  • 3
    $\begingroup$ It is a similar issue with ZFfin, where you can't just throw out infinity and accept the negation. You have to also improve regularity to the $\in$-induction scheme to get the theory that should be intended. In general, removing axioms from a theory involves some reflection about what at bottom the theory really is. Sometimes axiomatizations are a certain optimized list since it would be redundant to have certain other axioms on the list, even when those things are core commitments. But when removing axioms, you often want to keep these other commitments, when they are no longer equivalent. $\endgroup$ Commented Jul 7 at 21:59
  • 4
    $\begingroup$ @JoelDavidHamkins That's fair. That said, I would still claim that the surprisingly-low consistency strength of $\mathsf{ZF^{rep}-Ext}$ is notable independently of the much-better-motivatedness of $\mathsf{ZF^{coll}-Ext}$, if only as a general technical warning. I don't think this necessarily disagrees with any of the points you've made of course! $\endgroup$ Commented Jul 7 at 22:37
  • 2
    $\begingroup$ For example, the only reason separation and collection aren't on the axiom list is because they are provable from replacement, so we don't need them if we have replacement. But this redundancy is no longer possible when you drop power set or extrensionality, and so we must revisit the question of what theory we intend to be talking about. Who cares about some weird theory that arises by omitting axioms from a list that was optimized for reasons that are no longer in effect when that axiom is omitted? And I don't actually care about optimizing the axiomatization in the first place. $\endgroup$ Commented Jul 7 at 23:19
  • 1
    $\begingroup$ Ah, my latter comment was posted as a continuation of my previous comments, before I saw your comment, Noah. $\endgroup$ Commented Jul 7 at 23:20
6
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ Can you give at least the titles of the works you cite, if not links? Thanks $\endgroup$
    – David Roberts
    Commented Jul 13 at 11:02
  • 1
    $\begingroup$ I thought the description was a pretty unique description, but here you go. $\endgroup$ Commented Jul 13 at 19:41
  • $\begingroup$ oh, it was a unique description, but for the purposes of decreasing friction for people who either want to read, or are even just curious, giving more information and links is helpful. I guess by Sam Buss' book you mean mathweb.ucsd.edu/~sbuss/ResearchWeb/BAthesis/… ? $\endgroup$
    – David Roberts
    Commented Jul 14 at 5:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.