Hostname: page-component-78c5997874-j824f Total loading time: 0 Render date: 2024-11-05T21:42:24.978Z Has data issue: false hasContentIssue false

IS CANTOR’S THEOREM A DIALETHEIA? VARIATIONS ON A PARACONSISTENT APPROACH TO CANTOR’S THEOREM

Published online by Cambridge University Press:  29 June 2023

UWE PETERSEN*
Affiliation:
ALTONAER STIFTUNG FÜR PHILOSOPHISCHE GRUNDLAGENFORSCHUNG (ASFPG) EHRENBERGSTR. 27, 22767 HAMBURG, GERMANY
Rights & Permissions [Opens in a new window]

Abstract

The present note was prompted by Weber’s approach to proving Cantor’s theorem, i.e., the claim that the cardinality of the power set of a set is always greater than that of the set itself. While I do not contest that his proof succeeds, my point is that he neglects the possibility that by similar methods it can be shown also that no non-empty set satisfies Cantor’s theorem. In this paper unrestricted abstraction based on a cut free Gentzen type sequential calculus will be employed to prove both results. In view of the connection between Priest’s three-valued logic of paradox and cut free Gentzen calculi this, a fortiori, has an impact on any paraconsistent set theory built on Priest’s logic of paradox.

Type
Research Article
Copyright
© The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

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.

(1a) $$ \begin{align} & \quad \Rightarrow s = s ; \end{align} $$
(1b)
(1c)
(1d) $$ \begin{align} & \quad \Rightarrow \exists x \exists y (x \neq y) . \end{align} $$

Proof. Straightforward consequences of the definition. I only treat the last one.

Re 1d.

Proposition 2.12. Inferences according to the following schema are -derivable.

Proof. 2.12, “ $\Rightarrow $ ”.

$\Leftarrow $ ”.

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.

(3a)
(3b)
(3c)
(3d)
(3e)
(3f)
(3g) $$ \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 3c3e. 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.

(4a)
(4b)

Proof. 4a.

4b.

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.

(5a)
(5b)
(5c)
(5d)

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:

(6a)
(6b)

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.

(7a)
(7b) $$ \begin{align} & \Rightarrow \hat{\eta}(s) = t ; \end{align} $$
(7c)
(7d)
(7e)
(7f)

Proof. 7a, “ $\Rightarrow $ ”.

7a, “ $\Leftarrow $ ”.

7b. This is an immediate consequence of 7a by 2.12.

7c.

7d.

7e.

7f. This is an immediate consequence of 7b–iv.

Proposition 5.26. The following is -deducible.

(8a)
(8b)
(8c)

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.

(9a)
(9b)

Proof. Re 9a. Immediate consequence of 8c by a $\forall $ -l inference.

Re 9b. As for 9a, only with $ \mathcal {V} $ instead of .

Combining 5.20 and 5.27 we obtain the following dialetheias.

Corollary 5.28. The following is -deducible.

(10a)
(10b)

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.

(12a)
(12b) $$ \begin{align} & id^{\scriptscriptstyle\circ}(a) = id^{\scriptscriptstyle\circ}(b) \Rightarrow a = b . \end{align} $$

Proof. 12a.

Note that this is without any form of extensionality.

12b.

Proposition 7.36. The following is -deducible for all M.

(13a) $$ \begin{align} & \Rightarrow | M | \leq | \mathfrak{P} M | ; \end{align} $$
(13b) $$ \begin{align} & \Rightarrow | M | < | \mathfrak{P} M | . \end{align} $$

Proof. 13a.

Quantification does the rest.

13b. This an immediate consequence of 13a and 7.32 by a $\land $ -r inference.

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

(14a) $$ \begin{align} & \Leftrightarrow | \mathfrak{P} \mathcal{V} | = | \mathcal{V} | ; \end{align} $$
(14b) $$ \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 $ .

(15a) $$ \begin{align} & M \neq \emptyset^{(\ast)} \Rightarrow | \mathfrak{P} M | = | M | ; \end{align} $$
(15b) $$ \begin{align} & \Rightarrow | \mathfrak{P} \emptyset^\ast | = | \emptyset^\ast | ; \end{align} $$
(15c) $$ \begin{align} & M = \emptyset^\ast \Rightarrow | \mathfrak{P} M | = | M | . \end{align} $$

Proof. 15a.

15b. In view of the similarity to following proof this is left to the reader.

15c.

Just for the record, I add the following corollary:

Corollary 8.39. The following is -deducible for arbitrary M.

(16a) $$ \begin{align} & \Leftrightarrow M = \emptyset^\ast \lor M \neq \emptyset^\ast \to | \mathfrak{P} M | = | M | ; \end{align} $$
(16b) $$ \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.

Footnotes

