The Axiom Scheme of Acyclic Comprehension
A “new” criterion for set existence is presented, namely, that a set {x | φ} should exist if the multigraph whose nodes are variables in φ and whose edges are occurrences of atomic formulas in φ is acyclic. Formulas with acyclic graphs are stratified in the sense of New Foundations, so consistency of the set theory with weak extensionality and acyclic comprehension follows from the consistency of Jensen’s system NFU . It is much less obvious, but turns out to be the case, that this theory is equivalent to NFU : it appears at first blush that it ought to be weaker. This paper verifies that acyclic comprehension and stratified comprehension are equivalent, by verifying that each axiom in a finite axiomatization of stratified comprehension follows from acyclic comprehension. keywords: New Foundations, NFU, stratification, acyclic AMS Subject Classification Code: 03E70 The first author, who is a neurologist with an amateur interest in mathematical logic, proposed the criterion of acyclic comprehension for existence of sets (originally under another name) as an approach to the historical paradoxes of set theory, and communicated this to the second author. The second author noted that stratified comprehension implies acyclic comprehension, so the scheme of acyclic comprehension is certainly consistent relative to quite weak accepted theories (as the scheme of stratified comprehension is a subtheory of NFU , which was shown to be consistent by R. B. Jensen in [6]). The second author also conjectured that the scheme was very weak (meaning not equivalent to full stratified comprehension). The first author realized that one could attack this problem by attempting to prove all propositions in a finite axiomatization of stratified comprehension (that stratified comprehension is finitely axiomatizable was originally shown in [4], though the axiomatization given there is very unpleasant to work with). Undaunted by the skepticism of the second author, he proceeded to prove that each of the axioms of the finite axiomatization used in the second author’s [5] (adapted to the Wiener ordered pair of [9]) follows from Date: May19th, 2011 – submitted version.