FROM BASIC LOGIC TO QUANTUM LOGIC WITH CUT-ELIMINATION

The results presented in this paper were obtained in the framework of basic logic, a new logic aiming at the unification of several logical systems. The first result is a sequent formulation for orthologic whic h allows the use of methods of proof theory in quantum logic. Such a f ormulation admits a very simple procedure of cut-elimination and hence , because of the subformula property, also a method of proof search an d an effective decision procedure. By using the framework of basic log ic, we also obtain a cut-free formulation for orthologic with implicat ion, for linear orthologic, and, more in generally for a wide range of new quantum-like logics. These logics meet some requirements expresse d by physicists and computer scientists. In particular, we propose a g ood candidate for a linear quantum logic with implication.