MHB Solving a Logic Proof: Existential Hypothesis Rule

[Fumbles22]

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

View attachment 691

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:

View attachment 692

..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
UE = Universal Eradicator
Taut = Tautology
CP = Conditional Proposition
EH= Existential Hypothesis

Thanks in advance

 

[Evgeny.Makarov]

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! :)

 

[Fumbles22]

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\)

 

[Evgeny.Makarov]

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$.

 

[Fumbles22]

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

Universal Eradication sounds pretty radical!

When I was reading the page, I accidentally read "elimination" as "eradication". Since I was in learning mode, I remembered it as eradication. When I was writing the post I was thinking "it's elimination, not eradication" but then completely forgot at the key moment.

I've finally finished the sheet, which is why I'm a bit late posting this. On to Quantum Phenomena!

Thanks for your help emakarov!