Simple consequence relations (Q809992): Difference between revisions

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.