Abstract
The existence of simple semantics and appropriate cut-free Gentzen-type formulations are fundamental intrinsic criteria for the usefulness of logics. In this paper we show that by using hypersequents (which are multisets of ordinary sequents) we can provide such Gentzen-type systems to many logics. In particular, by using a hypersequential generalization of intuitionistic sequents we can construct cut-free systems for some intermediate logics (including Dummett's LC) which have simple algebraic semantics that suffice, e.g., for decidability. We discuss the possible interpretations of these logics in terms of parallel computation and the role that the usual connectives play in them (which is sometimes different than in the sequential case).
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
A.R. Anderson and N.P. Belnap,Entailment, vol. 1 (Princeton University Press, Princeton, NJ, 1975).
A. Avron, A constructive analysis of RM, J. Symbolic Logic 52 (1987) 939–951.
A. Avron, Natural 3-valued logic: foundations and proof theory, to appear in J. Symbolic Logic.
A. Avron, Simple consequence relations, to appear in Information and Computation.
A. Avron, The semantics and proof theory of linear logic, Theor. Comp. Sci. 57 (1988) 161–184.
A. Avron, Gentzen-type systems, resolution and tableaux, Technical Report 161/90, The Eskenasy Institute of Computer Science, Tel Aviv University, Tel Aviv, Israel.
A. Avron, On an implication connective of RM, Notre Dame J. Formal Logic 27 (1986) 201–209.
R.L. Constable et al.,Implementing Mathematics with the NuPRL Proof Development System (Prentice-Hall, Englewood Cliffs, NJ, 1986).
J.M. Dunn, Relevant logic and entailment, in:Handbook of Philosophical Logic, vol. 3, eds. D. Gabbay and F. Guenthner (Reidel, Dordrecht, Holland; Boston, USA, 1984).
M. Dummett, A propositional calculus with denumerable matrix, J. Symbolic Logic 24 (1959) 96–107.
J.M. Dunn and R.K. Mayer, Algebraic completeness results for Dummett's LC and its extensions, Z. math. Logik und Grundlagen der Mathematik 17 (1971) 225–230.
G. Gentzen, Investigations into logical deduction, in:The Collected Works of Gerhard Gentzen, ed. M.E. Szabo (North-Holland, Amsterdam, 1969).
J.Y. Girard, Linear logic, Theor. Comp. Sci. 50 (1987) 1–101.
K. Gödel, Zum intuitionistishen Aussagenkalküul, Ergeb. Math. Koll. 4 (1933) 34–38.
J.Y. Girard, Y. Lafont and P. Taylor,Proof and Types (Cambridge University Press, 1989).
G. Huet, Deduction and computation, in:Fundamentals of Artificial Intelligence, eds. W. Bibel and K. Jorrand, Lecture Notes in Computer Science (Springer, 1986).
R. Milner,Communication and Concurrency (Prentice-Hall, 1989).
B. Nordström, K. Peterson and J. Smith, Programming in Martin-Löf's type theory, preprint, University of Göteborg, Sweden (Midsummer 1988).
G. Pottinger, Uniform, cut-free formulations of T, S4 and S5, (abstract), J. Symbolic Logic 48 (1983) 900.
D. Prawitz,Natural Deduction — A Proof-theoretical Study (Almquist and Wiksell, Stockholm, 1965).
O. Sonobo, A. Gentzen-type formulation of some intermediate propositional logics, J. Tsuda College 7 (1975) 7–14.
A. Urquhart, Many-valued logic, in:Handbook of Philosophical Logic, vol. 3, eds. D. Gabbay and F. Guenthner (Reidel, Dordrecht, Holland; Boston, USA, 1984).
A. Visser, On the completeness principle: A study of provability in Heyting's arithmetic, Ann. Math. Logic 22 (1982) 263–295.
J. Zucker, The correspondence between cut-elimination and normalization, Ann. Math. Logic 7 (1974) 1–112.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Avron, A. Hypersequents, logical consequence and intermediate logics for concurrency. Ann Math Artif Intell 4, 225–248 (1991). https://doi.org/10.1007/BF01531058
Issue Date:
DOI: https://doi.org/10.1007/BF01531058