Understanding of "Somewhat Surprising" First Order Logic Expression in E.J.Lemmon, Beginning Logic

Question

In "Beginning Logic" by E.J.Lemmon, Page 126, Theorem 118 (1994 Reprint) a "somewhat surprising" inter-derivability result in Predicate Calculus is proved: $$( (\exists x\, Hx) \implies P) \dashv \vdash \forall x\, (Hx \implies P) $$

where Hx is a one place predicate and P is a zero place predicate.

My question relates to the left to right meaning of the $( (\exists x\, Hx) \implies P) \vdash \forall x\, (Hx \implies P) $ derivation (presumably that is the 'somewhat surprising' direction), in the context of a truth table meaning of "$\implies$".

If the $((\exists x\, Hx) \implies P)$ expression is to mean (when it is true) "if there is an element $t$ in the domain with $Hx[x\backslash t]$ true" then $P$ can only be true - because $P$ can't be false due to the truth table meaning of "$\implies$". This expression does not appear to talk about any specific element $f$ in the domain where $Hx[x\backslash f]$ is false.

However if in addition to $t$ there is an element $f$ in the domain where the expression $Hx[x\backslash f]$ is false then $\forall x (Hx \implies P)$ at this location gives, using $(Hx \implies P)[x\backslash f]$, the truth interpretation "$\bot \implies P$". This would mean at the location $f$, $P$ can be false whilst still giving $(Hx \implies P)[x\backslash f]$ true. So the $(Hx \implies P)$ expression (when true) could give two possible truth values for $P$ - at $f$ it could give $P$ is false and applying the same method at $t$, it gives $P$ is true. This would suggest a contradiction occurs and also that the two sides of the derivation don't actually say the same thing.

Any help to correct my understanding of how to apply the truth interpretation of "$\implies$" in the above will be greatly appreciated.

Answer 1

The statement is about inter-deriability, $\dashv \vdash$. This is a purely syntactic notion. You can convince yourself of the truth of this statement by a corresponding pair of derivations:

1. $\exists x Hx \to P \vdash \forall x (Hx \to P)$:
   

2. $\forall x (Hx \to P) \vdash \exists x Hx \to P$:

3. derivation $\mathcal{D}$ for the transitions $\neg (Ha \to P) \vdash Ha \land \neg P$ and $\neg(\exists x \to P) \vdash \exists x Hx \land \neg P$:

So $\exists x Hx \to P \vdash \forall x (Hx \to P)$ and $\forall x (Hx \to P) \vdash \exists x Hx \to P$, therefore $\exists x Hx \to P \vdash \vdash \forall x (Hx \to P)$. This proves the theorem you stated, namely $\vdash$.

Since you seem to be also/more interested in a semantic argument, namely $\vDash$, and due to soundness and completeness, we luckily also have $\exists x Hx \to P \vDash \forall x (Hx \to P)$, let's explain what happens in the formal proof; this will also explain what's going on in the semantics:

We prove both directions by contradition, i.e. we first assume that the derivation/entailment doesn't hold, which means that the premise is true while the conclusion is not, and derive a contradiction, from which we can deduce that the derivability/entailment does hold.

1. $\exists x Hx \to P \vdash, \vDash \forall x (Hx \to P)$:
   Assume $\exists x Hx \to P$ but $\neg \forall x (Hx \to P)$ (l. 1-2). This means that there is some object, say $a$, such that $\neg (Ha \to P)$ (l. 2-6), and if the implication is false, then it must be the case that $Ha$ but $\neg P$ (l. 7-10). Since we found an object $a$ such that $Ha$, we know that there exists an $x$ s.t. $Hx$, i.e. $\exists x Hx$ (l. 11). But modus ponens with the premise $\exists Hx \to P$ tells us that then $P$ must hold, which contradicts the statement $\neg P$ (l. 12-13) which we derived from the assumption that $Hx \to P$ does not hold of $a$. Since assuming $\neg \forall x (Hx \to P)$ leads to a contradiction, the negation of the statement must have been false (l. 14), and it follows that $\exists x Hx \to P \vDash \forall x(Hx \to P)$ (l. 15), which completes the proof of one direction.
2. $\forall x (Hx \to P) \vdash, \vDash \exists x Hx \to P$:
   Again, we prove by contradiction and assume that $\forall x(Hx \to P)$, but $\neg (\exists x \to P)$ (l. 1-2). Again, this is equivalent to stating that $\exists x$ and $\neg P$ holds (l. 2-6), so there is an $x$ to which $H$ applies but $P$ is not true. Let's call this element $a$ (l. 7). From the assumption $\forall x(Hx \to P)$ it follows that this must also hold of our $a$, so by modus ponens we get $P$ (l. 8-9). But this again contradicts the statement $\neg P$ which we derived from our assumption $\neg (\exists x \to P)$ (l. 10). So this assumption must have been false (l. 11), and we have $\exists x Hx \to P$ (l. 12) derived from $\forall x (Hx \to P)$, which proves the other direction.
3. is just the missing piece in the derivations 1. and 2. which I sourced out so the proofs wouldn't get too huge.