# Are Separation and Types the only way to avoid paradoxes?

When Russell discovered his paradox, two ways were invented to avoid Russell's paradox.

For logic with sets, ZFC was developed which restricts the creation of the definition of sets. Only sets that are subset of an existing set can be defined with the axiom of separation. And in some case you first need to to use the axiom of power set.

In type theory a different approach was taken. By giving the functions types, it is not possible to express something as element of itself.

My question is, did the logicians in the 20th century consider other ways to avoid paradoxes (only serious attempts)?

I am not completely satisfied with this way of paradox avoiding. Not because it doesn't work (I think it does work), but it forces me to accept the whole system. It is not an universal trick to avoid paradoxes, but inseparable linked to the system.

So, are there ways to avoid paradoxes that for instance also apply to the Liar's paradox?

I think that in general the following scheme is followed to obtain a contradiction from a paradox (whether it is Russell's paradox or the liar paradox, I don't think it is much different):

3) Express this in one statement, by discharging the assumption.
4) Reformulate previous result such that becomes exactly the paradox.

So, to avoid paradoxes, one or more of the above steps can not be fully unlimited.

Note, that applying a rule on itself in general should not be forbidden, because this happens often in a harmless way (for instance when you instantiate an universal quantifier over a predicate variable, which may result again in something with a similar quantifier).

I am experimenting if you can do the trick with levels. Suppose we have a sentence $C$ with definition: $$C := A \rightarrow B$$

Here $C$ is not just a propositional parameter, but a type of sentence that can produce one, more or infinite other logical sentences, if a logical sentence is given as input. In case of the Liar's paradox it takes itself as input and will produce $\bot$.

To avoid the paradox, each sentence is given a level and in the case above $A$ and $B$ must be of a lower level than $C$. Since, $A$ and $C$ can not be the same anymore, due to the level restriction, the contradiction can not be concluded anymore.

The level is taken from $\mathbb Z$, rather than $\mathbb N$. This prevents that you run out of levels.

If you have a theorem on a certain level, and the theorem is not under assumption, you may replace the level by the "any" level, since you can do a similar reasoning with any other level. The idea is that most statements gets the "any" level and you don't have to bother about it.

You are not allowed to do this under assumption. So, reasoning under assumption is limited in two ways:

1) You are not allowed to assume the "any" level.
2) You are not allowed to generalize to the "any" level under assumption.

Has anything attempted like this before and is this doomed to fail?

• I honestly can't figure out what your system is - can you describe it more precisely? What exactly are its axioms/rules of inference? (Also, if I understand correctly you are stratifying sentences as opposed to sets, which I think is overly complicated - you might be interested in New Foundations, which is essentially "type theory without types": sets don't have inherent types, but Comprehension only holds for "typable" formulas.) Jan 2, 2017 at 21:09
• Thanks for the comment. I had no knowledge about NF. The levels look like stratifying indeed. In my system (still in development), an expression consists of $\bot$, <expr> $\rightarrow$ <expr>, a triple (<computable function>, <level>, <input string>) or some arithmetic. If a theorem consists of the triple alone, the function can be executed with the input string and a number, to generate new theorems. Possibly, this can be an infinite number. With this the $\land$ and $\forall$ operators can be programmed, where the input string is the sub-expression. Jan 2, 2017 at 22:32
• Properties of $\land$ and $\forall$ need to be given initially, but when the system is strong enough, those properties can be proven by itself. So, the system is pure syntactically. I never got the system right, because of the paradoxes. You can easily express the Liar's paradox in this system. It is just function that generates itself implicating $\bot$. But with the levels it might work. Jan 2, 2017 at 22:37
• Alright, now I understand the syntax (mostly - what is an "input string": is it a finite binary string, or an expression in the system, or . . . ) of your system - how do proofs work? What are the axioms and rules of inference? Jan 2, 2017 at 23:14
• Anent the title question: Quine's New Foundations.
– bof
Jan 2, 2017 at 23:50

In point of fact, there are (at least) a couple more ways to circumvent the paradoxes brought about by the use of the unrestricted comprehension axiom

$$\existsy\forallx$$($$x\iny\leftrightarrow\varphi$$($$x$$)).

I will discuss (in not too much detail) two of them, then provide references for you to follow up on.

The first comes from Thoralf Skolem's paper, "Investigations On A Comprehension Axiom Without Negation In The Defining Propositional Functions" (Notre Dame Journal of Formal Logic, Vol 1, (1960), pp. 13-22). In that paper he proved that ideal set theory

(i) $$\forallx\forally\forallz$$(($$z\inx\leftrightarrowz\iny$$)$$\rightarrowx$$=$$y$$); (ii)$$\existsy\forallx$$($$x\iny\leftrightarrow\varphi$$($$x$$))

is consistent "provided that only conjunction and disjunction are allowed in $$\varphi$$" (pg. 13). This notion is made precise by the inductively defined notion of "positive propositions":

1. The truth constants $$0$$ [$$\bot$$] and $$1$$ [$$\top$$] are positive propositions

2. Every atomic proposition $$x\iny$$ is a positive proposition. Here $$x$$ and $$y$$ are free variables.

3. If $$A$$ and $$B$$ are positive propositions, so are $$A\land$$ $$B$$ and $$A\lorB$$. The latter have the free and bound variables occurring in $$A$$ and $$B$$.

