6
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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? $\endgroup$ – François G. Dorais Aug 6 '17 at 11:27
  • $\begingroup$ 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))$$ $\endgroup$ – George Cherevichenko Aug 6 '17 at 11:50
  • $\begingroup$ Yes, you are right mediafire.com/file/2u66ou5kg65rlp3/intuitionism.pdf $\endgroup$ – George Cherevichenko Aug 6 '17 at 12:11
  • $\begingroup$ (The results I send to FOM) $\endgroup$ – George Cherevichenko Aug 6 '17 at 12:12
6
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ Thank you, Francois, but I proved these results in 1991. Once I send it to FOM. There was a long silence, two my next letters had been rejected without explanations. Once I send it (denoted as "folklore" and with more difficult results) to arxiv.org, the article had been rejected without explanations. It is interesting to me, is it a secret knowledge? $\endgroup$ – George Cherevichenko Aug 6 '17 at 11:15
  • 1
    $\begingroup$ It's not secret knowledge, there must be a problem with how you communicate. For instance, your question is written in a slighthly odd way. I think part of it has to do with the English language, and part of it is cultural. Let me put it this way: if you are a Russian talking to Americans, you should always be so polite that your Russian friends would think that you are making fun of the Americans. And never ever be direct. Do not say "you are wrong because of X", say "maybe I am mistaken, but isn't X a problem?" Also, hinting at conspiracy make you look crazy. $\endgroup$ – Andrej Bauer Aug 6 '17 at 21:17
  • $\begingroup$ Andrej, if you give me links, I'll be grateful. My grandfather was Slovenian, Slovenian are direct people. $\endgroup$ – George Cherevichenko Aug 6 '17 at 21:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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