# Which are the rules for minimal logic in both sequent calculus and natural deduction styles?

Are there any references I could use which explictly contain the rules for minimal logic, both as a sequent calculus and in natural deduction? (Doesn't need to be the same reference for both!)

To give some context, plus some more specific points: I'm working with CPS translations and their view in logic (this is related to this question), and I'm particularly interested in the double negation translations that map classical logic into the implication-free fragment of minimal logic (i.e., the {$$\land,\lor,\neg$$} or {$$\land,\neg$$} fragments). So, references containing explicit rules for (constructive) negation are welcome, as well as references which use such double negation translations.

It was actually hard finding the rules for classical and intuitionistic logic being summarized; Wikipedia lists the rules for System LK, and I could only find the rules for System LJ in here (if I recall correctly, it's possible to define System LJ with multiple conclusions, in a restricted fashion, but I'm not sure if this is true for minimal logic). I've tried checking Gentzen's paper, but the pdf has really bad quality, and it's in German (just as the paper that introduces minimal logic).

Remark: I'm pretty much assuming at this point that the rules for implication-free minimal logic with constructive negation in sequent calculus match exactly those of Laurent's polarized linear logic. I haven't found any references about this, so if that's correct I'm not sure if anyone has pointed that out.

• That's the sort of thing I would look for in Schwichtenberg & Troelstra's book Basic proof theory. Have you checked it? Commented May 2, 2023 at 7:56
• Another book that comes to mind is Takeuti's Proof theory. Commented May 2, 2023 at 21:00
• Most presentations I know tend to base their calculi on implication though - afaik Takeuti's presentation has all operators. Commented May 3, 2023 at 6:58
• Regarding the remark: it is important to note that "minimal logic with negation", as used as the target of CPS-style double-negation translations, is not the same as minimal logic since you cannot derive implication from negation alone. So it is not clear that a reference for minimal logic would help you with your stated goals. Regarding the fact that Laurent's LLP is a symmetrical version of the logic with product and negation, I do not know what precise statement you are looking for, but from my own understanding, this is explained in the two other references I gave in the question linked. Commented May 3, 2023 at 13:56
• I meant that the fragment with negation you are interested in is different from what is usually meant by minimal logic, as it is specifically introduced in the context of CPS. I can confirm that your observation regarding the connection with Laurent's LLP was part of the motivations of the two publications I linked in the related question. This is stated explicitly on page 10 of Melliès and Tabareau's paper and on page 92 of my PhD thesis. I hope this helps clarify the connection between minimal logic and Laurent's LLP in the context of CPS translations and double negation translations. Commented May 4, 2023 at 13:54