User:Edisonabcd/Sandbox

This is the user sandbox of Edisonabcd. A user sandbox is a subpage of the user's user page. It serves as a testing spot and page development space for the user and is not an encyclopedia article. Create or edit your own sandbox here. Other sandboxes: Main sandbox | Template sandbox Finished writing a draft article? Are you ready to request review of it by an experienced editor for possible inclusion in Wikipedia? Submit your draft for review!

Table of the consistency strength about NF-style theory

Table of the consistency strength about NF-style theory

Beth number	NF-style set theory	ZF-style set theory	Typed-style theory	Higher-order arithmetic
	${\displaystyle {\mathsf {KF}}}$		${\displaystyle [\Pi _{2}^{\mathcal {P}}-{\mathsf {TST}}]^{*}}$  ${\displaystyle [\Pi _{2}^{\mathcal {P}}-{\mathsf {TST}}+\Pi _{1}^{\mathcal {P}}-{\mathsf {Amb}}]^{*}}$ [1]
	${\displaystyle {\mathsf {NFP}}}$ [2]		${\displaystyle {\mathsf {TSTP+Inf}}}$ [3] ${\displaystyle {\mathsf {RTT}}}$ [4]	${\displaystyle \trianglerighteq \ {\mathsf {I\Delta _{0}+exp}},{\mathsf {EFA}}}$  ${\displaystyle \triangleleft \ {\mathsf {PA}}}$
	${\displaystyle {\mathsf {NFU}}}$ [5][6][A],${\displaystyle {\mathsf {MLU}}}$  ${\displaystyle {\mathsf {NFU}}^{-\infty }}$		${\displaystyle {\mathsf {TSTU}}}$ [3]	${\displaystyle {\mathsf {I\Delta _{0}+exp}},{\mathsf {EFA}}}$ [unreliable source]
	${\displaystyle {\mathsf {NF}}_{3}}$ [7]		${\displaystyle {\mathsf {TST}}_{3}^{\infty }}$
${\displaystyle \triangleleft \ \beth _{\omega _{1}}}$ [B]	${\displaystyle {\mathsf {iNF}}}$		${\displaystyle {\mathsf {T}}\mathbb {Z} {\mathsf {T}}}$	${\displaystyle \trianglerighteq \ {\mathsf {I\Delta _{0}+exp}},{\mathsf {EFA}}}$
	${\displaystyle {\mathsf {NFUA}}^{-\infty }}$ [8]	${\displaystyle \mathrm {KPu} ^{r}}$ [9]p. 869		${\displaystyle {\mathsf {PA}}}$
${\displaystyle \beth _{n<\omega }}$ [10] ${\displaystyle \triangleleft \ \beth _{\omega }}$	${\displaystyle {\mathsf {NFU+Inf}}}$ [11], ${\displaystyle {\mathsf {MLU+Inf}}}$		${\displaystyle {\mathsf {TTTU+FlatOP}}}$ [10] ${\displaystyle {\mathsf {TSTU+FlatOP}}}$  ${\displaystyle {\mathsf {TTTU+Inf}}}$  ${\displaystyle {\mathsf {TSTU+Inf}}}$
	${\displaystyle {\mathsf {NFI}}}$ [2][4] ${\displaystyle {\mathsf {NFUB}}^{-\infty }}$ [8] ${\displaystyle {\mathsf {NF}}_{3}+{\mathsf {Inf}}}$ [12]	${\displaystyle {\mathsf {KP}}+\Pi _{\omega }^{\text{set}}-{\mathsf {Separation}}}$	${\displaystyle {\mathsf {TSTI+Inf}}}$ [3] ${\displaystyle {\mathsf {TST}}_{3}^{\infty }+{\mathsf {Inf}}}$ [12] ${\displaystyle \lambda 2}$ [13]	${\displaystyle {\mathsf {Z}}_{2}}$ ,${\displaystyle \Pi _{\infty }^{1}-{\mathsf {CA}}}$
