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

  • $\begingroup$ What are your logical axioms and rules of inference? Without knowing this, it is impossible to give you a meaningful answer. $\endgroup$ Dec 30 '18 at 14:35
  • $\begingroup$ @HenningMakholm I have edited the question to include the logical axioms and rules of inference. $\endgroup$
    – Oliver G
    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$.

  • $\begingroup$ 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. $\endgroup$
    – Oliver G
    Dec 30 '18 at 15:14
  • $\begingroup$ Otherwise known as weakening $\endgroup$ Dec 30 '18 at 15:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.