Basic logic: reflection, symmetry, visibility
- 1 September 2000
- journal article
- Published by Cambridge University Press (CUP) in The Journal of Symbolic Logic
- Vol. 65 (3) , 979-1013
- https://doi.org/10.2307/2586685
Abstract
We introduce a sequent calculusBfor a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic. quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterizeBpositively: reflection, symmetry and visibility.A logical constant obeys to the principle of reflection if it is characterized semantically by an equation binding it with a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection.To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube.Keywords
This publication has 9 references indexed in Scilit:
- Labelled Deductive SystemsPublished by Elsevier ,2003
- Twenty Five Years of Constructive Type TheoryPublished by Oxford University Press (OUP) ,1998
- From Basic Logic to Quantum Logics with Cut-EliminationInternational Journal of Theoretical Physics, 1998
- Labelled Deductive SystemsPublished by Oxford University Press (OUP) ,1996
- On the unity of logicAnnals of Pure and Applied Logic, 1993
- Jean-Yves Girard. Proof theory and logical complexity. Volume I. Studies in proof theory, no. 1. Bibliopolis, Naples 1987, also distributed by Humanities Press, Atlantic Highlands, N.J., 503 pp.The Journal of Symbolic Logic, 1989
- Logical constants as punctuation marks.Notre Dame Journal of Formal Logic, 1989
- Linear logicTheoretical Computer Science, 1987
- Display logicJournal of Philosophical Logic, 1982