${\displaystyle \trianglerighteq \beth _{\omega }}$  ${\displaystyle \triangleleft \ \beth _{\omega _{1}}}$ [14]	${\displaystyle {\mathsf {NF}}}$ , ${\displaystyle {\mathsf {ML}}}$ [15] ${\displaystyle {\mathsf {KF}}+\exists }$  Universal set ${\displaystyle {\mathsf {NFI}}}$  + Axiom of union, ${\displaystyle {\mathsf {NFP}}}$  + Axiom of union ${\displaystyle {\mathsf {NF}}_{4}}$ , ${\displaystyle {\mathsf {NF}}_{3}+}$ (there exists the set ${\displaystyle \{\{\{x\},y\}/x\in y\}}$ )[16]	${\displaystyle {\mathsf {MACQ}}}$ [3] ${\displaystyle \triangleleft \ {\mathsf {MAC+}}}$ (a tangled web of cardinals)[17]	${\displaystyle {\mathsf {TTT}}}$  ${\displaystyle {\mathsf {TST+Amb}}}$  ${\displaystyle \trianglelefteq \ {\mathsf {TST+Inf}}}$
	${\displaystyle {\mathsf {NF}}+V}$  is linearly ordered
	${\displaystyle {\mathsf {NF}}+{\mathcal {L}}_{\omega _{1},\omega }(\omega )}$ [18] ${\displaystyle {\mathsf {NF}}+}$ the NF set ${\displaystyle \mathbb {N} \land {\mathcal {P}}(\mathbb {N} )}$  are the real external ones
${\displaystyle \beth _{\beth _{n<\omega }}}$ [10] ${\displaystyle \triangleleft \ \beth _{\beth _{\omega }}}$	${\displaystyle {\mathsf {NFUR}}}$
	${\displaystyle {\mathsf {NFU*}}}$ [19]	${\displaystyle {\mathsf {Z}}^{-}+\Sigma _{2}\!-\!{\mathsf {Replacement}}}$
	${\displaystyle {\mathsf {NFUA}}}$ [10]	${\displaystyle {\mathsf {ZFC}}+N-{\mathsf {Mahlo}}}$  ${\displaystyle {\mathsf {NBG}}+N-{\mathsf {Mahlo}}}$
	${\displaystyle {\mathsf {NFUB}}}$ [10] ${\displaystyle {\mathsf {NFUB}}^{-}}$	${\displaystyle {\mathsf {MK}}+\mathbf {Ord} {\mathsf {\ is\ weakly\ compact}}}$  ${\displaystyle {\mathsf {ZFC-Pow+}}}$ (there is a weakly compact cardinal)
	${\displaystyle {\mathsf {NFUM}}}$ [10]	${\displaystyle {\mathsf {MKU}}}$  ${\displaystyle {\mathsf {MK}}+\mathbf {Ord} {\mathsf {\ is\ measurable}}}$

Key

This is a list of symbols used in this table:

• ${\displaystyle A\triangleleft \ B}$  represents ${\displaystyle B\vdash {\text{Con}}(A)}$  .
• ${\displaystyle A\trianglelefteq B}$  represents ${\displaystyle {\text{Con}}(B)\to {\text{Con}}(A)}$ .
• ${\displaystyle {\mathsf {Inf}}}$  in this table only denotes "exist a Dedekind infinite set".

All theories that do not have sufficient information to infer their consistency strength ordering, but whose consistency proofs are explicit, are colored yellow. All theories without consistency proofs are colored orange.

This is a list of the abbreviations used in this table:

