<p>I have <a href="https://mathoverflow.net/questions/480056/can-a-positive-elementary-inductive-definition-refer-to-its-own-stage-comparison">cross-posted</a> this question to MO</p>
<hr />
<p>Moschovakis' stage comparison theorem says that the <em>stage comparison relation</em> associated with any positive elementary induction is itself definable by (another) positive elementary induction. But what if we augmented a positive elementary induction by the ability to refer to its own stage-comparison relation, at least with regards to elements that already appear at some prior stage of the induction? Is the resulting least fixed-point still inductive?</p>
<p>Formally: Suppose <span class="math-container">$\varphi(x,R,S)$</span> is a first-order formula in a signature <span class="math-container">$L$</span> with <em>two</em> second-order variables: a unary relation symbol <span class="math-container">$S$</span> and a binary relation symbol <span class="math-container">$R$</span>. Suppose <span class="math-container">$R$</span> and <span class="math-container">$S$</span> each only appear positively in <span class="math-container">$\varphi$</span> (i.e., under an even number of negations).</p>
<p>I will define ordinal-indexed families of unary relations <span class="math-container">$S^\alpha$</span> and binary relations <span class="math-container">$R^\alpha$</span> on that structure as follows:</p>
<ul>
<li><span class="math-container">$S^0 := \emptyset$</span></li>
<li><span class="math-container">$R^\alpha(x,y)$</span> means ``there is some <span class="math-container">$\iota &lt; \jmath \le \alpha$</span> such that <span class="math-container">$x \in S^\iota$</span>, <span class="math-container">$y \in S^\jmath$</span>, and <span class="math-container">$y \notin S^\ell$</span> for any <span class="math-container">$\ell &lt; \jmath$</span>.''</li>
<li><span class="math-container">$S^{\alpha + 1} := \{x:\varphi(x,R^\alpha,S^\alpha)\}$</span>, and</li>
<li>For limit ordinals <span class="math-container">$\gamma$</span>, <span class="math-container">$S^\gamma := \bigcup_{\alpha &lt; \gamma} S^\alpha$</span>.</li>
</ul>
<p>(All definitions are with respect to a fixed implicit <span class="math-container">$L$</span>-structure)</p>
<p>I claim that the sequence <span class="math-container">$S^\alpha$</span> is monotone in <span class="math-container">$\alpha$</span>. (Note that monotonicity of <span class="math-container">$R^\alpha$</span> follows immediately from definition of <span class="math-container">$R$</span>.) Let's prove by induction on <span class="math-container">$\beta$</span> that for all <span class="math-container">$\alpha &lt; \beta$</span>, <span class="math-container">$S^\alpha \subseteq S^\beta$</span>. At successor stages (<span class="math-container">$\beta = \delta + 1$</span>) it suffices to observe that <span class="math-container">$S^\delta \subseteq S^{\delta + 1}$</span>: if <span class="math-container">$x \in S^\delta$</span> then <span class="math-container">$\varphi(x,R^\alpha,S^\alpha)$</span> for some <span class="math-container">$\alpha \le \delta$</span>, so <span class="math-container">$x \in S^{\delta + 1}$</span> as both <span class="math-container">$R$</span> and <span class="math-container">$S$</span> occur positively in <span class="math-container">$\varphi$</span>. For limit ordinals <span class="math-container">$\beta$</span> and <span class="math-container">$\alpha &lt; \beta$</span>, <span class="math-container">$S^\alpha \subseteq S^\beta$</span> immediately by definition of <span class="math-container">$S^\beta$</span>.</p>
<p>Since <span class="math-container">$S^\alpha$</span> is monotone in <span class="math-container">$\alpha$</span>, there is some least ordinal (the <em>closure ordinal</em>) <span class="math-container">$\Gamma$</span> such that <span class="math-container">$S^\alpha$</span> stabilizes past <span class="math-container">$\Gamma$</span> (i.e., for all <span class="math-container">$\Gamma \le \alpha &lt; \beta$</span>, <span class="math-container">$S^\alpha = S^\beta$</span>). At this point, <span class="math-container">$R^\Gamma$</span> is just the stage comparison relation associated with this induction.</p>
<p><strong>Question:</strong> Is <span class="math-container">$S^\Gamma$</span> inductive? I.e., is there a positive elementary <span class="math-container">$L$</span>-formula <span class="math-container">$\psi(x,T)$</span> such that the least fixed-point of <span class="math-container">$\psi$</span> is <span class="math-container">$S^\Gamma$</span>?</p>
<p>(I'd guess that if the answer is <em>yes,</em> then we should be able to find such a <span class="math-container">$\psi$</span> that's independent of the underlying <span class="math-container">$L$</span>-structure, though I have no good reason for that.)</p>

