[Om] logic1 CD revision?

[Jacques Carette]

As someone who spoke up during the logic1 discussion, I would have to 
say that I like this approach to the content of logic1 (and other CDs 
too), namely that in a base CD some symbols are defined quite loosely 
(see alg1.one and alg1.zero), and then give actual semantics in other, 
more refined CDs.  That way the base CDs would be more about defining a 
lingua franca almost at the level of syntax.  This should be much more 
reusable [although I expect that most applications would want to specify 
a "semantic" CD rather than a basic one].

Jacques

PS: I rather appreciate the statement below that "OpenMath does not 
really follow logic in its approach to mathematics".  It probably goes a 
long to way to explain why so few people in the theorem proving 
community have embraced it.

Arjeh Cohen wrote:
> 2) content: if you consider intuitionistic logic, the usual logic can be found
>    as a subsystem, by means of laws like
>    weakExists x A    ==== not Forall x not A
>    and
>    A weakOr B        ==== not( not A and not B)
>
>   In this way (cf. my paper with Henk Barendregt) you have the truth
>    (A weakOr not A), so the subsystem of intuitionistic logic represents
>   classical logic (excluded middle) and you can use the Exists x A
>   for the (strong ) statement that the x can actually be found constructively.
>
>   What I am trying to say is: in logic1 we may want to use the quantifiers
>    just as the mathematical symbols for many purposes. OpenMath does not
>     really follow logic in its apporach to mathematics. We make building blocks
>    to set up rigorous mathematics. Compare for instance to alg1.one
>    and alg1.zero.  These symbols are for use in all sorts of algebraic
>    structures to be cast upon the actual one of such a structure.
>
>   So if you want the excluded middle to hold, make a logic12.ocd,
>    where it is specified that you have the buyilding blocks for a for instance
>   ZF logic.
>
>
>
>
> Eager to learn your reactions, best regards, Arjeh M. Cohen.
>
>
>
> On Thu, Aug 17, 2006 at 11:34:28PM +0200, Paul Libbrecht wrote:
>   
>> W Naylor wrote:
>>     
>>>> I did not realize there is a big/issue-reporting tool for OpenMath.  Is 
>>>> there any link to this site from the OpenMath webpage?
>>>>    
>>>>         
>>> This is a new thing being set up by Paul, maybe it would be an idea to 
>>> have a link from the official site ... Paul?
>>>  
>>>       
>> I wanted to make sure it fits people before making an official link to 
>> it... I could see at least Bill happily working with it and would look 
>> forward to see others do so. The only issues that needs to be considered 
>> if we decide on moving to jira.activemath.org is that jira is not an 
>> open-source product and that on jira.activemath.org, the ActiveMath 
>> project is somewhat more visible... if both of these things are not a 
>> problem... I will make a link.
>>
>> paul
>>
>> PS: Bill, you've filed issue OM-2 about the logic1 revision but I've 
>> seen no attachment or details of the correction in the jira issue...
>>     
>
>
>
>   
>> _______________________________________________
>> Om mailing list
>> Om at openmath.org
>> http://openmath.org/mailman/listinfo/om
>>     
>
> _______________________________________________
> Om mailing list
> Om at openmath.org
> http://openmath.org/mailman/listinfo/om
>