Talk:Sequent calculus
From LLWiki
(Difference between revisions)
(Dealing with quantifiers) |
(→Quantifiers: subformula of <math>\forall X A</math>) |
||
| Line 6: | Line 6: | ||
* Why a distinction between atomic formulas and propositional variables? |
* Why a distinction between atomic formulas and propositional variables? |
||
* Some mixing between <math>\forall x A</math> and <math>\forall X A</math>. I tried to propose a [[notations#formulas|convention]] on that point, but it does not match here with the use of <math>\alpha</math> for atoms. |
* Some mixing between <math>\forall x A</math> and <math>\forall X A</math>. I tried to propose a [[notations#formulas|convention]] on that point, but it does not match here with the use of <math>\alpha</math> for atoms. |
||
| + | * 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) |
||
Revision as of 00:04, 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)
