5
$\begingroup$

I recently asked this question. In that question I presented a hand-waving proof as part of the question. There was some confusion as to the validity of my hand-waving proof. So I wanted to make it more precise. The difficulty that I had is that it's been 25 years since I've written formal logic proofs. I've forgotten some of the rules (Like how to handle introducing and eliminating quantifiers) and rule names. So as you'll see below I just invented names of rules in the proof below.

A few questions.

  1. Assuming I used standard rule names (rather than made up ones), is the proof correct. Or do a few steps need to be "tightened" up. What is a good reference to "standard" rule names typically used on this site.
  2. I never know how to typeset these sorts of proofs. Like in steps 3-5 of Case 2, I'd expect those to be indented to show that $c$ is only valid in the context of the existential. (Update: they are now indented using \quad) (I suppose this should be a separate question on meta or a LaTex site?)

A proof of $(\forall x P(x)) \to A) \Rightarrow \exists x (P(x) \to A)$

I'll prove by case analysis on $ \forall x P(x) $.

Case 1: $ \forall x P(x) $

$$\begin{align} & (\forall x P(x)) \to A && \text{Hypothesis} & \tag{1} \\ & \forall x P(x) && \text{Case Hypothesis} & \tag{2} \\ & A && \text{Implication 1, 2} & \tag{3} \\ & \neg P(c) \vee A && \text{Or Introduction} & \tag{4} \\ & P(c) \to A && \text{Definition of Implies, 4} & \tag{5}\\ & \exists x (P(x) \to A) && \text{Existential Intro, 5} & \tag{6}\\ \end{align} $$

Case 2: $ \neg \forall x P(x) $

$$\begin{align} & \neg \forall x P(x) && \text{Case Hypothesis} & \tag{1} \\ & \exists x \neg P(x) && \text{A Known Identity, 1} & \tag{2} \\ & \quad \neg P(c) && \text{Assumption, ref 2} & \tag{3} \\ & \quad \neg P(c) \vee A && \text{Or Introduction, 3} & \tag{4} \\ & \quad P(c) \to A && \text{Definition of Implies, 4} & \tag{5} \\ & \quad \exists x (P(x) \to A) && \text{Existential Intro, 5} & \tag{6} \\ & \exists x (P(x) \to A) && \text{Existential Elim, 2,6} & \tag{7} \\ \end{align} $$

UPDATE: A commenter pointed out that the statement is false in the case that the universe is empty, so let's assume a non-empty universe.

UPDATE: An answer addressed my funny introduction of $\neg P(c)$ in case 2 step 3. I tried to make things more precise by using indentation and referenced EE as demonstrated here: http://softoption.us/content/node/277

$\endgroup$
  • 5
    $\begingroup$ The statement is false. If the universe is empty, and $A$ is true, then $\forall x P(x)$ holds vacuously, and hence $(\forall x P(x)) \to A)$ holds. However since the universe is empty, $\exists x$ fails to hold, as does $\exists x (P(x) \to A)$. $\endgroup$ – vadim123 Dec 16 '15 at 2:54
  • $\begingroup$ Ok, understood. Thanks for that feedback. $\endgroup$ – Michael Welch Dec 16 '15 at 2:55
1
$\begingroup$

This depends on which rules you're allowed to use. If you're allowed to use those rules that you're using it seems OK - and all rules that's been used seem alowable too.

The comment of a non-empty universe is inherent in one or a few of the rules and since it's quite reasonable to require non-empty universe this fact doesn't ban these rules from being alowable.

Depending on how you view it's when using existential introduction (or perhaps when you introduce $c$ via or introduction). Either it's to conclude $\exists x \phi(x)$ from $\forall x \phi(x)$ that assumes non-empty or it's the assumption that $\phi(c)$ implies that $c$ refers to something existing.

Note that the second case might not need to rely on rules that imply non-empty universe since the case premise is false there. That's why you for example from the premise can conclude $\exists x\neg P(x)$

$\endgroup$
  • $\begingroup$ I'll mark yours as the correct answer as you said it looks OK. I did finally prove this using the tool mentioned in the referenced question and so that corroborates that I've done it correctly. The graphics proof is messier (need to prove the quantification identity I used) but follows the same structure. math.stackexchange.com/questions/1575982/… $\endgroup$ – Michael Welch Dec 17 '15 at 23:03
1
$\begingroup$

Addressing question 1 specifically:

