Return to Question

Suppose we in an impredicative framework isolate the fixed point

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

from a $Gx$ obtained by $\Pi^1_1$-comprehension via $\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?

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?

Suppose we in an impredicative framework isolate the fixed point

$Gx\leftrightarrow A(G,x)$

from a $Gx$ obtained by $\Pi^1_1$-comprehension via $\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?

Suppose we in an impredicative framework isolate the fixed point

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

from a $Gx$ obtained by $\Pi^1_1$-comprehension via $\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?

Suppose we in an impredicative framework obtain the fixed point

$Gx\leftrightarrow A(G,x)$

from a $Gx$ obtained by $\Pi^1_1$-comprehension via $\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?

Suppose we in an impredicative framework isolate the fixed point

$Gx\leftrightarrow A(G,x)$

from a $Gx$ obtained by $\Pi^1_1$-comprehension via $\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?