1 Introduction
Weber in [Reference Weber18, p. 282] presents a proof of Cantor’s theorem within a “paraconsistent set theory” based on a relevant logic. His proof goes via a well-formed formula of the form
employing some specific paraconsistent tools, in particular “the routley reduct of any X,
$$\begin{align*}\mathcal{R}(X) := \{ x : x \in X \land p \} \end{align*}$$
where p is any proven contradiction” ([Reference Weber18, p. 270], such as, above all, Russell’s paradox
.
For Weber “[r]elevant logics are a robust choice, in the sense that they feature an implication connective
$\to $
that obeys modus ponens” and he states explicitly that “set theories based in other paraconsistent logics, like Priest’s
$LP$
(Priest, 1979), … have no ‘ponenable’ conditional, and are not considered here” [Reference Weber18, p. 270]. In view of this I wish to emphasize that my first point here is that despite this lack of a ‘ponenable’ conditional in Priest’s
$LP$
a proof of Cantor’s theorem can be obtained on its basis with only unrestricted abstraction added (i.e., no extensionality) somewhat along Weber’s lines.
My second point is that it is possible not only to prove Cantor’s theorem in Priest’s logic of paradox endorsed with unrestricted abstraction, but also that it doesn’t hold for non-empty sets.
Priest’s logic of paradox can actually be given a very simple and completely straightforward sequential formulation as Gentzen’s
$\mathbf {LK}$
without cut which was pointed out as early as in [Reference Priest8],Footnote
1
but which never seems to have been given much credit in practice, not even by Priest himself. In order to keep things as simple as possible, I shall use here an intuitionistic version, i.e., I take Gentzen’s sequential formulation of intuitionistic logic
$\mathbf {LJ}$
without cut as a basis and just add unrestricted abstraction to form a system of naive property theory which I label
.
So my aim is firstly to prove
$\dagger $
in
, i.e., without relevant implication or any form of modus ponens, and secondly to prove by similar methods that no non-empty set actually satisfies Cantor’s theorem. To that end any dialetheia will, in fact, be sufficient, meaning there is no special need for a “routley reduct”.
Finally, there is one aspect of Cantor’s theorem that I want to mention, not least because it may serve as a link to my own approach to the paradoxes of set theory. It is well-known that Russell discovered his paradox by analysing Cantor’s theorem for the case of the universal set.Footnote 2 This is what I took as a starting point for my approach to dialectical logic in [Reference Petersen, Becker and Essler4]: if we take the universal set, then identity is a bijective function that contradicts Cantor’s theorem. Classical set theorists reacted to this by excluding the universal set from the realm of sets. In a set theory based on a paraconsistent logic the possibility of allowing a universal set turns Russell’s example into a paradigmatic dialetheia. While this may be understandably welcome to dialetheists, my point is that it doesn’t stop there. In a paraconsistent logic with unrestricted abstraction dialetheias threaten to multiply uncontrollably. In this sense the present paper can be seen as continuing the line of [Reference Petersen6]: Priest’s logic of paradox endorsed with unrestricted abstraction leads to unsavoury results.
2 Technical preliminaries
I assume a basic familiarity with Gentzen’s sequential formulation
$\mathbf {LJ}$
of intuitionistic logic as introduced in [Reference Gentzen2] (translated in [Reference Szabo16]) and also introduced in the first chapter of [Reference Takeuti17].
Definition 2.1. (1) The language
is that of
$\mathbf {LJ}$
with the additional basic symbols
and
governed by the following clauses:
If
$ \mathfrak {F}[a] $
is an
-wff, then
is an
-term.
If
$ s $
and t are
-terms, then
is an
-wff.
If a and b are free variables, then
is said to be a prime.
(2)
-rules:
(3) The system
is defined as the extension of Gentzen’s
$\mathbf {LJ}$
without cut based on the language
with the foregoing
-rules.
Theorem 2.2 (Non-triviality of
)
Not every wff is
-deducible.
Proof. Obviously, the empty sequent is not
-deducible for the usual reason: in the absence of cut the empty sequent cannot be the lower sequent of any inference figure.Footnote
3
Similarly, a prime sequent such as
, for instance, cannot be
-deducible because none of the operational rules of
can have a prime sequent as a lower sequent, and the only structural inference in
, the lower sequent of which could possibly have an empty antecedent and a prime succedent, is a weakening-right the upper sequent of which is the empty sequent.
Remarks 2.3. (1) In other words, just as the non-deducibility of the empty sequent in
is a trivial consequence of the lack of cut, so is the non-triviality of
. This is due to the specific character of the sequential rules as fixed by Gentzen in his doctoral dissertation in 1934 (published as [Reference Gentzen2]): none of the inference rules eliminates a wff for good, except cut.
(2) In view of the absence of any form of extensionality,
cannot count as a (naive) set theory, only a (naive) property theory, or higher order logic.
In order to provide a link to Priest’s logic of paradox, a translation of intuitionistic sequents (maximally one wff in the succedent) into wffs is introduced next.
Definition 2.4. (1) The translation
$ {\tau (A_1, \dots , A_m \Rightarrow B)} $
of a sequent is defined as the wff
$$\begin{align*}\neg (A_1 \land \dots \land A_m) \lor B \end{align*}$$
if
$ m> 0 $
and the succedent is not empty, just
$ B $
if the antecedent is empty and
$$\begin{align*}\neg (A_1 \land \dots \land A_m) \end{align*}$$
if the succedent is empty. The case that both are empty will not play any role in what follows, so any false wff will do, for instance the unprovable wff
which would yield any wff if inversions were available.
(2) The translation
$ \tau \left (\frac {S_1}{S_2} \right ) $
of a sequential inference with one upper sequent is defined as
$ \frac {\tau (S_1)}{\tau (S_2)} $
and for inferences with two upper sequents
$ \tau \left (\frac {S_1 \ S_2}{S_3} \right ) $
as
$ \frac {\tau (S_1) \ \tau (S_2) }{\tau (S_3)} $
.
Remark 2.5. In view of the equivalence of
$ \neg A \lor B $
and
$ A \to B $
in Priest’s logic of paradox it should be clear that one might just as well take
$$\begin{align*}\neg (A_1 \land \dots \land A_m) \to B \end{align*}$$
for the translation of a sequent with
$ m> 0 $
and a non-empty succedent.
Definition 2.6. The value
of a wff in
is defined as that of
in [Reference Priest7] with the additional clause
Theorem 2.7 (Soundness)
If
, then
, for every sequent S built from
-wffs.
Proof. Employ an induction on the length of the
-deduction of S. This amounts to confirming that every sequential inference rule with the exception of cut is non-falsity preserving with regard to Priest’s truth tables.Footnote
4
For the case of
$\mathbf {L\hspace {-.2ex}^iP}$
, i.e.,
$\mathbf {LJ}$
without cut, this is actually a straightforward consequence of the fact that every two-valued tautology is also valid in Priest’s three-valued semantics and vice versa (theorem III.13 in [Reference Priest7, p. 230]). The only additional case in
is that of
-inferences. In that case Definition 2.6 guarantees that the
$\tau $
-translation of the lower sequent of an inference according to 2.1(2) has the same truth-value as that of the upper sequent.
Remark 2.8. The fact that all classical tautologies are valid in Priest’s three-valued logic of paradox leads to the intuitively awkward situation that the wff
$ {A \land (A \to B) \to B} $
, for instance, is valid while modus ponens, i.e.,
$ {A, A \to B \vdash B} $
, is not admissible. This situation is repeated in
in the form that the sequent
$ A, A \to B \Rightarrow B $
is
-deducible while the inference from
$ \: \Rightarrow A$
and
$ \: \Rightarrow A \to B $
to
$ \: \Rightarrow B $
is not valid.
Proposition 2.7 can be seen as the justification for my use of the label
for Priest’s logic of paradox augmented with unrestricted abstraction.
Historical Note 2.9. The connection between three-valued logic and cut-free derivations can be traced back to [Reference Schütte15] which provided the crucial ingredient for the later proof of Takeuti’s conjecture.Footnote 5
The
-deductions that are to follow are fairly complete, except for exchanges and contractions. The danger consists in letting classical principles sneak in and that’s why I have tried to make deductions very explicit.
Conventions 2.10. (1) For simplicity’s sake, I shall occasionally use the following rule for
$ \land $
-left as it is
-derivable with the help of contraction and exchange:
(2) I write “
$ \,{\Leftrightarrow A}$
” to mean “
$ \,{\Rightarrow A}\, $
as well as
$ \,{A \Rightarrow }\, $
”, i.e., if
$ \,{\Leftrightarrow A }\, $
is provable then A is a dialetheia.
(3) Additional theoretical constants are defined as in [Reference Petersen6, definition 2.9] with the following exception:
$ \emptyset $
is defined as
because
is actually not completely empty (3f), and the universal set
$ \mathcal {V} $
is defined as
. I also use
which may not satisfy the expectations on an empty set properly so called, but it still proves helpful in formulating a result such as Corollary 8.39.
(4) Different symbols for free and bound (object) variables are used as listed in [Reference Petersen5, p. 91, able 12.13]. In view of the intended meaning of
$ f $
as a function term I use
$ f $
as a symbol for a free occurrence and
$\,\mathfrak {f}\,$
for its bound counterpart.
Proposition 2.11. The following is
-deducible for all terms s.
$$ \begin{align} & \quad \Rightarrow s = s ; \end{align} $$
$$ \begin{align} & \quad \Rightarrow \exists x \exists y (x \neq y) . \end{align} $$
Proposition 2.12. Inferences according to the following schema are
-derivable.
Remark 2.13. Of course, cut would yield the empty sequent in 2.12. But without cut, it “only” means that s equals every term—as well as not.
3 On the working of
The relevant wff
$\dagger $
in Weber’s proof of Cantor’s theorem may be rendered as “every subset of a set M has an element which is not the value (in the co-domain) of a function”. Obviously, there is no constraint on the function. In fact, this can be sharpened to “every subset of a set M has an element which doesn’t equal any term”, which is 5b, and which can be seen to be a dialetheia straightaway.
Let
$ {\bot \mspace {-14.0mu} \top } $
be a dialetheia (such as
), i.e.,
The following proposition lists a few
-deducible dialetheias based on
$ {\bot \mspace {-14.0mu} \top } $
.
Proposition 3.14. The following is
-deducible for all terms s.
$$ \begin{align} & \quad \Leftrightarrow s \equiv s . \end{align} $$
Proof. Re 3a.
Re 3b. This is a straightforward consequence of 3a by 2.12.
Re 3c–3e. Straightforward consequences of 3a, possibly with s being a free variable.
Re 3f. “
$\Leftarrow $
”.
Re 3g. “
$\Rightarrow $
” is trivial.
“
$\Leftarrow $
”.
Proposition 3.15. The following is
-deducible for arbitrary terms r, s and t.
4 Bringing in the power set
So far I have just collected a number of results concerning specific dialetheias. This was intended as a preparation for my approach to Cantor’s theorem which somewhat follows [Reference Weber18] in the sense of being based on dialetheias. I shall now begin to connect these results to the notion of power set.
Proposition 4.16. The following is
-deducible for arbitrary terms s and t.
Proof. Re 5a.
Re 5b. “
$ \Rightarrow $
”.
“
$ \Leftarrow $
”.
$ \mathfrak {P} $
is of no relevance.
Re 5c. “
$ \Rightarrow $
”.
“
$ \Leftarrow $
”.
Re 5d. “
$\Rightarrow $
”. This follows immediately from 5a and 4a by a
$\land $
-r inference.
“
$\Leftarrow $
”.
Theorem 4.17.
Proof. “
$ \Rightarrow $
”. Continue from 5d “
$\Rightarrow $
” as follows:
“
$ \Leftarrow $
”. This is a straightforward consequence of 5c “
$ \Leftarrow $
” by
$\forall $
-left inferences.
Remark 4.18. The foregoing theorem already establishes a sequent with the essential features of
$\dagger $
and that for just any term, i.e., without specifically involving a function. This will serve as a general template for variations.
5 Adding a place for functions
Cantor’s theorem is about the non existence of a bijective function but the results so far do not mention functions at all. This is going to change now without, however, adding new content. I shall just provide a definition for the image of a function here, as a placeholder, as it were, while its properties will only be needed in the next section.
Definition 5.19.
With this notion at hand, results can be given a more familiar appearance, i.e., one that comes closer to
$\dagger $
.
Corollary 5.20. The following is
-deducible:
Remark 5.21. 6a is the form that is employed in the proof of Theorem 5.6 in [Reference Weber18, p. 282]. 6b is a dialetheia as will be stated in 10a.
In Section 1, I mentioned that Cantor’s theorem is violated for the universal set with the identity function. While the identity function is certainly suitable to prove this for the universal set, I prefer to introduce a function which will do more than just that, i.e., which will extend to other than just the universal set.
I begin by introducing definition for the relevant properties of functions.
Definition 5.22. (1)
(2)
(3)
(4)
(5)
Remark 5.23. Of course it might look more common to take the identity function. But anything as unorthodox as employing a dialetheia to (dis)prove Cantor’s theorem deserves an unorthodox treatment.
Definition 5.24.
Proposition 5.25. The following is
-deducible.
$$ \begin{align} & \Rightarrow \hat{\eta}(s) = t ; \end{align} $$
Proof.
7a, “
$\Rightarrow $
”.
7a, “
$\Leftarrow $
”.
7b. This is an immediate consequence of 7a by 2.12.
7c.
7d.
7e.
Proposition 5.26. The following is
-deducible.
Proof. Re 8a.
Re 8b. As for 8a, just with
$\mathcal {V}$
instead of
${\bot \mspace {-14.0mu} \top }$
.
Re 8c. Immediate consequence of 8b by a
$\land $
-l inference with a subsequent
$\exists $
-l inference.
I list a few simple consequences.
Proposition 5.27. The following is
-deducible.
Combining 5.20 and 5.27 we obtain the following dialetheias.
Corollary 5.28. The following is
-deducible.
6 Putting
$\mathsf {bij}$
into the picture
While
$ \dagger $
is
-provable for all sets M and (function) terms f, it seems that a negation of
$ \dagger $
can only be established for specific terms as in 9b which involves on the function
$ \hat {\eta } $
, i.e., a function that, thanks to
$ {\bot \mspace {-14.0mu} \top }$
, takes any argument and returns an arbitrary value. Since this is a bijective function by 7f, I can now start bringing in the condition of a bijective function in order to get closer to a formulation of Cantor’s theorem and its opposite.
Proposition 6.29.
Proof. “
$\Rightarrow $
”. Take, again, 5d, “
$\Rightarrow $
”, with the free variable a taking the place of s and
$ f (z)$
that of t.
“
$\Leftarrow $
”.
7 Proving Cantor’s theorem
Cantor’s theorem is formulated in terms of cardinality. I am now going to introduce the relevant definition regarding a formal notion of cardinality.
Definition 7.30. (1)
(2)
(3)
$ | s | < | t | :\equiv | s | \leq | t | \land | s | \neq | t | . $
Remark 7.31. It should be clear that
is an alternative but equivalent definition of
$ | s | = | t |$
.
As a straightforward consequence of corollary 6a we have the following.
Proposition 7.32.
$ \Rightarrow | \mathfrak {P} M | \neq | M | $
is
-deducible for all M.
Proof.
□
Corollary 7.33.
$ \Leftrightarrow \forall x (| \mathfrak {P} x | \neq | x |) $
is
-deducible.
Proof. This is 6.29 formulated in terms of equal cardinality.
Definition 7.34.
Proposition 7.35. The following is
-deducible.
$$ \begin{align} & id^{\scriptscriptstyle\circ}(a) = id^{\scriptscriptstyle\circ}(b) \Rightarrow a = b . \end{align} $$
Proposition 7.36. The following is
-deducible for all M.
$$ \begin{align} & \Rightarrow | M | \leq | \mathfrak{P} M | ; \end{align} $$
$$ \begin{align} & \Rightarrow | M | < | \mathfrak{P} M | . \end{align} $$
8 Refuting Cantor’s theorem
It is apparently not possible to show
$ \,{| \mathfrak {P} M | = | M |}\, $
for arbitrary M, only for non-empty ones. I begin with the universal set as it is the example that led Russell to the paradox that bears his name.
Proposition 8.37. The following is
-deducible (Cf. [Reference Weber18, p. 282, corollaries 5.4 and 5.5]).
$$ \begin{align} & \Leftrightarrow | \mathfrak{P} \mathcal{V} | = | \mathcal{V} | ; \end{align} $$
$$ \begin{align} & \Leftrightarrow | \mathcal{V} | = | \mathcal{V} | . \end{align} $$
Proof.
14a, “
$\Rightarrow $
”. As for the first part of 6.29 “
$\Leftarrow $
”, only with 9b instead of 8c.
“
$\Leftarrow $
”. This is a straightforward consequence of 6a.
14b, “
$\Rightarrow $
”. Trivial.
“
$\Leftarrow $
”. This is a straightforward consequence of 1c and 4a.
Proposition 8.38. The following is
-deducible for arbitrary M, where
$\emptyset ^{(\ast )}$
can be
$ \emptyset $
or
$\emptyset ^\ast $
.
$$ \begin{align} & M \neq \emptyset^{(\ast)} \Rightarrow | \mathfrak{P} M | = | M | ; \end{align} $$
$$ \begin{align} & \Rightarrow | \mathfrak{P} \emptyset^\ast | = | \emptyset^\ast | ; \end{align} $$
$$ \begin{align} & M = \emptyset^\ast \Rightarrow | \mathfrak{P} M | = | M | . \end{align} $$
Just for the record, I add the following corollary:
Corollary 8.39. The following is
-deducible for arbitrary M.
$$ \begin{align} & \Leftrightarrow M = \emptyset^\ast \lor M \neq \emptyset^\ast \to | \mathfrak{P} M | = | M | ; \end{align} $$
$$ \begin{align} & \Leftrightarrow M = \emptyset^\ast \lor M \neq \emptyset^\ast \land | \mathfrak{P} M | \neq | M | . \end{align} $$
9 Taking stock
Getting back now to the question formulated in the title of this paper: is Cantor’s theorem a dialetheia?
First of all there is the special case of the universal set, which I mentioned in the introduction as providing a starting point for Russell’s paradox. If anything, this would qualify as a classic candidate for a dialetheia. In fact, by 14a,
$$ \begin{align*} & \Leftrightarrow | \mathfrak{P} \mathcal{V} | = | \mathcal{V} | & \end{align*} $$
is
-deducible. This will be hardly surprising as it is simply based on
which is 10b (Cf. [Reference Weber18, p. 282]).
While this may well be an acceptable dialetheia, the situation strikes me as quite different when it comes to arbitrary non-empty sets M.
In view of 15a the following can be seen to be a
-derivable inference:
by a slight variation of the proof of 15a:
In other words, if M is
-provably non-empty, i.e.,
can be established for some term s, then
Now these are full blown dialetheias. In my view, this takes the thrill out of Weber’s result. In terms of Weber’s question ([Reference Weber18, p. 269]): “is Cantor’s theorem true in the paraconsistent system?” The answer would have to be yes, but not only; it is also false, at least for non-empty sets.
It might be tempting for a paraconsistent theoretician to consider only one side of a dialetheia, especially in a case such as Cantor’s theorem, or not to consider the possibility of a dialetheia at all. Either way this strikes me as cherry picking and so my aim in this paper was to add some pieces of bitter fruit to round off the taste.
