2
$\begingroup$

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?

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

1 Answer 1

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$
    – Frode Alfson Bjørdal
    Commented Sep 21, 2023 at 0:00
  • 2
    $\begingroup$ 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$. $\endgroup$
    – Andreas Blass
    Commented Sep 21, 2023 at 0:07
  • $\begingroup$ Do we agree, then, that $\forall x(Gx\leftrightarrow\forall K((A(K,x)\to Kx)\to Kx))$ is a recursive definition of G? $\endgroup$
    – Frode Alfson Bjørdal
    Commented Oct 16, 2023 at 23:59
  • 1
    $\begingroup$ @FrodeAlfsonBjørdal Yes, that definition of $G$ looks good (assuming of course that $A$ describes a monotone operation). $\endgroup$
    – Andreas Blass
    Commented Oct 17, 2023 at 0:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .