[Om] logic1 CD revision?

[Clare So]

I did not realize there is a big/issue-reporting tool for OpenMath.  Is 
there any link to this site from the OpenMath webpage?

Clare

Paul Libbrecht wrote:
> I would be looking forward for issue-report or attempts at correction on 
> the issue tracker:
>  http://jira.activemath.org/browse/OM
> 
> paul
> 
> Jacques Carette wrote:
>> "the" logic???  Do you know how many two-valued boolean logics there are?
>>
>> You might mean "classical two-valued, first-order Boolean 
>> propositional logic".
>>
>> And while I am looking at it:
>> 1) doesn't anyone see anything wrong with the FMP for 'equivalent'?  
>> It seems to use a circular definition.
>> 2) the FMP (and CMP) for 'not' does not characterize 'not' as this FMP 
>> is also satisfied by the identity.  The informal description is 
>> actually a better 'definition'.
>> 3) in the same vein, the FMP for 'or', 'and' are not sufficient to 
>> uniquely define them either, as well as all being consequences of 
>> excluded-middle.  So _all_ the FMPs in this CD turn out to be 
>> restatements of excluded-middle!
>> 4) those FMPs use the forall quantifier, which is defined in quant1 
>> which depends on logic1.
>>
>> Jacques
>>