1
$\begingroup$

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.

Improve this question
$\endgroup$
7
  • 2
    $\begingroup$ That's the sort of thing I would look for in Schwichtenberg & Troelstra's book Basic proof theory. Have you checked it? $\endgroup$
    – Andrej Bauer
    May 2 at 7:56
  • 3
    $\begingroup$ Another book that comes to mind is Takeuti's Proof theory. $\endgroup$
    – Andrej Bauer
    May 2 at 21:00
  • 1
    $\begingroup$ Most presentations I know tend to base their calculi on implication though - afaik Takeuti's presentation has all operators. $\endgroup$
    – lambda.xy.x
    May 3 at 6:58
  • 1
    $\begingroup$ 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. $\endgroup$
    – gadmm
    May 3 at 13:56
  • 1
    $\begingroup$ 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. $\endgroup$
    – gadmm
    May 4 at 13:54

1 Answer 1

Reset to default
3
$\begingroup$

The first book that Andrej Bauer suggested above (Basic Proof Theory) 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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ 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!). $\endgroup$
    – paulotorrens
    May 4 at 17:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.