1 Cf. [Reference Priest9, p. 78]. Since this observation is attributed to me I wish to emphasize that in [Reference Priest, Başkent and Ferguson10, p. 597, fn. 87], in the context of discussing [Reference Dicher, Paoli, Başkent and Ferguson1], Priest reiterates this point and also remarks that the “result was proved” in [Reference Pynko11].

2 There is, above all, Russell’s remark in [Reference Russell12, p. 101] that he “was led to [the paradox] in the endeavour to reconcile Cantor’s proof that there can be no greatest cardinal number with the very plausible supposition that the class of all terms … has necessarily the greatest possible number of members.” Similarly in his autobiography [Reference Russell14, p. 221] and in [Reference Russell13, p. 136].

3 Cf. [Reference Szabo16, p. 103] translating [Reference Gentzen2, p. 405]: “the [empty] sequent … cannot be the lower sequent of any inference figure and is therefore not derivable.” This then is the reason why cut elimination has become the basic strategy for proving consistency in Gentzen type proof theory.

4 It is the cut rule that makes the difference: there is the possibility of and , but .

5 For more regarding Takeuti’s conjecture and three-valued logic, see [Reference Girard3, chap. 3]. In [Reference Girard3, p. 161], Jean-Yves Girard speaks of “Schütte-valuations” in this context.

References

BIBLIOGRAPHY

Dicher, B., & Paoli, F. (2019). ST, LP and tolerant metainferences. In Başkent, C., and Ferguson, T. M., editors. Graham Priest on Dialetheism and Paraconsistency. Outstanding Contributions to Logic, Vol. 18. Cham: Springer, pp. 383407.CrossRefGoogle Scholar
Gentzen, G. (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 176210, 405–431. Doctoral thesis accepted 1934; translation in Gentzen (1964), 288–306, and Gentzen (1965), 204–218, as well as Szabo (1969), 68–131.CrossRefGoogle Scholar
Girard, J.-Y. (1987). Proof Theory and Logical Complexity. Studies in Proof Theory, Vol. I. Napoli: Bibliopolis.Google Scholar
Petersen, U. (1981). What is dialectic: Logic versus epistemology. In Becker, W., and Essler, W. K., editors. Konzepte der Dialektik. Frankfurt am Main: Vittorio Klostermann, pp. 187190.Google Scholar
Petersen, U. (2002). Diagonal Method and Dialectical Logic. Tools, Materials, and Groundworks for a Logical Foundation of Dialectic and Speculative Philosophy. Osnabrück: Der Andere Verlag.Google Scholar
Petersen, U. (2022). Is cut-free logic fit for unrestricted abstraction? Annals of Pure and Applied Logic, 173(6), 103101.CrossRefGoogle Scholar
Priest, G. (1979). The logic of paradox. Journal of Philosophical Logic, 8(1), 219241.CrossRefGoogle Scholar
Priest, G. (1987). In Contradiction. A Study of the Transconsistent. Dordrecht: Martinus Nijhoff.CrossRefGoogle Scholar
Priest, G. (1987/2006). In Contradiction. A Study of the Transconsistent. Oxford: Clarendon Press. Expanded second edition of Priest (1987).CrossRefGoogle Scholar
Priest, G. (2019). Some comments and replies. In Başkent, C., and Ferguson, T. M., editors. Graham Priest on Dialetheism and Paraconsistency. Outstanding Contributions to Logic, Vol. 18. Cham: Springer, pp. 575675.CrossRefGoogle Scholar
Pynko, A. P. (2010). Gentzen’s cut-free calculus versus the logic of paradox. Bulletin of the Section of Logic, 39(1/2), 3542.Google Scholar
Russell, B. (1903). The Principles of Mathematics (Third reprint of 1937 (second) ed.). Cambridge: Cambridge University Press. London 1950: Allen & Unwin. Orig.Google Scholar
Russell, B. (1919). Introduction to Mathematical Philosophy (Dover ed.). London: George Allen & Unwin Ltd. Google Scholar
Russell, B. (1967). The Autobiography of Bertrand Russell, Vol. I, 18721914. London: George Allen & Unwin Ltd. Google Scholar
Schütte, K. (1960). Syntactical and semantical properties of simple type theory. The Journal of Symbolic Logic, 25, 305326.CrossRefGoogle Scholar
Szabo, M. E., editor (1969). The Collected Papers of Gerhard Gentzen. Amsterdam and London: North-Holland Publishing Company.Google Scholar
Takeuti, G. (1987). Proof Theory (second edition). Studies in Logic and the Foundations of Mathematics, Vol. 81. Amsterdam: North-Holland Publishing Company.Google Scholar
Weber, Z. (2012). Transfinite cardinals in paraconsistent set theory. The Review of Symbolic Logic, 5(2), 269293.CrossRefGoogle Scholar