# Rice's theorem in type theory

From the formula $$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$ we can get the scheme $$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\neg\phi(x)$$ From the scheme $$\forall x\colon A\,\exists y\colon A\,\phi(x,y)\Rightarrow\exists x\colon A\,\phi(x,x)$$ we can get $$\forall x\colon A\,(\phi(x)\vee\psi(x))\Rightarrow\neg\neg(\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\psi(x))$$ Where can I find these results? Give me a link, please.

P.S. Sorry, the second scheme must be $$\forall x\colon A\,(\neg\phi(x)\vee\neg\psi(x))\Rightarrow\neg\neg(\forall x\colon A\,\neg\phi(x)\vee\forall x\colon A\,\neg\psi(x))$$ The results are not quite difficult, but I never saw it in articles or books.

• Are you sure your second scheme is right? Proceeding in my answer below, we get $\forall x, y : A\,(\phi(x) \lor \psi(y))$ but that doesn't imply your desired conclusion in intuitionistic logic. Perhaps there are missing assumptions on $\phi$ and $\psi$? Should they be stable formulas? – François G. Dorais Aug 6 '17 at 11:27
• May be, I don't remember right now. We can get $$\forall x\colon A\,(\phi(x)\vee\psi(x))\Rightarrow\neg(\exists x\colon A\,\neg\phi(x)\wedge\exists x\colon A\neg\psi(x))$$ – George Cherevichenko Aug 6 '17 at 11:50
• Yes, you are right mediafire.com/file/2u66ou5kg65rlp3/intuitionism.pdf – George Cherevichenko Aug 6 '17 at 12:11
• (The results I send to FOM) – George Cherevichenko Aug 6 '17 at 12:12

I'll prove the first scheme; you can find a link by using the cite button below this answer.
First, we show that $$\forall x,y : A\,(\phi(x) \lor \lnot\phi(y))\tag{*}\label{eq}.$$ To see this, given $x,y : A$, define the function $$f_{x,y}(z) = \begin{cases} x & \text{if \phi(z),} \\ y &\text{if \lnot\phi(z).} \end{cases}$$ By hypothesis, $f_{x,y}$ has must have a fixed point. Since $$\forall z: A\,(f_{x,y}(z) = x \lor f_{x,y}(z) = y)$$ that fixed point must either be $x$ or $y$. Thus $$\forall x, y: A\,(f_{x,y}(x) = x \lor f_{x,y}(y) = y).$$ If $f_{x,y}(x) = x$ then $\phi(x)$ and if $f_{x,y}(y) = y$ then $\lnot\phi(y)$, so we conclude that \eqref{eq} is indeed true.
This is almost what we need. For the final stretch, first note that $A$ is inhabited since the identity function must have a fixed point. So fix $z:A$. We know that $\phi(z) \lor \lnot\phi(z)$. If $\phi(z)$ then $\phi(x) \lor \lnot\phi(z)$ is equivalent to $\phi(x)$ for any $x:A$, and so the instance of \eqref{eq} with $y = z$ gives $\forall x: A\,\phi(x)$. If $\lnot\phi(z)$ then $\phi(z) \lor \lnot\phi(y)$ is equivalent to $\lnot\phi(y)$ for any $y:A$, and so the instance of \eqref{eq} with $x = z$ gives $\forall y:A\,\lnot\phi(y).$ Thus, we conclude that $$\forall x:A\,\phi(x) \lor \forall y:A\,\lnot\phi(y),$$ which is an alphabetic variant of your desired conclusion.