4. If $$A$$($$x$$, $$x_1$$,...,$$x_n$$) is a positive proposition with $$x$$,$$x_1$$,...,$$x_n$$ as free variables $$\forallxA$$($$x$$,$$x_1$$,...,$$x_n$$) and $$\existsxA$$($$x$$,$$x_1$$,...,$$x_n$$) are positive propositions with $$x$$ as bound variable, $$x_1$$,...,$$x_n$$ as free variables, while the eventually occurring bound variables in $$A$$($$x$$, $$x_1$$,...,$$x_n$$) remain bound in the latter expressions.

If a set $$y$$ is such that $$\forallx$$(($$x\iny$$)=$$U$$($$x$$,$$x_1$$,...,$$x_n$$)) is true, where $$x$$,$$x_1$$,...,$$x_n$$ are the set variables in the positive proposition $$U$$, then $$y$$ is a set function of $$x_ 1$$,...,$$x_n$$.

This notion is further developed in the following papers by Olivier Esser:

"An Interpretation of the Zermelo-Fraenkel Set Theory and the Kelly-Morse Set Theory in a Positive theory", Mathematical Logic Quarterly, Vol. 43 (1997), pp. 369-377.

"On the Consistency of a Positive Theory", Mathematical Logic Quarterly, Vol. 45 (1999), No. 1, pp.105-116.

Skolem also studied the following naive comprehension axiom

$$\forallx_1$$...$$\forallx_n\existsy\forallx$$($$x\iny\leftrightarrow\varphi$$($$x$$, $$x_1$$,...,$$x_n$$)), where $$\varphi$$ is either a propositional constant or built from atomic expressions $$u\inv$$ by negation, conjumction and disjunction and there are no other variables in $$\varphi$$ than $$x$$,$$x_1$$,...,$$x_n$$ [this from his paper, "Studies on the Axiom of Comprehension", Notre Dame Journal of Formal Logic, Vol. 4, No. 3 (1963), pp.162-170--my comment].

in a 3-valued logic. In his paper,

"A Set Theory Based on a a Certain 3-valued Logic", ( Math. Scand., Vol. 8 (1960), pp. 127-136),

he constructs a domain (model) in which both the quantifier-free comprehension axiom

$$x\iny\leftrightarrow\Phi$$($$x$$) (where $$\Phi$$($$x$$) is a propositional function in which the variable $$x$$, but not $$y$$, occurs)

and the Axiom of Extensionality holds. However, he is unable to extend this result to a quantified version of his logic (in fact, he shows that attempting to extend his result to include relative quantification, defined by Skolem in his paper as this:

The relative one [quantification--my comment] means that we take the minimum or maximum of all values of a propositional function $$A$$($$x$$) just for those $$x$$ for which a function $$B$$($$x$$) has the value 1

results in inconsistency). In fact, in this paper, he notes that

The reader will notice that I have not even proved the consistency of the theory with only absolute quantification [presumably, for Skolem, "absolute quantification" means that we take the minimum or maximum of all values of a propositional function $$A$$($$x$$) without regard to any function $$B$$($$x$$) the $$x$$ might satisfy--my comment]. It might be inconsistent as well, but that appears to me improbable.

If I have not misunderstood Skolem's notion of "absolute quantification", Ross T. Brady, in his paper,

"The Consistency of the Axioms of Abstraction and Extensionality in a Three-Valued Logic", (Notre Dame Jounal of Formal Logic, Vol. 7, No.4 (1971), pp. 440-453),

proved the consistency of Skolem's 3-valued set theory, at least for absolute quantification (and possibly for relative quantification as well, provided the Lukasiewicz connective '$$\rightarrow$$' is not a primitive connective, but can be expressed in terms of '$$\lnot$$' and '&'). That Skolem and Brady are referring to the same 3-valued set theory can be shown by noting that the truth-tables for $$\lnot$$, &, and $$\lor$$ are identical for both Skolem and Brady, and Skolem's formula for deriving the truth-table for $$\rightarrow$$ gets the same values for $$\rightarrow$$'s truth-table as Brady's.

• @LucasK.: Happy to help. Feb 8, 2017 at 20:48

One way of avoiding such paradoxes is weakening the base logic that we use it for reasoning in our formal theory. One of these logics is Visser-Ruitenburg Basic logic. This logic is a sub-intuitionistic logic which satisfies this equation $\bf \frac{IPC}{S_4}=\frac{BPC}{K_4}$ with respect to translation of Godel (intuitionistic logic to modal logic). By removing modus ponens from $\bf IPC$ and adding some rules and axioms like cut, transitivity and etc to logic, $\bf BPC$ is defined. So it is not true that ${\bf BPC}\vdash \top \to \phi \Rightarrow \phi$ for every formula $\phi$.

Maybe this answers to your first question that Fregean Set theory or ${\bf FST}$ is consistent and has Kripke models with respect to this logic. I'm not sure, but I think that $\bf BPC$ is maximal logic that $\bf FST$ is consistent with respect to it.

References

1. W.Ruitenburg, M.Ardeshir, Basic propositional calculus I, Mathematical Logic Quarterly 44 (1998), pp. 317--343.
2. W.Ruitenburg, Basic predicate calculus, Notre Dame Journal of Formal Logic 39, No. 1 (1998), pp. 18--46.
3. W.Ruitenburg, Basic logic and Fregean set theory, in H. Barendregt, M. Bezem, J.W. Klop (editors), Dirk van Dalen Festschrift, Quaestiones Infinitae, Vol. 5, Department of Philosophy, Utrecht University, March 1993, pp. 121--142.
4. W.Ruitenburg, Constructive logic and the paradoxes, Modern Logic 1, No. 4 (1991), pp. 271--301.
• @LucasK. You're welcome :-) Jan 4, 2017 at 5:14