I am not an expert in the subject but I took a couple of logic subjects at uni and never really saw a standard naming convention for the deduction rules in first order logic. You are likely to find different authors with different conventions. What is most important is you follow the rules correctly and you have in this case.

$\endgroup$
  • 1
    $\begingroup$ Cool. Thanks for the proof. I'm a little confused. Line 5 doesn't seem valid. Line 3 should say $(\forall x P(x)) \to A$. Therefore the instantiation doesn't seem valid. We know that "if P(x) is true for all x, then A is true". However it doesn't seem like P(c) implies A from that fact. In other words, the quantification is not over the whole statement. It is embedded inside the implication. $\endgroup$ – Michael Welch Dec 16 '15 at 3:30
  • $\begingroup$ You are right, that was a mistake in the argument. Have edited my answer accordingly. $\endgroup$ – Bernard W Dec 16 '15 at 3:59
0
$\begingroup$

I'm a little bit puzzled by your proof in the case 2, i.e. under the assumption $\lnot \forall x \, P(x)$. As your proof should be valid classically but not intuitionistically (since it uses the law of excluded middle), you cannot infer from $\exists x \, \lnot P(x)$ that $P(c)$ (your step 3), the best you can classically do is apply the Herbrand's theorem. Indeed, in natural deduction (see Prawitz's Natural Deduction) the elimination rule for $\exists$ is NOT of the form

\begin{align*} \frac{\exists x A}{A[c/x]} \end{align*}

So, I think that you have to reformulate the case 2 as follows. Assume $\lnot \forall x \, P(x)$; this means that $\exists x \, \lnot P(x)$. Let us suppose that $x$ is such that $\lnot P(x)$: then $P(x) \to A$ since any statement can be proven from a contradiction (ex falso quodlibet), in particular $A$. Hence, for any $x$ such that $\lnot P(x)$ we have proved that $\exists x \, (P(x) \to A)$. Therefore, under the assumption $\lnot \forall x \, P(x)$, we have proved that $\exists x \, (P(x) \to A)$.

I formalized your whole proof of $\forall x \, P(x) \to A \vdash \exists x \, (P(x) \to A)$ (following my argument for the case 2) in Prawitz's natural deduction (I suppose you are referring to natural deduction when you say "how to handle introducing and eliminating quantifiers"):

enter image description here

where $\pi$ is a derivation in classical natural deduction (but it is not intuitionsitically valid) of the instance $\forall x \, P(x) \lor \lnot \forall x \, P(x)$ of the law of excluded middle, and $\pi_0$ is a derivation in classical natural deduction (but it is not intuitionsitically valid) of $\exists x \, \lnot P(x)$ under the assumption $\lnot \forall x \, P(x)$. I can detail $\pi$ and $\pi_0$ but I think it is out of scope of this discussion.

$\endgroup$
  • $\begingroup$ Thanks. I don't see how your second case works. If you are going to assume $P(y)$ then when you prove your contradiction than at best you've proved that $P(y) \to \bot$. I don't see how you can conclude $\bot$. $\endgroup$ – Michael Welch Dec 16 '15 at 13:29
  • $\begingroup$ Regarding my step 3: I can certainly accept I may be inventing an improper rule at that step. However, what I'm doing seems correct and it certainly seems like there must be a rule that allows me to do something along those lines. I'll look at your reference. If I know from step 2 that there exists an element $x$ for which $P(x)$ is false, then it seems like I should be able to give it a name and state it simply as $\neg P(c)$. $\endgroup$ – Michael Welch Dec 16 '15 at 13:33
  • $\begingroup$ I just googled for $\exists$ elimination rule and found this: softoption.us/content/node/277 This is along the lines of what I was thinking when I said in my proof that lines 3- 5 should be indented. Indeed lines 3 -6 should be indented and when I reach 6 I no longer have $c$ in the "target" so I can un-indent and conclude in line 7 what was shown in line 6. $\endgroup$ – Michael Welch Dec 16 '15 at 13:39
  • $\begingroup$ I've updated my proof to use EE correctly now, I think.(Based on the link in my comment above from softoption.us) $\endgroup$ – Michael Welch Dec 16 '15 at 17:36
  • $\begingroup$ @MauroALLEGRANZA: You are absolutely right, I have to fix it as soon as possible. Thank you very much. $\endgroup$ – Taroccoesbrocco Dec 16 '15 at 18:00

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.