0

I am trying to provide intuitionistic sequent proofs (Gentzen Style) for a few statements.

The rules that I have are the rule of assumption, conjunction introduction and elimination, disjunction introduction and elimination, conditional introduction and elimination, double negation introduction, reductio ad absurdum, and ex falso.

In particular, we do not have double negation elimination since this is intuitionistic logic.

The rules above are given by Sider in his book Logic for Philosophy Section 2.4.

I am trying to prove the following statements within this logic.

$1. \Rightarrow \alpha \rightarrow (\neg \alpha \rightarrow \beta)$

$2. \neg \neg (\alpha \land \beta) \Rightarrow \neg \neg \alpha \land \neg \neg \beta$

$3. \Rightarrow \neg \neg (\neg \neg \alpha \rightarrow \alpha)$

$4. \neg \neg (\alpha \rightarrow \beta), \neg \neg \alpha \Rightarrow \neg \neg \beta$

I only managed to prove the first statement $\Rightarrow \alpha \rightarrow (\neg \alpha \rightarrow \beta)$ which is somewhat intuitive.

I'm having trouble with the other three statements in the Gentzen style. And I cannot use any other metalangauge proof theorems that may simplify the derivations.

I tried looking at other resources, but almost every logic book does sequent proofs differently. Any help would be appreciated.

  • Alas, I won't have time to write a comprehensive answer any time soon: I hope someone else will help you.

    But I have time for a word of warning: the system presented in Sider's book is not a Gentzen-style Sequent Calculus! Instead, it looks like the Ni system presented in A.S. Troelstra and H. Schwichtenberg's Basic Proof Theory (or one of its close relatives), what we sometimes call a "Natural Deduction system presented in sequent style".

     – Z. A. K. Feb 16 '21 at 21:40
  • Ni works just like a Natural Deduction system, but instead of a tree with assumptions as leaves, we have the set of not-yet-discharged assumptions on the left of the $\Rightarrow$. This should explain your observation that "almost every logic book does sequent proofs differently": paradoxically, you would have had better luck by looking at resources about proving things in Natural Deduction! – Z. A. K. Feb 16 '21 at 21:41
  • I'll try looking through the book you suggested. –  Feb 16 '21 at 22:41
  • Whoever has pointed you to Sider's book has done you a disservice. While the later chapters on modal logic are OK, the first half of the book is I think pretty poor stuff. https://www.logicmatters.net/tyl/booknotes/sider/ There are much better introductions to natural deduction and/or to proper sequent proofs available. – Peter Smith Feb 17 '21 at 10:03
  • When working with problems such as this, it can be useful to use the derived rule that if $\Gamma$ is a context (set of formulas) and $\alpha, \beta$ are formulas, then $\Gamma \cup { \alpha } \Rightarrow \lnot\beta$ implies $\Gamma \cup { \lnot\lnot\alpha } \Rightarrow \lnot\beta }$. In other words, if the goal of the current step is a negation, then you can freely eliminate double negations on hypotheses; or, again if the goal is a negation, by using the cut rule, you can freely introduce hypotheses $\delta \lor \lnot\delta$ as if excluded middle held. – Daniel Schepler Feb 17 '21 at 21:32

1 Answers1

1

For 2):

  1. $¬¬(α ∧ β)$ --- premise
  2. $¬α$ --- assumption [a]
  3. $α ∧ β$ --- assumption [b]
  4. $α$ --- from 3)
  5. $\bot$ --- from 2) and 4)
  6. $¬(α ∧ β)$ --- from 3) and 5), discharging [b]
  7. $\bot$ --- from 1) and 6)
  8. $¬¬α$ --- from 2) and 7) , discharging [a]

Now repeat from:

  1. $¬β$ --- assumption [c]
  2. $α ∧ β$ --- assumption [d]

deriving:

  1. $¬¬β$ --- discharging [c] and [d]
  1. $¬¬α ∧ ¬¬β$ --- from 8) and 11).

For 3:

  1. $\lnot (\lnot \lnot p \to p)$ --- assumption [0]
  2. $p$ --- assumption [a]
  3. $\lnot \lnot p \to p$ --- from 2)
  4. $\bot$
  5. $\lnot p$ --- from 2) and 4), discharging [a]
  6. $\lnot \lnot \lnot p$ --- assumption [b]
  7. $\lnot \lnot p \to p$ --- from 6) and $\vdash \lnot p \to (p \to q)$
  8. $\bot$
  9. $\lnot \lnot \lnot \lnot p$ --- from 6) and 8) discharging [b]
  10. $\lnot p$ --- assumption [c]
  11. $\lnot \lnot \lnot p$ --- from 10) and $\vdash p \to \lnot \lnot p$
  12. $\bot$
  13. $p$ --- from 12)
  14. $\lnot \lnot p \to p$ --- from 10) and 13), discharging [c]
  15. $\bot$
  1. $\lnot \lnot (\lnot \lnot p \to p)$ --- from 1) and 15), discharging [0]

For 4):

  1. $¬¬(α → β)$ --- premise

  2. $¬¬α$ --- premise

  3. $¬β$ --- assumption [a]

  4. $α → β$ --- assumption [b]

  5. $α$ --- assumption [c]

  6. $β$ --- from 4) and 5)

  7. $\bot$ --- from 3) and 6)

  8. $¬α$ --- from 5) and 7) discharging [c]

  9. $\bot$ --- from 2) and 8)

  10. $¬(α → β)$ --- from 4) and 9), discharging [b]

  11. $\bot$ --- from 1) and 10)

  1. $¬¬β$ --- from 3) and 11), discharging [a]
Mauro ALLEGRANZA
  • 94,169