In [positive set theory](https://www.sciencedirect.com/science/article/pii/B9780444516213500086?via%3Dihub), the axiom scheme of generalized positive comprehension in $GPK^+\_\infty$ [of Olivier Esser] is stated in a manner as to forbid the symbol of the asserted set to occur in the defining formula. 


To quote from the above source:



> 
> **Positive Comprehension:** For any positive formula $\phi$ in which $A$ does not appear, $(\exists A.(\forall x.x \in A \leftrightarrow
>  \phi)).$
> 
> 
> 


Where a positive formula is defined as:



> 
> **Deﬁnition:** Let the class of (bounded) positive formulas be the smallest class containing the formula $x \neq x$ (useful because
>  uniformly false), all atomic formulas, and closed under conjunction,
>  disjunction, bounded universal quantiﬁcation $(\forall x \in A.\phi)$
>  and existential quantiﬁcation $(∃x ∈ A.φ)$.
> 
> 
> 


Question 1: Is there a clear inconsistency involved with permitting symbol $A$ to occur in $\phi$, in the statement of positive comprehension?


Question 2: Suppose that there is no clear inconsistency, then would that allowance results in increment in consistency strength over the original system?



Can we have cyclic generalized positive comprehension?
Yes, there is a clear inconsistency, take the formula:


$\exists A.\ (\forall x.\ (x\in A \leftrightarrow A=\emptyset))$.


Clearly, such a set $A$ cannot exist: if $A\neq \emptyset$, then any $x\in A$ would give a contradiction. If $A=\emptyset$, then this formula would imply that any $x$ satisfies $x\in A$, but then $A\neq \emptyset$.


