1
$\begingroup$

Let $S$ be an inconsistent set of propositional formulas.

If our system consists of the axioms:

\begin{align} AX1&\quad (P\implies (Q \implies P))\\ AX2&\quad (((P\implies(Q\implies R))\implies((P\implies Q)\implies(P\implies R)))\\ AX3&\quad ((\neg P\implies \neg Q)\implies((\neg P \implies Q) \implies P)) \end{align}

And the only inference rule is modus ponens, does $S\vdash \alpha\, \forall \,\alpha$?

I've been trying to construct a proof for $\alpha$ given $\Gamma \vdash \gamma, \neg \gamma$ for half an hour and couldn't get anywhere, maybe there's a simple combination of axiom application which works and I'm just not seeing it.

E: Following Noah's advice, I got this

\begin{align} 1.&\gamma &\text{Hyp}\\ 2.&\neg \gamma &\text{Hyp}\\ 3.&(\gamma\implies(\neg\alpha\implies \gamma))&\text{AX1}\\ 4.&(\neg\alpha\implies\gamma)&\text{MP (1,3)}\\ 5.&(\neg \gamma \implies (\neg \alpha \implies \neg \gamma))&\text{AX1}\\ 6.&(\neg \alpha \implies \neg \gamma)&\text{MP(2,5)}\\ 7.&((\neg \alpha \implies\neg \gamma) \implies ((\neg \alpha \implies \gamma)\implies \alpha))&\text{AX3}\\ 8.&((\neg \alpha \implies \gamma) \implies \alpha)) &\text{MP(6,7)}\\ 9.& \alpha.&\text{MP(4,8)}\\ \end{align}

$\endgroup$
  • 1
    $\begingroup$ I'm not sure how to formalize this, but I think a good idea is to take $P=\alpha,Q=\gamma$ and make use of AX3. $\endgroup$ – Wojowu Jan 20 '16 at 22:27
1
$\begingroup$

Here's an informal sketch.

Assume we've proved $A$ and $\neg A$, and fix any proposition $P$. Then we have $$\neg P\implies \neg A,$$ since we have the stronger proposition $\neg A$ (this uses AX1). Similarly, we have $\neg P\implies A$.

So by AX3, we have $P$.

$\endgroup$
  • $\begingroup$ Thanks! I think I got the proof right, would you mind checking it in my edit? $\endgroup$ – YoTengoUnLCD Jan 20 '16 at 22:52
  • $\begingroup$ @YoTengoUnLCD Looks good to me! $\endgroup$ – Noah Schweber Jan 20 '16 at 23:26

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.