<p><span class="math-container">$\let\eq\leftrightarrow$</span>Based on the comments, I’m interpreting the argument of <span class="math-container">$\psi$</span> as a “nullary predicate”. You can define <span class="math-container">$I$</span> by the formulas
<span class="math-container">$$\begin{align*}
I(n)&amp;\iff\exists W\,((0\in W\eq\phi)\land\forall i&lt;n\,(i+1\in W\eq\psi(i\in W))\land n\in W)\\
&amp;\iff\forall W\,((0\in W\eq\phi)\land\forall i&lt;n\,(i+1\in W\eq\psi(i\in W))\to n\in W).
\end{align*}$$</span>
The equivalence of the two definitions can be proved by induction on <span class="math-container">$n$</span>, and then it is easy to show that it satisfies the desired recursion.</p>

CC BY-SA 4.0
2022-09-24T20:45:01.103Z
This seems to work, but I'm still having a bit of trouble proving the equivalence. Any hints?
cody
CC BY-SA 4.0
2022-09-25T08:23:56.893Z
Which part are you having trouble with? It’s probably most intuitive to prove each implication separately. One direction amounts to $\let\eq\leftrightarrow(0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W))\land(0\in W'\eq\phi)\land\forall i<n\,(i+1\in W'\eq\psi(i\in W'))\to(n\in W\eq n\in W')$. You prove this by induction on $n$. The other direction amounts to $\exists W\,((0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W)))$. You also prove this by induction on $n$; in the induction step, use comprehension to change the membership of $n+1$ in $W$.
Emil Jeřábek
CC BY-SA 4.0
2022-09-25T21:21:30.473Z
BTW, this solution is absolutely miraculous! Is this a standard trick from somewhere?
cody
CC BY-SA 4.0
2022-09-26T06:14:10.850Z
Well, how else would you prove construction by recursion? Isn’t this just the standard textbook proof such as in e.g. https://proofwiki.org/wiki/Principle_of_Recursive_Definition/Strong_Version ?
Emil Jeřábek
CC BY-SA 4.0
2022-09-26T20:06:03.977Z
I feel like you really need to use the "$\Delta^1_0$-trick" in the 2nd order case, but not in HOL (or ZF), as mentioned in the question.
cody
CC BY-SA 4.0
2022-09-26T20:52:10.347Z
it's the "other direction" direction. What is the witness to the $\exists W$? is it the body of the second definition?
cody
CC BY-SA 4.0
2022-09-27T06:22:27.250Z
Sorry, what do you mean by the “$\Delta^1_0$-trick”?
Emil Jeřábek
CC BY-SA 4.0
2022-09-27T06:25:59.803Z
Given a $W$ that satisfies $\let\eq\leftrightarrow(0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W))$, you define $W'$ that satisfies $(0\in W'\eq\phi)\land\forall i<n+1\,(i+1\in W'\eq\psi(i\in W'))$ by comprehension: $W'=\{x:(x\ne n+1\land x\in W)\lor(x=n+1\land\psi(n\in W))\}$. Note that HA proves the decidability of equality of integers.
Emil Jeřábek
CC BY-SA 4.0
2022-09-27T16:33:40.817Z
I'm feeling *very* stupid, but I still don't have it: where am I getting $W$ from? The IH? This means I have to prove $\forall W, ... \rightarrow n \in W$.
cody
CC BY-SA 4.0
2022-09-27T16:39:10.463Z
You said you were proving the “other direction”. That is, you are proving $\let\eq\leftrightarrow\exists W\,((0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W)))$ by induction on $n$. So yes, you get $W$ from the IH. $\forall W\dots$ does not enter it.
Emil Jeřábek
CC BY-SA 4.0
2022-09-27T18:08:55.040Z
Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/139489/discussion-between-cody-and-emil-jerabek).
cody
CC BY-SA 4.0
2022-09-28T03:00:31.037Z
Last comment: Thanks to Emil's extreme patience and explanations, I finally got it; here's a detailed Coq proof: https://gist.github.com/codyroux/dd6d9ea3be02bbd3dfb513787fc99514
cody
CC BY-SA 4.0
2022-09-28T05:30:41.283Z
Very well, I’m glad it worked.
Emil Jeřábek
CC BY-SA 4.0
2022-09-23T19:10:24.717Z
2022-09-23T19:10:24.717Z
Emil Jeřábek
<p>This is a purely logical question, but I think it's adjacent enough to CS that it's worth a shot here.</p>
<p>Take 2nd order Heyting Arithmetic, say Heyting Arithmetic with an extra sort of (unary) predicates, a membership relation <span class="math-container">$\in$</span>, and the full comprehension axiom
<span class="math-container">$$ \exists X\forall n\quad n\in X \Leftrightarrow \phi(n) $$</span></p>
<p>for <em>every</em> formula not containing <span class="math-container">$X$</span>.</p>
<p>Suppose I have a formula <span class="math-container">$\psi(X)$</span> with some free predicate variable <span class="math-container">$X$</span>, and some base formula <span class="math-container">$\phi$</span>. I want to define the following predicate <span class="math-container">$I$</span>:</p>
<p><span class="math-container">$$I(0) \equiv \phi$$</span>
<span class="math-container">$$ I(n+1)\equiv \psi(I(n))$$</span></p>
<p>A <a href="https://mathoverflow.net/q/430785/36103">related question</a> convinced me that it is possible to do this in <em>classical</em> 2nd order arithmetic, but there it is possible to apply a trick, namely have <span class="math-container">$I(n+1)$</span> depend on a number <span class="math-container">$k$</span> such that <span class="math-container">$k = 1$</span> iff <span class="math-container">$I(n)$</span> holds. Such a number does not (necessarily) exist in the intuitionistic setting.</p>
<p>As a side note, in <em>3rd</em> order logic, one could simply define the graph of <span class="math-container">$I$</span>, no classical logic needed.</p>
<p>So my question is:</p>
<blockquote>
<p>Is it always possible to define the predicate <span class="math-container">$I$</span> in the intuitionistic setting?</p>
</blockquote>

