4
$\begingroup$

I've been trying it in Joachim Breitner's fun little Incredible Proof Machine applet (https://incredible.pm/), mostly just because it's easy to visualize that way, but I don't think that's essential. The applet does basicall constructive logic (with not $\lnot P$ represented as $P \Rightarrow \bot$) and an excluded middle axiom if you want to do classical logic.

I can prove the constructively valid direction $$ \cfrac{\cfrac{\cfrac{\exists x. P(x)} {P(k)} \cfrac{[\forall x. \lnot P(x)]} {\lnot P(k)}} {\bot}} {\lnot \forall x. \lnot P(x)}$$ but I can't do it the other way around. I know I need the LEM axiom since it's only classically valid, but I'm not sure where to put it or what to instantiate it with.

$\endgroup$
4
  • $\begingroup$ Note: You do not need the LEM axiom, since Double Negation Elimination is equally non-constructive. @Zyzzyva $\endgroup$ Oct 25, 2020 at 0:38
  • $\begingroup$ @GrahamKemp Yes, that's entirely fair, but the one non-constructive rule that the applet provides is LEM, and you have to derive all the other classical-but-not-constructive theorems from that. $\endgroup$
    – Zyzzyva
    Oct 25, 2020 at 1:00
  • $\begingroup$ Is there a user manual for this Incredible Proof Machine? $\endgroup$
    – Bram28
    Oct 25, 2020 at 17:47
  • $\begingroup$ Not that I know of; just an info panel in the upper right and the actual source code. $\endgroup$
    – Zyzzyva
    Oct 25, 2020 at 22:36

1 Answer 1

4
$\begingroup$

$\def\fitch#1#2{~~~~\begin{array}{|l} #1\\\hline #2\end{array}}$ Note: Well, you do not need the LEM axiom, @Zyzzyva, since Double Negation Elimination is equally non-constructive. Though you may use it if you so desire. Every LEM proof has an equivalent RAA proof.

The key point is that if you assume that there is no such entity that satisfies $P$, then any arbitrary entity must satisfy $\neg P~$ (IE: $\neg\exists x~P(x)\vdash \forall x~\neg P(x)$) . This would contradict a prior assumption for the desired conditional proof.

$$\begin{split}P(k)&\vdash \exists x~P(x)&\text{existential introduction}\\\neg\exists x~P(x),P(k)&\vdash\bot&\text{negation elimination}\\\neg\exists x~P(x)&\vdash\neg P(k)&\text{negation introduction}&(4)\\\neg\exists x~P(x)&\vdash\forall x~P(x)&\text{universal introduction}&(3)\\\neg\forall x~\neg P(x),\neg\exists x~P(x)&\vdash\bot&\text{negation elimination}\\\neg\forall x~\neg P(x)&\vdash\neg\neg\exists x~P(x)&\text{negation introduction}&(2)\\\neg\forall x~\neg P(x)&\vdash\exists x~P(x)&\text{double negation elimination}\\&\vdash \neg\forall x~\neg P(x)\to\exists x~P(x)\quad&\text{conditional introduction}\quad&(1)\end{split}$$

As you see, we raise and discharge four assumptions: $\neg\forall x~\neg P(x), \neg\exists x~P(x),$ arbitrary variable $k$, and $P(k)$. (Although some systems do not explicitly describe a local variable as an "assumption", its context is raised and discharged.)


The LEM proof is easily built from this:

$$\begin{split}&\vdash(\exists x~P(x))\vee(\neg\exists x~P(x))&\text{law of excluded middle}\\[1ex]\exists x~P(x)&\vdash\exists x~P(x)&\text{reiteration}\\[1ex]P(k)&\vdash \exists x~P(x)&\text{existential introduction}\\\neg\exists x~P(x),P(k)&\vdash\bot&\text{negation elimination}\\\neg\exists x~P(x)&\vdash\neg P(k)&\text{negation introduction}&(5)\\\neg\exists x~P(x)&\vdash\forall x~P(x)&\text{universal introduction}&(4)\\\neg\forall x~\neg P(x),\neg\exists x~P(x)&\vdash\bot&\text{negation elimination}\\\neg\forall x~\neg P(x),\neg\exists x~P(x)&\vdash\exists x~P(x)&\text{explosion}\\\hline\neg\forall x~\neg P(x)&\vdash\exists x~P(x)&\text{disjunction elimination}&(2,3)\\&\vdash \neg\forall x~\neg P(x)\to\exists x~P(x)\quad&\text{conditional introduction}\quad&(1)\end{split}$$


That just leaves translating it into your preferred format.

$$\phantom{\tiny{\dfrac{\dfrac{\dfrac{\dfrac{\lower{1.5ex}{[\neg\forall x~P(x)]^1}~\dfrac{{\dfrac{\dfrac{\lower{1.5ex}{[\neg\exists x~P(x)]^2}~\dfrac{[P(k)]^4}{\exists x~P(x)}{\tiny\exists\mathsf I}}{\bot}{\tiny\neg\mathsf E}}{\neg P(k)}{\tiny\neg\mathsf I^4}}}{\forall x~\neg P(x)}{{\tiny\forall\mathsf I}^{\small\require{cancel}\cancel k}}}{\bot}{\tiny\neg\mathsf E}}{\neg\neg\exists x~P(x)}{\tiny\neg\mathsf I^2}}{\exists x~P(x)}{\tiny\neg\neg\mathsf E}}{\neg\forall x~\neg P(x)\to\exists x~P(x)}{\tiny\to\mathsf I^1}}\tiny{\dfrac{\dfrac{\dfrac{}{\left(\exists x~P(x)\right)\vee\left(\neg\exists x~P(x)\right)}{\tiny\textsf{LEM}}~\dfrac{[\exists x~P(x)]^2}{\exists x~P(x)}{\tiny\mathsf{R}}~\dfrac{\dfrac{\lower{1.5ex}{[\neg\forall x~P(x)]^1}~\dfrac{{\dfrac{\dfrac{\lower{1.5ex}{[\neg\exists x~P(x)]^3}~\dfrac{[P(k)]^5}{\exists x~P(x)}{\tiny\exists\mathsf I}}{\bot}{\tiny\neg\mathsf E}}{\neg P(k)}{\tiny\neg\mathsf I^5}}}{\forall x~\neg P(x)}{{\tiny\forall\mathsf I}^{\small\require{cancel}\cancel k}}}{\bot}{\tiny\neg\mathsf E}}{\exists x~P(x)}{\tiny\mathsf X}}{\exists x~P(x)}{\tiny\vee\mathsf E^{2,3}}}{\neg\forall x~\neg P(x)\to\exists x~P(x)}{\tiny\to\mathsf I^1}}}$$

$\endgroup$
2
  • $\begingroup$ Thanks very much! $\endgroup$
    – Zyzzyva
    Oct 25, 2020 at 2:52
  • $\begingroup$ +1. @Graham Kemp, could you explain in which way are you deriving each step ? How are you adding assumptions to the left of $\vdash$ ? Where can I learn more about this system ? $\endgroup$
    – F. Zer
    Oct 28, 2020 at 0:55

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.