Assuming $\Sigma \vdash \eta$, what is the deduction for $\Sigma \vdash \neg\eta \rightarrow \eta$?

Assuming $$\Sigma \vdash \eta$$, what is the deduction for $$\Sigma \vdash \neg\eta \rightarrow \eta$$?

I understand that $$\Sigma \vdash \eta \rightarrow \Sigma \cup\neg\eta \vdash \eta$$, but I'm trying to specifically find the derivation for $$\Sigma \vdash \neg\eta \rightarrow \eta$$.

I can't figure out how to do this. I know a deduction is a sequence of logical axioms or non-logical axioms from $$\Sigma$$ or by a rule of inference but any sequence I try doesn't seem to work.

Anyone have any ideas?

The rules of inference I am using are:

Type PC: If $$\Gamma$$ is a finite set of $$L$$ formulas and $$\phi$$ is an $$L$$ formula and $$\phi$$ is a propositional consequence of $$\Gamma$$, then $$(\Gamma, \phi)$$ is a rule of inference of type PC.

Type QR: Suppose $$x$$ is a variable that is not free in $$\psi$$. Then $$(\{\psi \rightarrow \phi\}, \psi \rightarrow (\forall x\phi)), (\{\phi \rightarrow \psi\}, (\exists x\phi) \rightarrow \psi)$$

The logical axioms I am using are:

E1: $$x=x$$ for each variable $$x$$

E2: $$[(x_1=y_1) \land (x_2=y_2) \land \dots (x_n = y_n)] \rightarrow f(x_1, x_2,, \dots, x_n) = f(y_1, y_2, \dots, y_n)$$

E3: $$[(x_1=y_1) \land (x_2=y_2) \land \dots (x_n = y_n)] \rightarrow (R(x_1, x_2,, \dots, x_n) \rightarrow R(y_1, y_2, \dots, y_n))$$

Q1: If $$t$$ is substitutable for $$x$$ in $$\phi$$, then $$(\forall x \phi) \rightarrow \phi_t^x$$

Q2: If $$t$$ is substitutable for $$x$$ in $$\phi$$, then $$\phi_t^x \rightarrow (\exists x \phi)$$

• What are your logical axioms and rules of inference? Without knowing this, it is impossible to give you a meaningful answer. Dec 30 '18 at 14:35
• @HenningMakholm I have edited the question to include the logical axioms and rules of inference. Dec 30 '18 at 15:03

$$\neg\eta\to\eta$$ is a propositional consequence of $$\eta$$.
So if you have a derivation of $$\Sigma\vdash \eta$$, appending a single PC step to it will give you a derivation of $$\Sigma\vdash\neg\eta\to\eta$$.
• I see now. $\eta \rightarrow (\neg \eta \rightarrow \eta)$ is the appropriate step since $\eta$ is the only thing being assumed we can then claim $\neg \eta \rightarrow \eta$ is in the deduction. Dec 30 '18 at 15:14