1
$\begingroup$

Definition

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

Definition

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

Definition

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

$\endgroup$
4
  • $\begingroup$ There's this similar question, but the comments/answer didn't quite help me: math.stackexchange.com/questions/1018833/… $\endgroup$ Commented Jan 22, 2016 at 19:41
  • 1
    $\begingroup$ It is the so-called Mendelson's axiom system. $\endgroup$ Commented 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$ Commented Jan 23, 2016 at 0:14
  • $\begingroup$ @MauroALLEGRANZA Thanks! I had no idea it was from that book. $\endgroup$ Commented Jan 23, 2016 at 0:38

2 Answers 2

4
$\begingroup$

Hint

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

Proof

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.

$\endgroup$
1
  • $\begingroup$ Excellent Mauro. Thanks!! $\endgroup$ Commented Jan 23, 2016 at 0:37
1
$\begingroup$

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

$\endgroup$
3
  • $\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$ Commented 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$ Commented 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$ Commented Jan 22, 2016 at 20:04

You must log in to answer this question.

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