• NF-style set theory
  • ${\displaystyle {\mathsf {KF}}}$  is a subsystem of both ${\displaystyle {\mathsf {NF}}}$  and ${\displaystyle {\mathsf {Z}}^{-}}$ , axiomatized as extensionality, pair set, power set, sumset, and stratified ${\displaystyle \Delta _{0}^{\mathcal {P}}}$  separation.
  • ${\displaystyle {\mathsf {NFI}}}$  is a subsystem of ${\displaystyle {\mathsf {NF}}}$ , axiomatized as untyped ${\displaystyle {\mathsf {TTI}}}$ .
  • ${\displaystyle {\mathsf {NFP}}}$  is a subsystem of ${\displaystyle {\mathsf {NF}}}$  like ${\displaystyle {\mathsf {NFI}}}$ , axiomatized as untyped ${\displaystyle {\mathsf {TTP}}}$ .
  • ${\displaystyle {\mathsf {NF}}_{3}}$  is a subsystem of ${\displaystyle {\mathsf {NF}}}$ , in which only comprehension is restricted to those formulae which can be stratified using no more than three types. It is not clear whether it is appropriate to put ${\displaystyle {\mathsf {NF}}_{3}}$  on this row.
  • ${\displaystyle {\mathsf {NFU}}}$  see NF with urelements.^A It is not recommended to read references that are too old and can be read instead ^[11]
  • ${\displaystyle {\mathsf {MLU}}}$  is ${\displaystyle {\mathsf {ML}}}$  with urelements.
  • ${\displaystyle {\mathsf {iNF}}}$  the system of set theory that has the same nonlogical axioms as ${\displaystyle {\mathsf {NF}}}$  but is embedded in an intuitionistic logic. ${\displaystyle {\mathsf {INF}}}$ , ${\displaystyle {\mathsf {iNF}}}$ , ${\displaystyle i{\mathsf {NF}}}$ , and ${\displaystyle {\mathsf {constructive\ NF}}}$  are the same theory.^B It is not clear whether it is appropriate to put ${\displaystyle {\mathsf {iNF}}}$  on this row, because we just have ${\displaystyle {\mathsf {NF}}\trianglerighteq {\mathsf {iNF}}\trianglerighteq {\mathsf {NFU}}}$  and don't have a proof for ${\displaystyle {\mathsf {iNF}}\trianglerighteq {\mathsf {HA}}}$  and ${\displaystyle {\mathsf {iNF}}\vdash {\mathsf {Inf}}}$ . That is, there might be a largest finite cardinal ${\displaystyle |U|}$ , which would contain a finite set U that is "unenlargeable", that not exist ${\displaystyle {\mathsf {iNF}}}$  set ${\displaystyle x\not \in U}$ .^[20]
  • ${\displaystyle {\mathsf {NF}}}$  see New Foundations#Definition.
  • ${\displaystyle {\mathsf {ML}}}$  is the theory obtained by adding class notion to ${\displaystyle {\mathsf {NF}}}$ . ^[21]Its equiconsistency with ${\displaystyle {\mathsf {NF}}}$  implies that we cannot prove anything about classes that are not ${\displaystyle {\mathsf {NF}}}$  sets.
  • ${\displaystyle {\mathsf {NF}}+V}$  is linearly ordered, There is currently no proof of its consistency.
  • ${\displaystyle {\mathsf {NF}}+{\mathcal {L}}_{\omega _{1},\omega }(\omega )}$  is ${\displaystyle {\mathsf {NF}}}$  + comprehension for stratified formules of the language ${\displaystyle {\mathcal {L}}_{\omega _{1},\omega }}$  using only finitely many types. Its model are exactly the models for which the NF set ${\displaystyle \mathbb {N} \land {\mathcal {P}}(\mathbb {N} )}$  are the real external ones.
  • ${\displaystyle {\mathsf {NFUR}}}$  axiomatized as ${\displaystyle {\mathsf {NFU+Inf}}+\mathbb {N} {\mathsf {\ is\ SC}}}$ .
  • ${\displaystyle {\mathsf {NFU*}}}$  axiomatized as ${\displaystyle {\mathsf {NFU+SCS}}+\mathbb {N} {\mathsf {\ is\ SC}}}$ .
  • ${\displaystyle {\mathsf {NFUA}}}$  axiomatized as ${\displaystyle {\mathsf {NFU+Inf}}+{\mathsf {C\ is\ SC}}}$ .
  • ${\displaystyle {\mathsf {NFUB}}}$  axiomatized as ${\displaystyle {\mathsf {NFUA+SO}}}$ .
  • ${\displaystyle {\mathsf {NFUB}}^{-}}$  axiomatized as ${\displaystyle {\mathsf {NFU+Inf}}+{\mathsf {C\ is\ SC}}+{\mathsf {SO}}}$ .
  • ${\displaystyle {\mathsf {NFUM}}}$  axiomatized as ${\displaystyle {\mathsf {NFUB}}^{-}+{\mathsf {LO}}}$ .
  • ${\displaystyle {\mathsf {NFU}}^{-\infty }}$  axiomatized as ${\displaystyle {\mathsf {NFU}}+V}$  is finite.
  • ${\displaystyle {\mathsf {NFUA}}^{-\infty }}$  axiomatized as ${\displaystyle {\mathsf {NFU}}^{-\infty }+{\mathsf {C\ is\ SC}}}$ .
  • ${\displaystyle {\mathsf {NFUB}}^{-\infty }}$  axiomatized as ${\displaystyle {\mathsf {NFUA}}^{-\infty }+{\mathsf {SO}}}$ .

