[Om] logic1 CD revision?
socm at mcmaster.ca
Thu Aug 17 17:01:50 CEST 2006
I did not realize there is a big/issue-reporting tool for OpenMath. Is
there any link to this site from the OpenMath webpage?
Paul Libbrecht wrote:
> I would be looking forward for issue-report or attempts at correction on
> the issue tracker:
> 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.
More information about the Om