Talk:Sequent calculus

Quantifiers

The presentation does not seem to be completely uniform concerning quantifiers: are first-order quantifiers taken into account? It would be nice.

A few related points:

• Why a distinction between atomic formulas and propositional variables?
• Some mixing between $\forall x A$ and $\forall X A$. I tried to propose a convention on that point, but it does not match here with the use of α for atoms.
• Define immediate subformula of $\forall X A$ as A?

-- Olivier Laurent 18:37, 14 January 2009 (UTC)

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 $\Gamma\vdash\Delta \mapsto {}\vdash\Gamma\orth,\Delta$
• 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)