What is the best notion of proof for linear logic seen as the logic of (non commutative) monoidal categories with the two implications.
Dear Cameron,
I'm interested in a linear logic with
finite linear non commutative congiunctions
and left and right implications.
But I'm also interested
in every good notion of proof,
including programs.
Dear Giancarlo,
I guess you are looking for a deductive system (possibly a sequent calculus) whose sound categorical interpretation would be a closed (non-commutative) monoidal category. Or otherwise stated, the so-called "internal language" of a closed (non-commutative) monoidal category. Here "closed" would mean with adjonctions for both the left conjunction functors ( _ and A) and for the right conjunction functors (A and _ ).
Well, I think that should be the Lambek calculus, historically the first substructural logic ever taken into account. It has nothing but a non commutative conjunction and the two possible implications.
Dear Domenico,
thank you for the information
that Lambek sequent calculus
is the first substructural logic
ever taken into account.
I like very much such a calculus
but not for proof theory,
only for the notion of provability.
In proof theory
we have to consider
a very good notion
(and very easy to manipulate)
of equivalent classes of proofs
and sequent calculus,
it seems to me,
is not the best solution.
Then you should have a look at the work of those who have tried to study non-commutative linear logic, and see in particular if they have been able to formalize some good notion of proof nets for non-commutative MLL (which in terms of provability is nothing but the old good Lambek calculus), the fragment of "full non commutative linear logic" without Girard's exponentials. As far as I know, I can name only two persons who have been interested in this: Vito Michele Abrusci and Paul Ruet (the web page of the latter: http://www.pps.univ-paris-diderot.fr/~ruet/ ). Anyway, I doubt they were able to find a satisfactory definition.
Maybe I was too much pessimistic:
http://www.sciencedirect.com/science/article/pii/S0168007299000147
I am interested to know if
some good notion of proof nets
or some good notion of programs
is a elegant solution
MV-algebras and residuated lattices (LL are a case) are all modeled by monoidal closed caetgories. See also my notes:
https://www.researchgate.net/publication/259188590_Algebraic_structures_of_generalized_many-valued_logics?ev=prf_pub
This surely does not answer your question, but there are colleagues who deal with proof theory in this framework.
Data Algebraic structures of generalized many-valued logics
- Badges
- Science topic
- Similar topics
- Computer Science and Engineering
- Programming Languages