The axioms listed below are higher infinite axioms specific to NF-style set theory, and they also apply to NF-style type theory. When used individually, they are not necessarily very strong in the traditional sense (such as ${\displaystyle \trianglerighteq {\text{Con}}({\textsf {ZFC}})}$ ), but when used in combination, they are indeed very strong.

• NF-style higher infinite
  • ${\displaystyle \mathbb {N} {\mathsf {\ is\ SC}}}$  or ${\displaystyle {\mathsf {Count}}}$  is Rosser's Axiom of Counting, which asserts that the set of natural numbers is a strongly Cantorian set.
  • ${\displaystyle {\mathsf {SCS}}}$  is Axiom of strongly Cantorian separation, which asserts that for any strongly Cantorian set A and any formula ${\displaystyle \phi }$  (not necessarily stratified) the set ${\displaystyle \{x\in A|\;\phi \}}$  exists.
  • ${\displaystyle {\mathsf {C\ is\ SC}}}$  is Axiom of Cantorian Sets, which asserts that Every Cantorian set is strongly Cantorian.
  • ${\displaystyle {\mathsf {LO}}}$  is Axiom of Large Ordinals, which asserts that for each non-Cantorian ordinal ${\displaystyle \alpha }$ , there is a natural number n such that ${\displaystyle T^{n}(\Omega )<\alpha }$ .
  • ${\displaystyle {\mathsf {SO}}}$  is Axiom of Small Ordinals, which asserts that for any formula ${\displaystyle \phi }$  (not necessarily stratified), there is a set A such that the elements of A which are strongly Cantorian ordinals are exactly the strongly Cantorian ordinals such that ${\displaystyle \phi }$ .

• ZF-style set theory
  • ${\displaystyle {\mathsf {MAC}}}$  see Mac Lane set theory.
  • ${\displaystyle {\mathsf {MACQ}}}$  as ${\displaystyle {\mathsf {MAC}}}$  with foundation weakened to allow Quine atoms and an axiom scheme asserting the existence of an n-tree of cardinals for each concrete natural number n.
  • A tangled web of cardinals is a tangled web of cardinals of order ${\displaystyle \tau }$ . For any infinite ordinal ${\displaystyle \alpha }$ , a tangled web of cardinals of order ${\displaystyle \alpha }$  is a function ${\displaystyle \tau }$  from the set of nonempty sets of ordinals with ${\displaystyle \alpha }$  as maximum to cardinals such that

1. If ${\displaystyle |A|>1,\tau (A_{1})=2^{\tau (A)}}$ .
2. If ${\displaystyle |A|\leq n}$ , the first order theory of a natural model of ${\displaystyle {\mathsf {TST}}_{n}}$  with base type ${\displaystyle \tau (A)}$  is completely determined by ${\displaystyle A\backslash A_{n}}$ , the n smallest elements of ${\displaystyle A}$ .

• • ${\displaystyle {\mathsf {Z}}^{-}}$  see Zermelo set theory.
  • ${\displaystyle {\mathsf {ZFC}}}$  see Zermelo–Fraenkel set theory.
  • ${\displaystyle {\mathsf {NBG}}}$  see Von Neumann–Bernays–Gödel set theory.
  • ${\displaystyle {\mathsf {MK}}}$  see Morse–Kelley set theory.
  • ${\displaystyle {\mathsf {MKU}}}$  axiomatized as ${\displaystyle {\mathsf {MK}}+}$  "there is a ${\displaystyle \kappa }$ -complete nonprincipal ultrafilter on the proper class ordinal ${\displaystyle \kappa }$ ".

• Higher infinite
  • ${\displaystyle N-{\mathsf {Mahlo}}}$  is a schema asserting the existence of an n-Mahlo cardinal for each concrete natural number n, and doesn't prove that n-Mahlo cardinals exist forall n, thus allowing for nonstandard counterexamples.
  • ${\displaystyle n<\omega -{\mathsf {Mahlo}}}$  asserts that there are n-Mahlo cardinals for every n.
  • ${\displaystyle {\mathsf {weakly\ compact}}}$  see weakly compact cardinal.
  • ${\displaystyle {\mathsf {measurable}}}$  see measurable cardinal.