CC BY-SA 4.0
2022-09-23T16:52:58.707Z
I’m confused by the syntax. When you are using formulas such as $B$ or $F$ in place of predicates (i.e., sets), do you mean that the formulas have a free number variable $n$ and you are equating $B$ with the predicate $\{n:B(n)\}$? If not, what does $F(I(n))$ mean?
Emil Jeřábek
CC BY-SA 4.0
2022-09-23T17:06:02.253Z
But if my reading is correct, can’t you just do the usual proof of construction by recursion? Fix a pairing function $(n,m)$, define $X^{[n]}=\{m:(n,m)\in X\}$, and let a partial $I$-predicate of length $n$ be an $X$ such that $X^{[0]}\equiv B$ and $X^{[i+1]}\equiv F(X^{[i]})$ for all $i<n$. Then you prove easily that two partial $I$-predicates agree on their common domain, that a given partial $I$-predicate of length $n$ can be extended to length $n+1$, thus partial $I$-predicates exist for all $n$ by induction. Then define $I(n)$ as $X^{[n]}$ for any partial $I$-predicate $X$ of length $>n$.
Emil Jeřábek
CC BY-SA 4.0
2022-09-23T17:21:43.477Z
My syntax is confusing; `B` and `F` are *formulas* and not predicates, for which I should have used greek letters. Let me fix this.
cody
CC BY-SA 4.0
2022-09-23T17:26:06.050Z
This does not help. You say $\psi(X)$ is a formula with a free predicate variable $X$, but then you write $\psi(I(n))$, where $I(n)$ has also have been defined as equivalent to a formula rather than a predicate. So what does $\psi(I(n))$ mean?
Emil Jeřábek
CC BY-SA 4.0
2022-09-23T17:54:25.817Z
Also a fair point! I mean $X$ to actually be a nullary predicate, or, say $m\in X$ where $m$ is some irrelevant variable, in which case $\psi(I(n))$ means "replace $m\in X$ by $I(n)$".
cody
CC BY-SA 4.0
2022-09-23T19:04:12.827Z
All right. Well then you can use what I wrote, except simpler (no need for a pairing function).
Emil Jeřábek
<lo.logic><constructive-mathematics>
Can you define recursive predicates in 2nd order intuitionistic logic?
cody
# Can you define recursive predicates in 2nd order intuitionistic logic?

(Asked by: username_0 on 2022-09-23)

This is a purely logical question, but I think it's adjacent enough to CS that it's worth a shot here.

Take 2nd order Heyting Arithmetic, say Heyting Arithmetic with an extra sort of (unary) predicates, a membership relation $\in$, and the full comprehension axiom
$$ \exists X\forall n\quad n\in X \Leftrightarrow \phi(n) $$

for *every* formula not containing $X$.

Suppose I have a formula $\psi(X)$ with some free predicate variable $X$, and some base formula $\phi$. I want to define the following predicate $I$:

$$I(0) \equiv \phi$$
$$ I(n+1)\equiv \psi(I(n))$$

