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$ Jan 22, 2016 at 19:41
  • 1
    $\begingroup$ It is the so-called Mendelson's axiom system. $\endgroup$ Jan 22, 2016 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$ Jan 23, 2016 at 0:14
  • $\begingroup$ @MauroALLEGRANZA Thanks! I had no idea it was from that book. $\endgroup$ Jan 23, 2016 at 0:38

2 Answers 2



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$ Jan 23, 2016 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$ Jan 22, 2016 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$ Jan 22, 2016 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$ Jan 22, 2016 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.