[Om] logic1 CD revision?

[Arjeh Cohen]

Dear OpenMathers,

It seems that the logic 1 discussion has ground to a halt.
There are two issues I want to bring up before proceeding:

1) organization: Of what use is the jira.activemath.org site to us.
   am I just meant to read what is going on? In this case, my
   question is how to make eg logic1.ocd readible from that site?

   Or are we supposed to edit and manage too? In this case maybe more
   instructions would be welcome.
   


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