Arjeh Cohen wrote:
> 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.
>
I think the idea is to provide a place to focus on particular issue.
This is slightly similar to an email thread, e.g. on this list, with two
major differences:
- it only makes noise to people that "watch" it (this is default)
- it allows uploads
Note that anyone can login and add comments, upload proposed changed
files (as Bill actually did), and add other watchers... so I think your
comment below would have been best there even though an invitation on
the list to go discuss at the issue
http://jira.activemath.org/browse/OM-2
I am unclear why I didn't upload this slight clarification of Bill
yet... maybe I was hoping to get some feedback which you are providing here.
paul
> 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...
>>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/x-pkcs7-signature
Size: 3245 bytes
Desc: S/MIME Cryptographic Signature
Url : http://openmath.org/pipermail/om/attachments/20061002/15b2ac0a/attachment.bin