# Can you define recursive predicates in 2nd order intuitionistic logic?

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 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?

• 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? Sep 23, 2022 at 16:52
• 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$. Sep 23, 2022 at 17:06
• 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
Sep 23, 2022 at 17:21
• 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? Sep 23, 2022 at 17:26
• All right. Well then you can use what I wrote, except simpler (no need for a pairing function). Sep 23, 2022 at 19:04

$$\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.
• 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$. Sep 25, 2022 at 8:23
• 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. Sep 27, 2022 at 6:25