5
$\begingroup$

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?

$\endgroup$
6
  • $\begingroup$ 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? $\endgroup$ Sep 23, 2022 at 16:52
  • $\begingroup$ 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$. $\endgroup$ Sep 23, 2022 at 17:06
  • $\begingroup$ My syntax is confusing; B and F are formulas and not predicates, for which I should have used greek letters. Let me fix this. $\endgroup$
    – cody
    Sep 23, 2022 at 17:21
  • $\begingroup$ 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? $\endgroup$ Sep 23, 2022 at 17:26
  • 1
    $\begingroup$ All right. Well then you can use what I wrote, except simpler (no need for a pairing function). $\endgroup$ Sep 23, 2022 at 19:04

1 Answer 1

4
$\begingroup$

$\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<n\,(i+1\in W\eq\psi(i\in W))\land n\in W)\\ &\iff\forall W\,((0\in W\eq\phi)\land\forall i<n\,(i+1\in W\eq\psi(i\in W))\to n\in W). \end{align*}$$ 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.

$\endgroup$
13
  • $\begingroup$ This seems to work, but I'm still having a bit of trouble proving the equivalence. Any hints? $\endgroup$
    – cody
    Sep 24, 2022 at 20:45
  • $\begingroup$ 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$. $\endgroup$ Sep 25, 2022 at 8:23
  • $\begingroup$ BTW, this solution is absolutely miraculous! Is this a standard trick from somewhere? $\endgroup$
    – cody
    Sep 25, 2022 at 21:21
  • 1
    $\begingroup$ 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. $\endgroup$ Sep 27, 2022 at 6:25
  • 1
    $\begingroup$ Very well, I’m glad it worked. $\endgroup$ Sep 28, 2022 at 5:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.