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

Question

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. — hmakholm left over Monica, Dec 30 '18 at 14:35
@HenningMakholm I have edited the question to include the logical axioms and rules of inference. — Oliver G, Dec 30 '18 at 15:03

score 2 · Accepted Answer · answered Dec 30 '18 at 15:11

2

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

answered Dec 30 '18 at 15:11

hmakholm left over Monica

286,031

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. – Oliver G Dec 30 '18 at 15:14
Otherwise known as weakening – Agnishom Chattopadhyay Dec 30 '18 at 15:17

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

1 Answers1