# Impredicativity, definition, recursion and conservatism

Suppose we in an impredicative framework isolate the fixed point

$$Gx\leftrightarrow A(G,x)$$

from a $$Gx$$ obtained by $$\Pi^1_1$$-comprehension as equivalent to $$\forall K((A(K,x)\to Kx)\to Kx)$$, where $$K$$ only occurs positively in $$A(K,x)$$.

May we take $$Gx\leftrightarrow A(G,x)$$ to be a recursive definition of $$Gx$$ in terms of $$A(G,x)$$?

(1) If so, may that not conflict with the requirement that definitions should be conservative?

(2) If not, what else may/should we consider $$Gx\leftrightarrow A(G,x)$$ to be?

• What's the point of displaying source code? this is not pleasant to decipher...
– YCor
Sep 20 at 17:07
• @YCor Resolved. It seems to me that there was an update on how to code. Sep 20 at 17:19
• Re, we've discussed elsewhere that \\$\$/extract_itex] works, but  and even  don't, for technical reasons. (Just for fun, for \[$ it's \$\$, not \\\$\\\$.) Sep 20 at 18:31

The formula $$Gx\leftrightarrow A(G,x)$$, expressing that $$G$$ is a fixed-point of the operator defined by $$A$$, is not sufficient, by itself, to uniquely characterize $$G$$. That operator may have many fixed-points, of which $$\forall K(\forall y(A(K,y)\to Ky)\to Kx)$$ is the smallest. (The similar formula in the question is incorrect because it lacks the universal quantifier governing the antecedent of the outer implication. I've added the quantifier and renamed the bound variable to avoid confusion with the free variable $$x$$ in the consequent.)
So $$Gx\leftrightarrow A(G,x)$$ does not serve as a definition of $$G$$. It would need to be supplemented by the additional information that it is the smallest among all such $$G$$'s. One way to say this is $$\forall G'((\forall x(G'x\leftrightarrow A(G',x))) \to \forall x(Gx\to G'x)).$$ You asked about taking $$Gx\leftrightarrow A(G,x)$$ as a recursive definition of $$G$$. If you meant by this simply a definition that happens to be recursive, then what I wrote above applies. But if you meant something else, and if that something else included a leastness requirement, then $$Gx\leftrightarrow A(G,x)$$ could serve as a definition.
• Suppose T is ACA_0 + $\forall x(Gx\leftrightarrow A(x,G))$. May not T be stronger than ACA_0, so that $\forall x(Gx\leftrightarrow A(x,G))$ is not conservative? Sep 21 at 0:00
• If you add to $ACA_0$ an axiom saying that every arithmetical operator $A$ has a least fixed point, then you can obtain a $\Pi^1_1$-complete set as a fixed point, so the system would be at least as strong as $\Pi^1_1$-$CA_0$. If you only added existence of a fixed point but not minimality, then I'd expect the result to be $ATR_0$ or nearby. So in either case, I don't expect conservativity over $ACA_0$. Sep 21 at 0:07
• Do we agree, then, that $\forall x(Gx\leftrightarrow\forall K((A(K,x)\to Kx)\to Kx))$ is a recursive definition of G? Oct 16 at 23:59
• @FrodeAlfsonBjørdal Yes, that definition of $G$ looks good (assuming of course that $A$ describes a monotone operation). Oct 17 at 0:42