[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Fwd: Request for references

From: Tim Daly
Subject: Re: [Axiom-developer] Fwd: Request for references
Date: Wed, 13 Dec 2017 11:36:15 -0500


As I mentioned, over the break I'm trying to climb the
substructural logic hill. It looks particularly interesting.

Axiom is based on group theory. It splits into two parts
"categories" (not category theory) which are collections of
signatures and "domains" which are implementations of

So in Axiom you start with Set or Type and then define
things like Group (which requires more singatures), Rings,
(more required signatures), Fields (e.g. a division signature).

Once the tower of categories exists you can define a
domain that inherits from some (sub-)tower. Now you have
to write code to implement each of the inherited signatures.

This gives Axiom a very useful way of organizing along the
lines of group theory.

Using my own form of reasoning (unreasonable analogy) it
must be possible to organize substructural logic into a set
of categories that can be organized in a similar way.

So, by analogy, it should be possible to start a root category
with a "reflexive signature" A |- A

Then a set of categories can be defined, one each, to allow
structural rules like Weakening which you might or might not

Then a set of categories with specific introduction and
elimination rules (e.g. one for ->I, ->E for implication)

Organized in this granular fashion one can then create
something like a LinearLogic, OrderedLogic,  or a Gentzen
domain that inherits only the categories that apply.

Clearly Halleck's work
both supports this idea and shows that it is too simplistic
to really cover all of logic. But for a reasonable subset such
as I will need while proving Axiom it seems that the naive
organization might be sufficient.

Just after our attempted phone call two books showed up
"An Introduction to Substructural Logics" and
"Abstract Algeraic Logic: An Introductory Textbook".

I'm part way through the first book and it looks like it
supports the organization I'm postulating. The second
book, at first glance, looks like Font has already done the
organizational work I need. It is, however, a much slower read.

Even more interesting is that Avigad's Proof Theory course
showed that there are logics of equivalent power but different
levels of _expression_. This seems to me to imply that there is
a form of automated coercion that must exist between various
logics that can be constructed.

Axiom does automatic coercions in its group theory setting.
These really complicate the Type Theory reasoning I'm trying
to use. At the moment I'm quite confused about coercion so
I may have to do a survey paper to try to get a grip on the topic.


On Tue, Dec 12, 2017 at 9:30 AM, Florian Rabe <address@hidden> wrote:
Hi Tim,

I missed you yesterday, but I've added jguidry899 on skype now. 3pm my time usually works.


On 11.12.2017 15:12, Tim Daly wrote:
I tried to Skype but it failed.
I tried to call but it failed.
Lets use email.

I'll write later today.


On Sun, Dec 10, 2017 at 10:13 PM, Tim Daly <address@hidden> wrote:

There is a 6 hour time difference between Pittsburgh and
Berlin. I'll try to skype with you at 3pm your time (9am mine).

I'll be using the skype id jguidry899 as skype doesn't seem
to like any of my prior passwords for my normal id.

If this is not convenient, please let me know.


On Thu, Dec 7, 2017 at 1:51 PM, Florian Rabe <address@hidden>

Yes, I'll be around.

Skype: florian.rabe
WhatsApp/cell phone: +49 1520 5321277

On 07.12.2017 17:47, Tim Daly wrote:

I'm a bit buried at the moment. I printed out your "top 5" papers.
I plan to read them over the weekend so I understand what you're doing.
Are you available some time next week? I have the whole week free.


On Thu, Dec 7, 2017 at 6:53 AM, Florian Rabe <address@hidden
<mailto:address@hidden>> wrote:

    Hi Tim,

    I'm exactly the right person to contact about this.
    I'm CC'ing Michael Kohlhase with whom I ran the LATIN project a few
years ago, whose goal was to form at atlas of logics in this style.

    The logical framework LF was developed for that purpose and my MMT
framework significantly abstracts from and generalizes the LF results.
    You can find the most relevant papers at <>

    We strongly commend any work on Axion that takes these logical
framework ideas into account.
    An integration of our systems (which are good for defining the
logics) with Axiom (which needs to use the logics to verify results) would
be very interesting.

    However, as your second email indicates you have found out already
yourself by now, the problem is quite hard.
    Therefore, depending on your interests and available resources, I
have wildly different advice on how to proceed.
    Maybe we should have a phone call about this?


    On 06.12.2017 14:47, Tim Daly wrote:

        James Davenport suggested I forward this question to you.

        I'm trying to prove Axiom correct. (

        Axiom draws its power from organizing algorithms based on group
        theory, adding propositions as the complexity increases. This
        limit the assumptions needed to provide algorithms.

        Recently I've learned a bit about substructural and (super?)
        logics. So, for example, given the propositions
           (W) Weakening
           (C)  Contraction
           (E)  Exchange
        they can be combined to form (Crary):
             W &  C  &  E ==> Persistant logic.
             W & ~C &  E ==> Affine logic
           ~W &  C  &  E ==> Strict logic
           ~W & ~C &  E ==> Linear logic
             W &   C & ~E ==> ?
             W & ~C & ~E ==> ?
           ~W &   C & ~E ==> ?
           ~W & ~C & ~E ==> Ordered logic

        In addition, there appears to be a group theory-like
organization of
        logics above the substructural e.g. predicate, simply-typed
        and lambda calculus (Avigad).

        Organizing these logics by the gradual introduction of
        and properties would fit exactly into Axiom's structure and make
        proof assumptions clear. I want to organize these in Axiom so the
        proofs inherit the required logic.

        Can you give me any references to a group-theory-like
        of the various logics, similar to the above? I have done a
        search but have not found anything yet.

        Thank you.
        Tim Daly

reply via email to

[Prev in Thread] Current Thread [Next in Thread]