nLab axiom of full comprehension

Full (unrestricted) comprehension

Full (unrestricted) comprehension

Idea

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$:

$\{ x \mid P(x) \}.$

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.

Restricted comprehension

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

Stratified comprehension

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.

Substructural logics

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.

Normal logics

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.

References

In linear logic

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)

Global restrictions

Several global restrictions were considered in

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:

• Susan Rogerson, Natural deduction and Curry’s paradox, Journal of Philosophical Logic (2007) 36: 155–179. pdf

The normalizability restriction is also discussed philosophically in

• Tennant, N.: Proof and paradox, Dialectica 36 (1982), 265-296

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.