×

Connectification for \(n\)-contraction. (English) Zbl 0823.03003

Summary: We introduce connectification operators for intuitionistic and classical linear algebras corresponding to linear logic and to some of its extensions with \(n\)-contraction. In particular, \(n\)-contraction \((n\geq 2)\) is a version of the contraction rule, where \(n+ 1\) occurrences of a formula may be contracted to \(n\) occurrences. Since cut cannot be eliminated from the systems with \(n\)-contraction considered, most of the standard proof-theoretic techniques to investigate meta-properties of those systems are useless. However, by means of connectification we establish the disjunction property for both intuitionistic and classical affine linear logics with \(n\)-contraction.

MSC:

03B20 Subsystems of classical logic (including intuitionistic logic)
03G25 Other algebras related to logic
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Do?en, K., P. Schroeder-Heister (eds.), 1993,Substructural Logics, Studies in Logic and Computation, D. Gabbay (ed.), Clarendon Press, Oxford.
[2] Girard, J. Y., 1987, ?Linear Logic?,Theoretical Computer Science 50.
[3] Hori, R., H. Ono and H. Schellinx, 199x, ?Extending Intuitionistic Linear Logic with Knotted Structural Rules?, to appear inNotre Dame Journal of Formal Logic. · Zbl 0812.03008
[4] Kanazawa, M., 1992, ?The Lambek Calculus Enriched by Additional Connectives?,Journal of Logic, Language and Information (1). · Zbl 0793.03028
[5] Moerdijk, I., 1982, ?Glueing Topoi and Higher Order Disjunction and Existence?,The L. E. J. Brouwer Centenary Symposium, A. S. Troelstra and D. van Dalen (eds), North-Holand. · Zbl 0514.03038
[6] Moerdijk, I., 1983, ?On the Freyd Cover of a Topos?,Notre Dame Journal of Formal Logic, vol.24, num. 4. · Zbl 0487.03034
[7] Prijatelj, A., 1993, ?Bounded Contraction and Many-Valued Semantics?,ILLC Prepublication Series for Mathematical Logic and Foundations ML-93-04, University of Amsterdam.
[8] Prijatelj, A., 1994, ?Free Algebra Corresponding to Multiplicative Classical Linear Logic and some Extensions?,ILLC Prepublication Series for Mathematical Logic and Foundations ML-94-08, University of Amsterdam.
[9] Scedrov, A., P. J. SCOTT, 1982, ?A Note on the Friedman Slash and Freyd Covers?,The L. E. J. Brouwer Centenary Symposium, A. S. Troelstra and D. van Dalen (eds), North-Holand. · Zbl 0529.03039
[10] Smorynski, C. A., 1973, ?Applications of Kripke Models?,Metamathematical Investigations of Intuitionistic Arithmetic and Analysis, A. S. Troelstra (ed), Springer-Verlag, Berlin. · Zbl 0261.02033
[11] Troelstra, A. S., 1992,Lectures on Linear Logic, CSLI Lecture Notes, No. 29, Center for the Study of Language and Information, Stanford. · Zbl 0942.03535
[12] Troelstra, A. S. and D. van Dalen, 1988,Constructivism in Mathematics, vol. I., vol. II, North-Holland Publishing Company, Amsterdam. · Zbl 0661.03047
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.