Simple consequence relations (Q809992)

The approach to characterize propositional logical connectives by rules for sequent calculi was developed mainly via natural deduction. The author uses multiple sequent calculi with definitions like: internal disjunction is a binary connective \(+\) such that \(X\vdash Y,A,B\) iff \(X\vdash Y,A+B\). In this way he characterizes multiplicative and additive connectives of Girard's linear logic as well as other connectives. There is a hope to apply this framework for implementing logical systems on computers using the LF system. A good test for such an implementation is to try to prove translations (into the system considered) of sufficiently difficult intuitionistic formulas.