• Type-style theory
  • ${\displaystyle {\mathsf {FlatOP}}}$  see New Foundations#Ordered pairs, is Axiom of type-level ordered pair, which can also be called flat ordered pair. In models without the Axiom of Choice ${\displaystyle {\mathsf {AC}}}$ , the existence of a type-level ordered pair implies but is not equivalent to the existence of an infinite set, but NFU with the axiom "there is an infinite set" interprets NFU with a type-level pair in a straightforward manner. It's well-known that proofs concerning like ${\displaystyle \alpha }$ -strong cardinals run into problems if one doesn't use the flat ordered pair, and this is no different from ZF-style set theory.
  • ${\displaystyle {\mathsf {Amb}}}$  is typical ambiguity axiom, which asserts that validity for closed predicates is invariant under shifts of type levels.
  • ${\displaystyle {\mathsf {TSTI}}}$  or ${\displaystyle {\mathsf {TTI}}}$  is a subsystem of ${\displaystyle {\mathsf {TST}}}$ , axiomatized as unrestricted extensionality and those instances of comprehension in which no variable is assigned a type higher than that of the set asserted to exist.
  • ${\displaystyle {\mathsf {TSTP}}}$  or ${\displaystyle {\mathsf {TTP}}}$  is a subsystem of ${\displaystyle {\mathsf {TST}}}$  like ${\displaystyle {\mathsf {TSTI}}}$ , in which only free variables are allowed to have the type of the set asserted to exist by an instance of comprehension.
  • ${\displaystyle {\mathsf {RTT}}}$  axiomatized as Principia Mathematica ramified type theory without the axiom of reducibility.
  • ${\displaystyle {\mathsf {TTU}}}$  is ${\displaystyle {\mathsf {TTT}}}$  with urelements, and ${\displaystyle {\mathsf {NFU}}}$  is untyped ${\displaystyle {\mathsf {TTU}}}$ .
  • ${\displaystyle {\mathsf {TSTU}}}$  is ${\displaystyle {\mathsf {TST}}}$  with urelements, and ${\displaystyle {\mathsf {NFU}}}$  is untyped ${\displaystyle {\mathsf {TSTU}}}$ .
  • ${\displaystyle {\mathsf {T}}\mathbb {Z} {\mathsf {T}}}$  is Simple theory of types with all integer types, it has a realizability model and computational interpretation and is therefore consistent, and ${\displaystyle {\mathsf {iNF}}}$  is untyped ${\displaystyle {\mathsf {T}}\mathbb {Z} {\mathsf {T}}}$ .
  • ${\displaystyle {\mathsf {TTT}}}$  see New Foundations#Tangled Type Theory. ${\displaystyle {\mathsf {NF}}}$  is untyped ${\displaystyle {\mathsf {TTT}}}$ .
  • ${\displaystyle {\mathsf {TST}}}$  or ${\displaystyle {\mathsf {TT}}}$  see New Foundations#Typed Set Theory. ${\displaystyle {\mathsf {NF}}}$  is untyped ${\displaystyle {\mathsf {TTT}}}$ .
  • ${\displaystyle {\mathsf {TST}}_{k}}$  is ${\displaystyle {\mathsf {TST}}}$  restricted to levels 0 to k − 1, forall k > 2.
  • ${\displaystyle {\mathsf {TST}}_{k}^{\infty }}$  is ${\displaystyle {\mathsf {TST}}_{k}+}$ "level 0 contains ≥ n things for every concrete n."
  • ${\displaystyle {\mathsf {TST}}_{3}^{\infty }}$  is ${\displaystyle {\mathsf {TST}}_{k}^{\infty }}$  restricted to k = 3.

• Higher-order arithmetic
  • ${\displaystyle {\mathsf {I\Delta _{0}+exp}}}$  is arithmetic with induction restricted to Δ0-predicates without any axiom asserting that exponentiation is total.
  • ${\displaystyle {\mathsf {EFA}}}$  see elementary function arithmetic.
  • ${\displaystyle {\mathsf {PA}}}$  see Peano arithmetic.
  • ${\displaystyle {\mathsf {Z}}_{2}}$  see Second-order arithmetic.

Notes