CC BY-SA 4.0
2023-10-25T06:13:29.580Z
You introduce $\varphi$ as a binary symbol (it takes $x$ and $S$) but then later on you use it as a unary symbol (you write $\varphi(\varphi^\alpha)$. What's going on?
Andrej Bauer
CC BY-SA 4.0
2023-10-25T16:35:01.413Z
In a nutshell: currying. In general $S$ is a $n$-ary relation symbol and $x$ is a $n$-tuple of variables, for some $n$. Then by $\varphi(S)$ I mean $\{x : \varphi(x,S)\}$.
Siddharth
CC BY-SA 4.0
2023-11-03T14:06:38.603Z
Just to check: are you fixing the underlying language to be the language of arithmetic?
Anupam Das
CC BY-SA 4.0
2023-11-06T20:41:21.043Z
Not necessarily. I'm wondering if this holds for arbitrary first-order structures (the setting of the original stage comparison theorem). But if there are solutions for particular cases, I'm interested in that too.
Siddharth
CC BY-SA 4.0
2023-11-07T10:42:17.517Z
Okay. Also, can you perhaps edit the question to be more precise about the definition of the operator $\varphi(X,R)$ ($X$ unary, $R$ binary in place of $\prec$)? It's still unclear to me how precisely you are seeing this as a monotone operator.
Anupam Das
CC BY-SA 4.0
2024-01-06T18:15:52.903Z
Done (at last).
Siddharth
<pl.programming-languages><finite-model-theory><model-theory>
Can a positive elementary inductive definition refer to its own stage comparison relation?
Siddharth
# Can a positive elementary inductive definition refer to its own stage comparison relation?

(Asked by: username_0 on 2023-10-23)

I have [cross-posted](https://mathoverflow.net/questions/480056/can-a-positive-elementary-inductive-definition-refer-to-its-own-stage-comparison) this question to MO

---

Moschovakis' stage comparison theorem says that the *stage comparison relation* associated with any positive elementary induction is itself definable by (another) positive elementary induction. But what if we augmented a positive elementary induction by the ability to refer to its own stage-comparison relation, at least with regards to elements that already appear at some prior stage of the induction? Is the resulting least fixed-point still inductive?

Formally: Suppose $\varphi(x,R,S)$ is a first-order formula in a signature $L$ with *two* second-order variables: a unary relation symbol $S$ and a binary relation symbol $R$. Suppose $R$ and $S$ each only appear positively in $\varphi$ (i.e., under an even number of negations).

I will define ordinal-indexed families of unary relations $S^\alpha$ and binary relations $R^\alpha$ on that structure as follows:

* $S^0 := \emptyset$
* $R^\alpha(x,y)$ means ``there is some $\iota < \jmath \le \alpha$ such that $x \in S^\iota$, $y \in S^\jmath$, and $y \notin S^\ell$ for any $\ell < \jmath$.''
* $S^{\alpha + 1} := \{x:\varphi(x,R^\alpha,S^\alpha)\}$, and
* For limit ordinals $\gamma$, $S^\gamma := \bigcup\_{\alpha < \gamma} S^\alpha$.

(All definitions are with respect to a fixed implicit $L$-structure)

I claim that the sequence $S^\alpha$ is monotone in $\alpha$. (Note that monotonicity of $R^\alpha$ follows immediately from definition of $R$.) Let's prove by induction on $\beta$ that for all $\alpha < \beta$, $S^\alpha \subseteq S^\beta$. At successor stages ($\beta = \delta + 1$) it suffices to observe that $S^\delta \subseteq S^{\delta + 1}$: if $x \in S^\delta$ then $\varphi(x,R^\alpha,S^\alpha)$ for some $\alpha \le \delta$, so $x \in S^{\delta + 1}$ as both $R$ and $S$ occur positively in $\varphi$. For limit ordinals $\beta$ and $\alpha < \beta$, $S^\alpha \subseteq S^\beta$ immediately by definition of $S^\beta$.

Since $S^\alpha$ is monotone in $\alpha$, there is some least ordinal (the *closure ordinal*) $\Gamma$ such that $S^\alpha$ stabilizes past $\Gamma$ (i.e., for all $\Gamma \le \alpha < \beta$, $S^\alpha = S^\beta$). At this point, $R^\Gamma$ is just the stage comparison relation associated with this induction.

**Question:** Is $S^\Gamma$ inductive? I.e., is there a positive elementary $L$-formula $\psi(x,T)$ such that the least fixed-point of $\psi$ is $S^\Gamma$?

(I'd guess that if the answer is *yes,* then we should be able to find such a $\psi$ that's independent of the underlying $L$-structure, though I have no good reason for that.)

**Tags:** pl.programming-languages, finite-model-theory, model-theory
> **Comments:**
> **username_1**: You introduce $\varphi$ as a binary symbol (it takes $x$ and $S$) but then later on you use it as a unary symbol (you write $\varphi(\varphi^\alpha)$. What's going on?  
> **username_0**: In a nutshell: currying. In general $S$ is a $n$-ary relation symbol and $x$ is a $n$-tuple of variables, for some $n$. Then by $\varphi(S)$ I mean $\{x : \varphi(x,S)\}$.  
> **username_2**: Just to check: are you fixing the underlying language to be the language of arithmetic?  
> **username_0**: Not necessarily. I'm wondering if this holds for arbitrary first-order structures (the setting of the original stage comparison theorem). But if there are solutions for particular cases, I'm interested in that too.  
> **username_2**: Okay. Also, can you perhaps edit the question to be more precise about the definition of the operator $\varphi(X,R)$ ($X$ unary, $R$ binary in place of $\prec$)? It's still unclear to me how precisely you are seeing this as a monotone operator.  
> **username_0**: Done (at last).  

---

## 0 answers

