Talk:Sequent calculus
From LLWiki
(Difference between revisions)
(→Quantifiers: subformula of <math>\forall X A</math>) |
(→Two-sided sequent calculus: new section) |
||
| Line 8: | Line 8: | ||
* Define immediate subformula of <math>\forall X A</math> as <math>A</math>? |
* Define immediate subformula of <math>\forall X A</math> as <math>A</math>? |
||
-- [[User:Olivier Laurent|Olivier Laurent]] 18:37, 14 January 2009 (UTC) |
-- [[User:Olivier Laurent|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 <math>\Gamma\vdash\Delta \mapsto {}\vdash\Gamma\orth,\Delta</math> |
||
| + | * 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". |
||
| + | |||
| + | -- [[User:Olivier Laurent|Olivier Laurent]] 21:34, 15 January 2009 (UTC) |
||
Revision as of 23:34, 15 January 2009
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
and 
. 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 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
- 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)
