Talk:Sequent calculus
From LLWiki
Revision as of 16:45, 14 March 2009 by Olivier Laurent (Talk | contribs)
Two-sided sequent calculus
I think the terminology "two-sided sequent calculus" should be used for the system where all the connectives are involved and all the rules are duplicated (with respect to the one-sided version) and negation is a connective.
In this way, we obtain the one-sided version from the two-sided one by:
- quotient the formulas by de Morgan laws and get negation only on atoms, negation is defined for compound formulas (not a connective)
- fold all the rules by
- remove useless rules (negation rules become identities, almost all the rules appear twice)
A possible name for the two-sided system presented here could be "two-sided positive sequent calculus".
-- Olivier Laurent 21:34, 15 January 2009 (UTC)