<p>The first book that Andrej Bauer suggested above (<a href="https://www.cambridge.org/core/books/basic-proof-theory/928508F797214A017D245A1FB67CCCD9" rel="nofollow noreferrer">Basic Proof Theory</a>) contains the rules you are looking for.</p>
<p>Due to the connection between minimal logic and lambda-calculus, the following paper might be relevant to your question: Hugo Herbelin. <em>A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure.</em> Computer Science Logic, Sep 1994, Kazimierz, Poland. pp.61–75. <a href="https://hal.inria.fr/inria-00381525" rel="nofollow noreferrer">https://hal.inria.fr/inria-00381525</a>. It contains a sequent calculus for minimal logic, though it might not be a historical or textbook source.</p>

CC BY-SA 4.0
2023-05-04T17:42:09.890Z
The first book that Andrej Bauer suggested above (Basic Proof Theory) contains the rules I was looking for, or at least one possible axiomatization of them that matched what I was expecting (same rules as MELLP), so perhaps you could add a remark to that in the answer. I will still accept the answer as this paper, indeed, shows a possible syntax for minimal logic in sequent calculus style which is related to what I'm trying to do (in fact, what they did in there looks pretty similar to Appel's interpreter for CPS terms!).
paulotorrens
CC BY-SA 4.0
2023-05-04T16:29:30.913Z
2023-05-05T13:29:47.327Z
2023-05-05T13:29:47.327Z
gadmm
<p>Are there any references I could use which explictly contain the rules for minimal logic, <em>both</em> as a sequent calculus and in natural deduction? (Doesn't need to be the same reference for both!)</p>
<p>To give some context, plus some more specific points: I'm working with CPS translations and their view in logic (this is <a href="https://cstheory.stackexchange.com/q/50964/51841">related to this question</a>), 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 {<span class="math-container">$\land,\lor,\neg$</span>} or {<span class="math-container">$\land,\neg$</span>} fragments). So, references containing explicit rules for (constructive) negation are welcome, as well as references which use such double negation translations.</p>
<p>It was actually hard finding the rules for classical and intuitionistic logic being summarized; <a href="https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK" rel="nofollow noreferrer">Wikipedia lists the rules for System LK</a>, and I could only find the <a href="http://pages.cpsc.ucalgary.ca/%7Erobin/class/617/projects-10/Subashis.pdf" rel="nofollow noreferrer">rules for System LJ in here</a> (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).</p>
<p>Remark: I'm pretty much assuming at this point that the rules for implication-free minimal logic with constructive negation in sequent calculus match <em>exactly</em> 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.</p>

CC BY-SA 4.0
2023-05-02T07:56:15.167Z
That's the sort of thing I would look for in Schwichtenberg & Troelstra's book [Basic proof theory](https://doi.org/10.1017/CBO9781139168717). Have you checked it?
Andrej Bauer
CC BY-SA 4.0
2023-05-02T09:38:06.163Z
@AndrejBauer, thanks a lot, I was not aware of that book. This confirms my suspicion. The book doesn't seem to give explicit rules for negation, and it would be nice to find somewhere that does, but this should be enough. Please feel free to turn your comment into an answer.
paulotorrens
CC BY-SA 4.0
2023-05-02T21:00:07.270Z
Another book that comes to mind is Takeuti's [Proof theory](https://store.doverpublications.com/0486490734.html).
Andrej Bauer
CC BY-SA 4.0
2023-05-03T06:58:11.693Z
Most presentations I know tend to base their calculi on implication though - afaik Takeuti's presentation has all operators.
lambda.xy.x
CC BY-SA 4.0
2023-05-03T13:56:38.527Z
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.
gadmm
CC BY-SA 4.0
2023-05-04T05:25:59.477Z
@gadmm, I'm really glad you've seem this question! I'm not sure what you mean by "derive implication" in here, though. The statement I'm looking for, and it seems correct based on the book suggested above, is that: if I take (ME)LLP, and I remove the internalized duality by moving negative formulas to the left of the sequent as their dual (so I have only positive formulas now, on both sides), taking the tensor as conjunction and bang as negation, I get the _same rules_ as minimal logic as a sequent calculus (except left/right implication, of course). Am I missing something?
paulotorrens
CC BY-SA 4.0
2023-05-04T13:54:34.920Z
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.
gadmm
<reference-request><lo.logic><linear-logic>
Which are the rules for minimal logic in both sequent calculus and natural deduction styles?
paulotorrens
# Which are the rules for minimal logic in both sequent calculus and natural deduction styles?

(Asked by: username_0 on 2023-05-02)

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](https://cstheory.stackexchange.com/q/50964/51841)), 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](https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK), and I could only find the [rules for System LJ in here](http://pages.cpsc.ucalgary.ca/%7Erobin/class/617/projects-10/Subashis.pdf) (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.

**Tags:** reference-request, lo.logic, linear-logic

> **Comments:**
> **username_1**: That's the sort of thing I would look for in Schwichtenberg & Troelstra's book [Basic proof theory](https://doi.org/10.1017/CBO9781139168717). Have you checked it?  
> **username_0**: @AndrejBauer, thanks a lot, I was not aware of that book. This confirms my suspicion. The book doesn't seem to give explicit rules for negation, and it would be nice to find somewhere that does, but this should be enough. Please feel free to turn your comment into an answer.  
> **username_1**: Another book that comes to mind is Takeuti's [Proof theory](https://store.doverpublications.com/0486490734.html).  
> **username_2**: Most presentations I know tend to base their calculi on implication though - afaik Takeuti's presentation has all operators.  
> **username_3**: 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.  
> **username_0**: @username_3, I'm really glad you've seem this question! I'm not sure what you mean by "derive implication" in here, though. The statement I'm looking for, and it seems correct based on the book suggested above, is that: if I take (ME)LLP, and I remove the internalized duality by moving negative formulas to the left of the sequent as their dual (so I have only positive formulas now, on both sides), taking the tensor as conjunction and bang as negation, I get the _same rules_ as minimal logic as a sequent calculus (except left/right implication, of course). Am I missing something?  
> **username_3**: 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.  

---

## 1 answers

### Answer by username_3 on 2023-05-04. Score: 3 | Accepted answer

The first book that username_1 suggested above ([Basic Proof Theory](https://www.cambridge.org/core/books/basic-proof-theory/928508F797214A017D245A1FB67CCCD9)) contains the rules you are looking for.

Due to the connection between minimal logic and lambda-calculus, the following paper might be relevant to your question: Hugo Herbelin. *A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure.* Computer Science Logic, Sep 1994, Kazimierz, Poland. pp.61–75. <https://hal.inria.fr/inria-00381525>. It contains a sequent calculus for minimal logic, though it might not be a historical or textbook source.

> **Comments:**
> **username_0**: The first book that username_1 suggested above (Basic Proof Theory) contains the rules I was looking for, or at least one possible axiomatization of them that matched what I was expecting (same rules as MELLP), so perhaps you could add a remark to that in the answer. I will still accept the answer as this paper, indeed, shows a possible syntax for minimal logic in sequent calculus style which is related to what I'm trying to do (in fact, what they did in there looks pretty similar to Appel's interpreter for CPS terms!).  

---

