Let $\gamma\in \text{Form}$. A proof of $\gamma$ is a sequence of formulas $\phi_1,\phi_2,...,\phi_n=\gamma$ where each $\phi_i$ is an instance of an axiom or was obtained by modus ponens from two previous formulas.

The axioms we use are

Axiom 1: $ (\alpha\implies (\beta \implies \alpha)).$

Axiom 2: $((\alpha \implies (\beta \implies \gamma ))\implies (( \alpha \implies \beta) \implies (\alpha \implies \gamma))).$

Axiom 3: $((\neg \alpha \implies \neg \beta) \implies ((\neg \alpha \implies \beta) \implies \alpha)).$


We say that $\Gamma\vdash \gamma$ if there exists a finite proof of $\gamma$ from $\Gamma$ (that is, each formula of $\Gamma$ can be treated as an axiom).


We say a set $\Gamma$ is inconsistent if there exists a formula $\alpha$ such that $\Gamma \vdash \alpha$ and $\Gamma\vdash \neg \alpha$.

Now I want to show that if $\Gamma\cup \{\gamma\}$ is inconsistent, then $\Gamma\vdash \neg\gamma$, but I'm pretty lost.

We know there exists some $\varphi$ such that $\Gamma\cup \{\gamma\}\vdash \varphi,\neg\varphi$, but I don't see how this helps.

I also proved that a $\Gamma$ set is inconsistent if and only if $\Gamma\vdash \beta$ for every formula $\beta$, thinking this would help, but didn't get far.

Could someone help me out?

Also, a side question, does the system I described here have a common name? I could find very little information about it (I'm trying to prove the completeness theorem using this system, and need this for Lindembaum's lemma).

  • $\begingroup$ There's this similar question, but the comments/answer didn't quite help me: math.stackexchange.com/questions/1018833/… $\endgroup$ – YoTengoUnLCD Jan 22 '16 at 19:41
  • 1
    $\begingroup$ It is the so-called Mendelson's axiom system. $\endgroup$ – Mauro ALLEGRANZA Jan 22 '16 at 20:21
  • $\begingroup$ Well, the question is basically the same, but it has only one answer, with negative score, the author also didn't say which system he was using, unlike I did. $\endgroup$ – YoTengoUnLCD Jan 23 '16 at 0:14
  • $\begingroup$ @MauroALLEGRANZA Thanks! I had no idea it was from that book. $\endgroup$ – YoTengoUnLCD Jan 23 '16 at 0:38


For Mendelson's system, see :

We need :

Lemma 1.8 [ page 27 ] : $\vdash \varphi \to \varphi$.

With it, (Ax.1) and (Ax.2), we can prove Prop.1.9 (Deduction Th) [ page 28 ] and some useful results [ page 29 ]:

Corollary 1.10(a) : $\varphi \to \psi, \psi \to \tau \vdash \varphi \to \tau$

and :

Lemma 1.11(b) : $\vdash \lnot \lnot \varphi \to \varphi$.

First, we can prove the "easy" version :

a) if $\Gamma \cup \{ \lnot \gamma \}$ is inconsistent, then $\Gamma ⊢ \gamma$.


1) $\Gamma \cup \{ \lnot \gamma \}$ is inconsistent, i.e. $\Gamma \cup \{ \lnot \gamma \} \vdash \varphi$ and $\Gamma \cup \{ \lnot \gamma \} \vdash \lnot \varphi$, for some formula $\varphi$

Thus :

2) $\Gamma \vdash \lnot \gamma \to \varphi$ --- from 1) by Ded.Th

3) $\Gamma \vdash \lnot \gamma \to \lnot \varphi$ --- from 1) by Ded.Th

4) $\vdash (\lnot \gamma \to \lnot \varphi) \to ((\lnot \gamma \to \varphi) \to \gamma)$ --- (Ax.3)

5) $\Gamma \vdash \gamma$ --- from 2), 3) and 4) by modus ponens twice.

Finally, for the sought result :

b) if $\Gamma \cup \{ \gamma \}$ is inconsistent, then $\Gamma ⊢ \lnot \gamma$,

we have to apply Noah's suggestion.

As in case a) above, we have :

1) $\Gamma \vdash \gamma \to \varphi$

2) $\Gamma \vdash \gamma \to \lnot \varphi$

3) $\vdash \lnot \lnot \gamma \to \gamma$ --- by Lemma 1.11(a)

4) $\Gamma \vdash \lnot \lnot \gamma \to \lnot \varphi$ --- from 2), 3) and Corollary 1.10(a)

5) $\Gamma \vdash \lnot \lnot \gamma \to \varphi$ --- from 1), 3) and Corollary 1.10

6) $\vdash (\lnot \lnot \gamma \to \lnot \varphi) \to ((\lnot \lnot \gamma \to \varphi) \to \lnot \gamma)$ --- (Ax.3)

7) $\Gamma \vdash \lnot \gamma$ --- from 4), 5) and 6) by modus ponens twice.

  • $\begingroup$ Excellent Mauro. Thanks!! $\endgroup$ – YoTengoUnLCD Jan 23 '16 at 0:37

I'm assuming you've already proved that this system satisfies the Deduction Theorem ($\Gamma\cup\{\gamma\}\vdash\varphi$ implies $\Gamma\vdash\gamma\rightarrow\varphi$) and double negation equivalence ($\Gamma\cup\{\gamma\}\vdash\varphi$ implies $\Gamma\cup\{\neg\neg\gamma\}\vdash\varphi$).

If so, then if $\Gamma\cup\{\gamma\}$ is inconsistent, then for some $\varphi$ we have $$\Gamma\vdash \neg\neg \gamma\rightarrow\varphi\mbox{ and } \Gamma\vdash\neg\neg\gamma\rightarrow\neg\varphi.$$ So applying Axiom 3 gives us $\Gamma \vdash \neg\gamma$.

  • $\begingroup$ No, I haven't yet proved neither yet (in fact, my next question was going to be about a proof of the deduction theorem here). What allows me to substitute a formula with its double negation there? $\endgroup$ – YoTengoUnLCD Jan 22 '16 at 19:54
  • $\begingroup$ @YoTengoUnLCD Actually, looking more at your system I'm not at all sure it satisfies the second property I mention, although I strongly suspect it does satisfy the deduction theorem. Where did you run into this particular list of axioms? (It's possible it is complete, but now I'm doubtful.) $\endgroup$ – Noah Schweber Jan 22 '16 at 19:59
  • $\begingroup$ In a course of logic in my university, proving the soundness and completeness of the system was given as an exercise for the final. I could prove that the system is sound pretty easily, but not more than that. $\endgroup$ – YoTengoUnLCD Jan 22 '16 at 20:04

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.