<p>I try to understand the differences between the calculi mentioned above, mainly the difference between natural deduction and the sequence calculus. For this I consulted the <a href="https://en.wikipedia.org/wiki/Sequent_calculus" rel="nofollow noreferrer">wikipedia article on the sequent calculus</a>, &quot;Proof Theory&quot; by Gaisi Takeuti and &quot;Basic Proof Theory&quot; by Troelstra and Schwichtenberg.</p>
<p>The wikipedia article says that natural deduction (which I understand to be <strong>NK</strong>) has judgements of the form <span class="math-container">$A_1, A_2, ..., A_n\vdash B$</span> and then goes on to define the sequent calculus (which I understand to be <strong>LK</strong>) as a generalisation of judgements to <span class="math-container">$A_1, A_2, ..., A_n\vdash B_1, B_2, ..., B_k$</span>.</p>
<p>Takeuti, as well as Troelstra and Schwichtenberg, define <strong>LK</strong> (resp. <strong>G1c</strong>) with judgements of the form <span class="math-container">$A_1, A_2, ..., A_n\vdash B_1, B_2, ..., B_k$</span> and then say that we define <strong>LJ</strong> (resp. <strong>G1i</strong>) by restricting the judgements to have only one formula on the right side of the turnstile.</p>
<p>So my question is essentially: if I restrict judgements of <strong>LK</strong> to have only one formula on the right side of the turnstile, do I get <strong>LJ</strong> or <strong>NK</strong>?</p>

CC BY-SA 4.0
2022-03-19T08:09:27.917Z
The difference is in the rules: natural deduction has introduction and elimination rules on the right-hand side, whereas a sequent calculus has only introduction rules, but on both sides.
Emil Jeřábek
CC BY-SA 4.0
2022-03-25T09:21:01.477Z
You get $\mathbf{LJ}$.  $\mathbf{NK}$ and $\mathbf{LJ}$ have the same shape of sequents, but, as Emil Jeřábek says, they manipulate such sequents in rather different ways.
Damiano Mazza
<proof-theory>
Confusion about different definitions of LK, LJ, NK, and NJ
Florian
# Confusion about different definitions of LK, LJ, NK, and NJ

(Asked by: username_0 on 2022-03-19)

I try to understand the differences between the calculi mentioned above, mainly the difference between natural deduction and the sequence calculus. For this I consulted the [wikipedia article on the sequent calculus](https://en.wikipedia.org/wiki/Sequent_calculus), "Proof Theory" by Gaisi Takeuti and "Basic Proof Theory" by Troelstra and Schwichtenberg.

The wikipedia article says that natural deduction (which I understand to be **NK**) has judgements of the form $A\_1, A\_2, ..., A\_n\vdash B$ and then goes on to define the sequent calculus (which I understand to be **LK**) as a generalisation of judgements to $A\_1, A\_2, ..., A\_n\vdash B\_1, B\_2, ..., B\_k$.

Takeuti, as well as Troelstra and Schwichtenberg, define **LK** (resp. **G1c**) with judgements of the form $A\_1, A\_2, ..., A\_n\vdash B\_1, B\_2, ..., B\_k$ and then say that we define **LJ** (resp. **G1i**) by restricting the judgements to have only one formula on the right side of the turnstile.

So my question is essentially: if I restrict judgements of **LK** to have only one formula on the right side of the turnstile, do I get **LJ** or **NK**?

**Tags:** proof-theory

> **Comments:**
> **username_1**: The difference is in the rules: natural deduction has introduction and elimination rules on the right-hand side, whereas a sequent calculus has only introduction rules, but on both sides.  
> **username_2**: You get $\mathbf{LJ}$.  $\mathbf{NK}$ and $\mathbf{LJ}$ have the same shape of sequents, but, as username_1 says, they manipulate such sequents in rather different ways.  

---

## 0 answers

