# Formal Logic Proof

#### fumbles

##### New member
This question is really getting on my nerves. It's 6i) from here:

Right off the bat, it looks like they've thrown me a curveball. The fact that $$v$$ does not occur free in $$\psi$$ means that the Existential Hypothesis rule is going to need some care when applied.

I've come up with two possible proofs:

..each in a different colour.

To me, the top proof looks more correct than the bottom. It's just the Existential Hypothesis rule that's throwing me.

For the first proof, I think line 10 is wrong. I need the existential hypothesis rule to depend on all the assumptions where v is free. This happens in lines 1,2 and MAYBE 3. If v is a free variable in line 3, then i'm sorted and everything is right. If it isn't, then I have a problem on my hands.

There's a similar problem for the second proof too.

Useful things:

The far left number show the assumptions a line depends on. The bracketed number is the line number and the far right column is the rules column.

As s = Assumption
Taut = Tautology
CP = Conditional Proposition
EH= Existential Hypothesis

#### Evgeny.Makarov

##### Well-known member
MHB Math Scholar
I think both proofs are fine. In the first proof, you just do some propositional reasoning, namely, deriving $\neg\psi$ from $\phi$ and $\neg\phi\leftrightarrow\psi$. In the second proof, this subderivation is contracted into one step because you can do arbitrary propositional reasoning in one step.

The restriction on EH, which derives some $\chi$ from $\exists v\,\theta$ and a subderivation of $\chi$ from $\theta$, is that $v$ can occur freely only in $\theta$: it cannot occur freely in $\chi$ nor in other open assumptions of $\chi$ except $\theta$. In your case, $\neg\psi$ has open assumptions $\forall x\,\phi$ and $\neg\phi\leftrightarrow\psi$. The variable $v$ occurs freely in $\neg\phi\leftrightarrow\psi$ but not in $\forall x\,\phi$ or $\neg\psi$. Therefore, the application of EH is justified.

Note that in natural deduction, inference rules come in pairs for every connective. For every connective *, there is *-introduction, whose conclusion has * as the top-level connective, and *-elimination, where one of the premises has * as the top-level connective. So the standard names for UE and EH are universal elimination and existential elimination, respectively. Universal Eradication sounds pretty radical!

#### fumbles

##### New member
Why is it that v occurs freely in ?

We know that v is bound in $$\psi$$, so how do we know it's free here? $$\neg\phi\leftrightarrow\psi$$

Last edited by a moderator:

#### Evgeny.Makarov

##### Well-known member
MHB Math Scholar
Why is it that v occurs freely in $\neg\phi\leftrightarrow\psi$?
Strictly speaking, v may not be free in that formula. When I said,

In your case, $\neg\psi$ has open assumptions $\forall x\,\phi$ and $\neg\phi\leftrightarrow\psi$. The variable $v$ occurs freely in $\neg\phi\leftrightarrow\psi$ but not in $\forall x\,\phi$ or $\neg\psi$.
I was describing a typical case. If v occur free neither in $\phi$ nor in $\psi$, then this derivation reduces to propositional reasoning. But if v occurs free in $\phi$, then it also does in $\neg\phi\leftrightarrow\psi$. The point is that EH allows v to occur free in that formula, but not in $\neg\psi$ or other open assumptions of $\neg\psi$.

#### fumbles

##### New member
I think I get it. The Existential Hypothesis rule is quite hard compared to the others.