Logic – Proof of (?x P(x)) ? A ? ?x (P(x) ? A)

logicproof-verificationquantifiers

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

Best Answer

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.

Related Question