A [related question](https://mathoverflow.net/q/430785/36103) convinced me that it is possible to do this in *classical* 2nd order arithmetic, but there it is possible to apply a trick, namely have $I(n+1)$ depend on a number $k$ such that $k = 1$ iff $I(n)$ holds. Such a number does not (necessarily) exist in the intuitionistic setting.

As a side note, in *3rd* order logic, one could simply define the graph of $I$, no classical logic needed.

So my question is:

> Is it always possible to define the predicate $I$ in the intuitionistic setting?

**Tags:** lo.logic, constructive-mathematics
> **Comments:**
> **username_1**: I’m confused by the syntax. When you are using formulas such as $B$ or $F$ in place of predicates (i.e., sets), do you mean that the formulas have a free number variable $n$ and you are equating $B$ with the predicate $\{n:B(n)\}$? If not, what does $F(I(n))$ mean?  
> **username_1**: But if my reading is correct, can’t you just do the usual proof of construction by recursion? Fix a pairing function $(n,m)$, define $X^{[n]}=\{m:(n,m)\in X\}$, and let a partial $I$-predicate of length $n$ be an $X$ such that $X^{[0]}\equiv B$ and $X^{[i+1]}\equiv F(X^{[i]})$ for all $i<n$. Then you prove easily that two partial $I$-predicates agree on their common domain, that a given partial $I$-predicate of length $n$ can be extended to length $n+1$, thus partial $I$-predicates exist for all $n$ by induction. Then define $I(n)$ as $X^{[n]}$ for any partial $I$-predicate $X$ of length $>n$.  
> **username_0**: My syntax is confusing; `B` and `F` are *formulas* and not predicates, for which I should have used greek letters. Let me fix this.  
> **username_1**: This does not help. You say $\psi(X)$ is a formula with a free predicate variable $X$, but then you write $\psi(I(n))$, where $I(n)$ has also have been defined as equivalent to a formula rather than a predicate. So what does $\psi(I(n))$ mean?  
> **username_0**: Also a fair point! I mean $X$ to actually be a nullary predicate, or, say $m\in X$ where $m$ is some irrelevant variable, in which case $\psi(I(n))$ means "replace $m\in X$ by $I(n)$".  
> **username_1**: All right. Well then you can use what I wrote, except simpler (no need for a pairing function).  

---

## 1 answers

### Answer by username_1 on 2022-09-23. Score: 4

$\let\eq\leftrightarrow$Based on the comments, I’m interpreting the argument of $\psi$ as a “nullary predicate”. You can define $I$ by the formulas
$$\begin{align\*}
I(n)&\iff\exists W\,((0\in W\eq\phi)\land\forall i
The equivalence of the two definitions can be proved by induction on $n$, and then it is easy to show that it satisfies the desired recursion.

> **Comments:**
> **username_0**: This seems to work, but I'm still having a bit of trouble proving the equivalence. Any hints?  
> **username_1**: Which part are you having trouble with? It’s probably most intuitive to prove each implication separately. One direction amounts to $\let\eq\leftrightarrow(0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W))\land(0\in W'\eq\phi)\land\forall i<n\,(i+1\in W'\eq\psi(i\in W'))\to(n\in W\eq n\in W')$. You prove this by induction on $n$. The other direction amounts to $\exists W\,((0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W)))$. You also prove this by induction on $n$; in the induction step, use comprehension to change the membership of $n+1$ in $W$.  
> **username_0**: BTW, this solution is absolutely miraculous! Is this a standard trick from somewhere?  
> **username_1**: Well, how else would you prove construction by recursion? Isn’t this just the standard textbook proof such as in e.g. https://proofwiki.org/wiki/Principle_of_Recursive_Definition/Strong_Version ?  
> **username_0**: I feel like you really need to use the "$\Delta^1_0$-trick" in the 2nd order case, but not in HOL (or ZF), as mentioned in the question.  
> **username_0**: it's the "other direction" direction. What is the witness to the $\exists W$? is it the body of the second definition?  
> **username_1**: Sorry, what do you mean by the “$\Delta^1_0$-trick”?  
> **username_1**: Given a $W$ that satisfies $\let\eq\leftrightarrow(0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W))$, you define $W'$ that satisfies $(0\in W'\eq\phi)\land\forall i<n+1\,(i+1\in W'\eq\psi(i\in W'))$ by comprehension: $W'=\{x:(x\ne n+1\land x\in W)\lor(x=n+1\land\psi(n\in W))\}$. Note that HA proves the decidability of equality of integers.  
> **username_0**: I'm feeling *very* stupid, but I still don't have it: where am I getting $W$ from? The IH? This means I have to prove $\forall W, ... \rightarrow n \in W$.  
> **username_1**: You said you were proving the “other direction”. That is, you are proving $\let\eq\leftrightarrow\exists W\,((0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W)))$ by induction on $n$. So yes, you get $W$ from the IH. $\forall W\dots$ does not enter it.  
> **username_0**: Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/139489/discussion-between-cody-and-emil-jerabek).  
> **username_0**: Last comment: Thanks to Emil's extreme patience and explanations, I finally got it; here's a detailed Coq proof: https://gist.github.com/codyroux/dd6d9ea3be02bbd3dfb513787fc99514  
> **username_1**: Very well, I’m glad it worked.  

---

