4

I have been tasked to prove a slightly different version of the Drinker's paradox:

$\vdash_{NI} \neg\neg\exists x\forall y[P(y) \to P(x)]$

Where ${NI}$ stands for natural deduction in intuitionistic logic. My professor dubbed this the detective's paradox: "There is someone, who, if someone did murder, is the murderer"

I know that I should be looking for a statement $\varphi$ such that $$\varphi\to\exists x\forall y[P(y) \to P(x)] \land \neg\varphi\to\exists x\forall y[P(y) \to P(x)]$$

If I have this, then I may conclude \begin{align*}\varphi \lor \neg\varphi &\to \exists x\forall y[P(y) \to P(x)]\\ \neg\neg(\varphi \lor \neg\varphi) &\to \neg\neg\exists x\forall y[P(y) \to P(x)]\\ &\neg\neg\exists x\forall y[P(y) \to P(x)]\end{align*}

But I am having struggles looking for this $\varphi$. Currently I have tried $\exists x [P(x)], \forall x [P(x)]$ and many statements which use the previous two + various connectives. I am asking for a hint in the right direction so I know where to search for such $\varphi$ (or give another method for solving this in an easier way).

Edit: From the comments by Lereau and DanielIV I have tried the following:

  1. Assume $\forall x [\neg P(x)]$
  2. Assume $P(y)$
  3. From 1, conclude $\neg P(y)$
  4. From 2 and 3, conclude $\bot$
  5. From ex falso quodlibet, conclude $P(x)$
  6. $\to$-introduction, conclude $P(y) \to P(x)$
  7. $\forall$-introduction, conclude $\forall y[P(y) \to P(x)]$
  8. $\exists$-introduction, conclude $\exists x\forall y[P(y) \to P(x)]$
  9. $\to$-introduction, conclude $\forall x [\neg P(x)]\to\exists x\forall y[P(y) \to P(x)]$

This is the closest I can get to a proof. Nevertheless, do I think this is invalid because the $\forall$-introduction is, in my opinion, not allowed since an assumption is made about $y$, namely $\neg P(y)$. Thus how can I correct this proof?

Tungsten
  • 130
  • Your first guess $\exists x , P(x)$ still looks promising to me. – Léreau Jan 06 '22 at 14:53
  • The reason I dropped this idea is that I fail to prove $\neg\exists x P(x) \to\exists x\forall y[P(y)\to P(x)]$. Do you have hints on how to do this? – Tungsten Jan 06 '22 at 15:34
  • 1
    Start by assuming $\lnot \exists x . Px$ and assuming $Py$. – DanielV Jan 06 '22 at 15:54
  • 1
    @Tungsten Maybe this helps as a hint: $\neg \exists x , P (x)$ is intuitionistically equivalent to $\forall x , \neg P(x)$. – Léreau Jan 06 '22 at 16:07
  • I have edited the question in the hope that your hints have been incorporated in my attempt correctly. – Tungsten Jan 06 '22 at 18:40
  • 1
    @Tungsten Your proof is correct. The problem you mention fortunately isn't one. What you are doing in the lines 2 to 6 is to establish $\forall x , \neg P(x) \vdash P(y) \to P(x)$. On this, you can now safely use $\forall$-introduction, as there is indeed no further assumption about $y$ in the context on the left of $\vdash$. – Léreau Jan 07 '22 at 12:44
  • @Lereau I see I see. I tried this proof in a proof assistant and it didn't agree with me. That is why I was in doubt but I thank you very much – Tungsten Jan 07 '22 at 14:21
  • 1
    @Tungsten Based on my own attempt in Coq, I will make the guess that you ran into the same subtlety I encountered, which comes down to the logics that are being implemented. If you are quantifying over a type, you need to make sure that it is inhabited. Otherwise you cannot do step 5 in the proof you presented. If you are using an assistant for first-order logic, then the same fix can be achieved by changing the formula to $\forall a , \neg \neg \exists x \forall y , P(y) \to P(x)$. (Similar to here) – Léreau Jan 07 '22 at 14:49
  • 1
    @Lereau That does clarify my problems! Thank you for this example. – Tungsten Jan 07 '22 at 16:43

0 Answers0