Re: BLD: two issues with the BNF

>> The second issue is not an error, but it can be considered misleading 
>> (the BNF is too liberal): in the presentation syntax, rules are 
>> quantified rule implications.  So, an atomic formula is not a rule and 
>> may thus not be directly included in a group.  According to the BNF, an 
>> atomic formula can be considered a rule; this is misleading.
> 
> There was a mistake in the math syntax. Groups should also allow atomic
> formulas. Fixed.

One more thing: atomic formulas can also contain variables.  I guess 
that such non-ground atomic formulas should not be allowed in groups?

Best, Jos

> 
> m
> 
>> Best, Jos
> 

-- 
                          debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
One man that has a mind and knows it can
always beat ten men who haven't and don't.
   -- George Bernard Shaw