Proving a class of relations is closed under an operation

97 Views Asked by At

Given a class of functions $\mathcal{A}$ is closed under substitution and the operation $(\mu y)_{\leq z}$, where $$ (\mu y)_{\leq z}f(y, \vec x) = \begin{cases} \min\{y : y \leq z \land f(y, \vec x) = 0\}\\ 0 \mathrm{,\ if\ min\ doesn't\ exist} \end{cases} $$ along with a class of relations $\mathcal{A}_* = \{f(\vec x) = 0 : f \in A\}$, show that $\mathcal{A}_*$ is closed under $(\exists y)_{\leq{z}}$. (In this context, "true" is $0$ and "false" is $1$.)

I've tried coming up with solutions like (say $g \in \mathcal{A}_*$ and $g(y, \vec x) = (f(y, \vec x) = 0)$ for some $f \in \mathcal{A}$):

$$(\exists y)_{\leq z}g(y, \vec x) \equiv (\exists y)_{\leq z}(f(y, \vec x) = 0) \equiv \left( (\mu w)_{\leq z}(\mu y)_{\leq z}(f(y, \vec x)=w) \right) =0$$

But this returns the opposite of what I want (0 in place of 1 and vice versa), and I'm not confident everything I've done is legal (particularly the $= w$ bit). Is this the right sort of approach? A push in the right direction would be much appreciated.

1

There are 1 best solutions below

1
On BEST ANSWER

$$ (\exists y)_{\leq z}(f(y, \vec x) = 0) \ \ \Leftrightarrow\ \ \ f((\mu y)_{\leq z}f(y, \vec x), \vec x)=0. $$