basic constructions:
strong axioms
further
In mathematical logic/mathematical foundations, the axiom or rule of full or unrestricted comprehension says that for any property $P$, there exists a set of all objects satisfying $P$:
Set theory with the unrestricted comprehension rule is called naive set theory?, and is inconsistent due to Russell's paradox and Curry's paradox. Here we mention several approaches to this issue.
Standard set theories such as ZFC avoid this paradox by replacing unrestricted comprehension with the axiom scheme of separation (or “restricted comprehension”), which restricts $x$ to lie in some previously specified set $X$.
Set theories such as New Foundations instead replace comprehension by a rule of “stratified comprehension”. This permits a “set of all sets” but still appears to avoid paradox.
It is also possible to retain full comprehension but avoid paradox by modifying the ambient logic. Passing to constructive logic doesn’t help, and indeed the root issue has nothing to do with negation as such, since Curry's paradox can be stated without any negation. One might think that paraconsistent logic would help, but many paraconsistent logics are still vulnerable to Curry’s paradox. Perhaps the most obvious culprit is the contraction rule, and indeed linear logic (including some paraconsistent logics) can admit a full comprehension rule without explosion.
Another possibility is to keep the contraction rule but restrict the use of the cut rule. It is not necessary to forbid all uses of cut, since many cuts can be normalized or eliminated. Indeed, in ordinary consistent logic, all cuts can be eliminated; but in the presence of full comprehension they cannot all be. Thus, another way to avoid paradox with full comprehension is to permit only proofs that can be normalized.
Note that unlike a restriction on contraction, this is a “global” restriction: the proofs of two lemmas can independently be valid, but their combination may no longer be so. Similar “global” restrictions on logic were investigated by Fitch 1953, 69.
In linear logic:
Grishin, V. N., “Predicate and set theoretic calculi based on logic without contraction rules” (Russian), Izvestiya Akademii Nauk SSSR Seriya Matematicheskaya, 45(1): 47 – 68, 1981. English translation in Math. USSR Izv., 18(1): 41 – 59, 1982. (math-net.ru)
Jean-Yves Girard, Light Linear Logic, Information and Computation, 14(3):123-137, 2003. (pdf.gz)
Kazushige Terui, Light Affine Set Theory: A Naive Set Theory of Polynomial Time, Studia Logica: An International Journal for Symbolic Logic, Vol. 77, No. 1 (Jun., 2004), pp. 9-40. (jstor) (pdf). See also Terui’s slides, Linear Logic and Naive Set Theory (Make our garden grow)
Several global restrictions were considered in
Frederic Fitch, Symbolic Logic: An introduction, Ronald Press, New York 1952
Frederic Fitch, A method for avoiding the Curry paradox, in Essays in Honor of Carl G. Hempel, Reidel, Dordrecht, Holland 1969, pp. 255–265 (doi:10.1007/978-94-017-1466-2)
The notation therein is somewhat difficult to follow for a modern reader, especially due to the somewhat confused treatment of what nowadays would be called free and bound variables. A more modern explanation of Fitch’s restrictions can be found in:
The normalizability restriction is also discussed philosophically in
and other references (someone add!).
Last revised on September 18, 2021 at 01:54:03. See the history of this page for a list of all contributions to it.