What's the core of an inference system?

Kai Brünnler <[email protected]>
Newsgroups gmane.science.mathematics.frogs
Message-ID <[email protected]>
Hello Frogs,

so far, we informally defined the core of an inference system as the set 
of those of its inference rules that are needed in order to reduce both 
the cut as well as identity to atomic form. (That's not yet a formal 
definition, for example there could be two different ways to do this 
reduction, but this has never happened for any of our systems.) Atomic 
cut and identity were not included in this definition of core.

I noticed that it would be elegant to include atomic cut and atomic 
identity in the definition of core, because then cut = core-up rather 
than cut = core-up + atomic cut. Several lemmas, e.g. the replacement of 
a rule by its dual+core, become more succinct.

On a more conceptual level, I also like the idea of being able to derive 
cut and identity in the core, which is impossible with the current 
notion of core. Every system of inference rules that I know and that I'd 
call "logical" has some form of an identity axiom and some form of cut. 
To me, reflexivity and transitivity are a minimum requirement for a 
logical cosequence relation. Don't they fully deserve to be part of 
whatever it will be that we call "the core"?

I'd like to include atomic cut/identity in the core. I'm looking for 
arguments against doing so.

Peace!

-Kai
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.