I'm tryin=
g to prove Axiom correct.

Axiom draws its power from organizin=
g algorithms based on group=
=C2=A0=C2=A0=C2=A0=C2=A0 W & ~C &=C2=A0 E =3D=3D> Affine logic <=
br>

=C2=A0=C2=A0 ~W &=C2=A0 C=C2=A0 &=C2=A0 E =3D=3D> Stric=
t logic =

Organizing t=
hese logics by the gradual introduction of propositions

and p=
roperties would fit exactly into Axiom's structure and make

proofs inherit the required logic.

Thank you.

--f403043862789ee5c0055fa8450b--
From MAILER-DAEMON Wed Dec 13 11:36:24 2017
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1ePA1A-0001jZ-NT
for mharc-axiom-developer@gnu.org; Wed, 13 Dec 2017 11:36:24 -0500
Received: from eggs.gnu.org ([2001:4830:134:3::10]:55367)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from Tim Daly

Florian,

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

signatures and "domains" which are implementations of

=

I'=
m part way through the first book and it looks like it signatures.

So in Axiom you start with Set =
or Type and then define

things like Group (which requires more si=
ngatures), Rings,

(more required signatures), Fields (e.g. a divi=
sion signature).

Once the tower of categories exis=
ts you can define a

domain that inherits from some (sub-)tow=
er. 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 (unreason=
able 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 sta=
rt a root category

with a "reflexive signature" A |- A<=
/div>

Then a set of categories can be defined, one each,=
to allow

structural rules like Weakening which you might or migh=
t not

allow.

Then a set of categories wi=
th 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 LinearLogi=
c, OrderedLogic,=C2=A0 or a Gentzen

domain that inherits onl=
y the categories that apply.

Clearly Halleck's=
work

http://www.cc.utah.edu/~nahaj/logic/structures/index.htmlto really cover all of logic. But for a reasonable subset such

both supports this idea and shows that it is too simplistic

as I will need while proving Axiom it seems that the naive

organ=
ization might be sufficient.

Just after our attempted phone call two books showed up

"An Introduction to Substructural Logics" and

"A=
bstract Algeraic Logic: An Introductory Textbook"."An Introduction to Substructural Logics" and

=

Even more interesting is that Avigad's Proof Theory cour=
se

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

<=
div>logics that can be constructed. Axiom doe=
s automatic coercions in its group theory setting.

These really c=
omplicate 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.

Tim

On Tue, Dec 1=
2, 2017 at 9:30 AM, Florian Rabe <florian.rabe@gmail.com> wrote:

Hi Tim,

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

Best,

Florian

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.

Tim

On Sun, Dec 10, 2017 at 10:13 PM, Tim Daly <axiomcas@gmail.com> 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.

Tim

On Thu, Dec 7, 2017 at 1:51 PM, Florian Rabe <florian.rabe@gmail.com>

wrote:

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" pa= pers.

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.

Tim

On Thu, Dec 7, 2017 at 6:53 AM, Florian Rabe <florian.rabe@gmail.com

<mailto:flor= ian.rabe@gmail.com>> wrote:

=C2=A0 =C2=A0 Hi Tim,

=C2=A0 =C2=A0 I'm exactly the right person to contact about this.

=C2=A0 =C2=A0 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.

=C2=A0 =C2=A0 The logical framework LF was developed for that purpose and m= y MMT

framework significantly abstracts from and generalizes the LF results.

=C2=A0 =C2=A0 You can find the most relevant papers at

https://uniformal.github.io/doc/philosoph= y/papers.html <

https://uniformal.github.io/doc/philosoph= y/papers.html >

=C2=A0 =C2=A0 We strongly commend any work on Axion that takes these logica= l

framework ideas into account.

=C2=A0 =C2=A0 An integration of our systems (which are good for defining th= e

logics) with Axiom (which needs to use the logics to verify results) would<= br> be very interesting.

=C2=A0 =C2=A0 However, as your second email indicates you have found out al= ready

yourself by now, the problem is quite hard.

=C2=A0 =C2=A0 Therefore, depending on your interests and available resource= s, I

have wildly different advice on how to proceed.

=C2=A0 =C2=A0 Maybe we should have a phone call about this?

=C2=A0 =C2=A0 Best,

=C2=A0 =C2=A0 Florian

=C2=A0 =C2=A0 On 06.12.2017 14:47, Tim Daly wrote:

=C2=A0 =C2=A0 =C2=A0 =C2=A0 James Davenport suggested I forward this questi= on to you.

=C2=A0 =C2=A0 =C2=A0 =C2=A0 ...

=C2=A0 =C2=A0 =C2=A0 =C2=A0 I'm trying to prove Axiom correct. (http:/= /axiom-developer.org)

=C2=A0 =C2=A0 =C2=A0 =C2=A0 Axiom draws its power from organizing algorithm= s based on group

=C2=A0 =C2=A0 =C2=A0 =C2=A0 theory, adding propositions as the complexity i= ncreases. This

helps

=C2=A0 =C2=A0 =C2=A0 =C2=A0 limit the assumptions needed to provide algorit= hms.

=C2=A0 =C2=A0 =C2=A0 =C2=A0 Recently I've learned a bit about substruct= ural and (super?)

structural

=C2=A0 =C2=A0 =C2=A0 =C2=A0 logics. So, for example, given the propositions=

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(W) Weakening

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(C)=C2=A0 Contraction

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(E)=C2=A0 Exchange

=C2=A0 =C2=A0 =C2=A0 =C2=A0 they can be combined to form (Crary):

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0W &=C2=A0 C=C2=A0 &= =C2=A0 E =3D=3D> Persistant logic.

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0W & ~C &=C2=A0 E = =3D=3D> Affine logic

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0~W &=C2=A0 C=C2=A0 &=C2=A0= E =3D=3D> Strict logic

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0~W & ~C &=C2=A0 E =3D=3D&g= t; Linear logic

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0W &=C2=A0 =C2=A0C &= ~E =3D=3D> ?

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0W & ~C & ~E =3D=3D&= gt; ?

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0~W &=C2=A0 =C2=A0C & ~E = =3D=3D> ?

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0~W & ~C & ~E =3D=3D> Or= dered logic

=C2=A0 =C2=A0 =C2=A0 =C2=A0 In addition, there appears to be a group theory= -like

organization of

=C2=A0 =C2=A0 =C2=A0 =C2=A0 logics above the substructural e.g. predicate, = simply-typed

lambda,

=C2=A0 =C2=A0 =C2=A0 =C2=A0 and lambda calculus (Avigad).

=C2=A0 =C2=A0 =C2=A0 =C2=A0 Organizing these logics by the gradual introduc= tion of

propositions

=C2=A0 =C2=A0 =C2=A0 =C2=A0 and properties would fit exactly into Axiom'= ;s structure and make

=C2=A0 =C2=A0 =C2=A0 =C2=A0 proof assumptions clear. I want to organize the= se in Axiom so the

=C2=A0 =C2=A0 =C2=A0 =C2=A0 proofs inherit the required logic.

=C2=A0 =C2=A0 =C2=A0 =C2=A0 Can you give me any references to a group-theor= y-like

organization

=C2=A0 =C2=A0 =C2=A0 =C2=A0 of the various logics, similar to the above? I = have done a

literature

=C2=A0 =C2=A0 =C2=A0 =C2=A0 search but have not found anything yet.

=C2=A0 =C2=A0 =C2=A0 =C2=A0 Thank you.

=C2=A0 =C2=A0 =C2=A0 =C2=A0 Tim Daly