1. Forster, Thomas; Kaye, Richard (March 1991). "End-extensions preserving power set". The Journal of Symbolic Logic. 56 (1). doi:10.2307/2274922. ISSN 0022-4812.
2. Crabbé, Marcel (1982). "On the Consistency of an Impredicative Subsystem of Quine's NF". The Journal of Symbolic Logic. 47 (1). doi:10.2307/2273386. ISSN 0022-4812.
3. Holmes, M. Randall (1995). "The Equivalence of NF-Style Set Theories with "Tangled" Theories; The Construction of ω-Models of Predicative NF (and more)" (PDF). The Journal of Symbolic Logic. 60 (1). doi:10.2307/2275515. ISSN 0022-4812. Retrieved 2025-07-17.
4. Holmes, M. Randall (1999-04-01). "Subsystems of Quine's ``New Foundations with Predicativity Restrictions" (PDF). Notre Dame Journal of Formal Logic. 40 (2). doi:10.1305/ndjfl/1038949535. ISSN 0029-4527. Retrieved 2025-07-15.
5. Jensen, Ronald Björn (1968). "On the Consistency of a Slight (?) Modification of Quine's "New Foundations"". Synthese. 19 (1/2). ISSN 0039-7857.
6. Boffa, Maurice (1988). "ZFJ and the consistency problem for NF". Jahrbuch der Kurt Gödel Gesellschaft. 1 (102–106): 75--79.
7. Grishin, Vyacheslav Nikolaevich (1969). "Consistency of a fragment of Quine's NF system". Doklady Akademii Nauk SSSR (in Russian). 189 (2): 241--243 – via Russian Academy of Sciences.
8. Enayat, Ali and Kalantari, Iraj and Moniri, Mojtaba (2006). "From bounded arithmetic to second order arithmetic via automorphisms". Logic in Tehran. 26. Association for Symbolic Logic: 87--113.
9. G. Jäger, "The Strength of Admissibility Without Foundation". Journal of Symbolic Logic vol. 49, no. 3 (1984).
10. Holmes, M. Randall (2001). "Strong Axioms of Infinity in NFU" (PDF). The Journal of Symbolic Logic. 66 (1). doi:10.2307/2694912. ISSN 0022-4812. Retrieved 2025-07-15.
11. Adlešić, Tin; Čačić, Vedran (2024-12-13). "Boffa's construction and models for NFU". Studia Logica. doi:10.1007/s11225-024-10155-9. ISSN 1572-8730.
12. Pabion, J. F. (1980). "TT₃ + AxInf est équivalent à l'arithmétique du second ordre" (PDF). Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) (in French). 290: 1117--1118.
13. Blot, Valentin (2022-08-02). "A direct computational interpretation of second-order arithmetic via update recursion". Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. ACM: 1–11. doi:10.1145/3531130.3532458. ISBN 978-1-4503-9351-5.
14. Holmes, M. Randall; Wilshaw, Sky. "NF is Consistent" (version last ed.). arXiv:1503.01406. doi:10.48550/arXiv.1503.01406.
15. Wang, Hao (March 1950). "A formal system of logic". The Journal of Symbolic Logic. 15 (1). doi:10.2307/2268438. ISSN 0022-4812. Retrieved 2025-07-17.
16. Grishin, Vyacheslav Nikolaevich (1972). "The method of stratification in set theory". Russian, Ph. D. thesis, Moscow University (in Russian). 3 – via Russian Academy of Sciences.
17. Holmes, M. Randall; Wilshaw, Sky. "NF is Consistent" (version 22 ed.). arXiv:1503.01406v22.
18. Esser, Olivier and Forster, Thomas (2007). "Relaxing stratification" (PDF). Bulletin of the Belgian Mathematical Society-Simon Stevin. 14 (2). The Belgian Mathematical Society: 247--258. Archived from the original (PDF) on 2025-08-13. Retrieved 2025-08-13.
19. Solovay, Robert (2025-07-23). "The consistency strength of NFU_star". Archived from the original on 2025-07-23. Retrieved 2025-07-23.
20. Forster, Thomas E (2009). "A tutorial on constructive NF" (PDF). Proceedings of the 70th anniversary NF meeting in Cambridge. 16. Archived from the original (PDF) on 2025-07-18. Retrieved 2025-07-18.
21. Quine, Willard Van Orman (1976). Mathematical logic (Rev. ed., 8th print ed.). Cambridge [Mass.]: Harvard university press. ISBN 978-0-674-55450-4.