2
$\begingroup$

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

$\endgroup$
2
  • $\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, 2018 at 14:35
  • $\begingroup$ @HenningMakholm I have edited the question to include the logical axioms and rules of inference. $\endgroup$
    – Oliver G
    Dec 30, 2018 at 15:03

1 Answer 1

2
$\begingroup$

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

$\endgroup$
2
  • $\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, 2018 at 15:14
  • $\begingroup$ Otherwise known as weakening $\endgroup$ Dec 30, 2018 at 15:17

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .