All Questions
1 question
6
votes
1
answer
839
views
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\,\...
