This paper presents an overview of the methods of hypersequents and display sequents in the proof theory of non-classical logics. In contrast with existing surveys dedicated to hypersequent calculi or to display calculi, our aim is to provide a unified perspective on these two formalisms highlighting their differences and similarities and discussing applications and recent results connecting and comparing them.

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.

We perform a proof-theoretical investigation of two modal predicate logics: global intuitionistic logic GI and global intuitionistic fuzzy logic GIF. These logics were introduced by Takeuti and Titani to formulate an intuitionistic set theory and an intuitionistic fuzzy set theory together with their metatheories. Here we define analytic Gentzen style calculi for GI and GIF. Among other things, these calculi allows one to prove Herbrand’s theorem for suitable fragments of GI and GIF.

It is shown that Gqp↑, the quantified propositional Gödel logic based on the truth-value set V↑ = {1 - 1/n : n≥1}∪{1}, is decidable. This result is obtained by reduction to Büchi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of Gqp↑ as the intersection of all finite-valued quantified propositional Gödel logics.

The Mīmā ṃ sā school of Indian philosophy elaborated complex ways of interpreting the prescriptive portions of the Vedic sacred texts. The present article is the result of the collaboration of a group of scholars of logic, computer science, European philosophy and Indian philosophy and aims at the individuation and analysis of the deontic system which is applied but never explicitly discussed in Mīmā ṃ sā texts. The article outlines the basic distinction between three sorts of principles —hermeneutic, linguistic and (...) deontic. It proposes a mathematical formalization of the deontic principles and uses it to discuss a well-known example of seemingly conflicting statements, namely the prescription to undertake the malefic Śyena sacrifice and the prohibition to perform any harm. (shrink)

In this paper we deepen Mundici's analysis on reducibility of the decision problem from infinite-valued ukasiewicz logic to a suitable m-valued ukasiewicz logic m , where m only depends on the length of the formulas to be proved. Using geometrical arguments we find a better upper bound for the least integer m such that a formula is valid in if and only if it is also valid in m. We also reduce the notion of logical consequence in to the same (...) notion in a suitable finite set of finite-valued ukasiewicz logics. Finally, we define an analytic and internal sequent calculus for infinite-valued ukasiewicz logic. (shrink)

A Partial Combinatory Algebra is completable if it can be extended to a total one. In [1] it is asked (question 11, posed by D. Scott, H. Barendregt, and G. Mitschke) if every PCA can be completed. A negative answer to this question was given by Klop in [12, 11]; moreover he provided a sufficient condition for completability of a PCA (M, ·, K, S) in the form of ten axioms (inequalities) on terms of M. We prove that just one (...) of these axiom (the so called Barendregt's axiom) is sufficient to guarantee (a slightly weaker notion of) completability. (shrink)

Over the course of more than two millennia the philosophical school of Mīmāṃsā has thoroughly analyzed normative statements. In this paper we approach a formalization of the deontic system which is applied but never explicitly discussed in Mīmāṃsā to resolve conflicts between deontic statements by giving preference to the more specific ones. We first extend with prohibitions and recommendations the non-normal deontic logic extracted in Ciabattoni et al. from Mīmāṃsā texts, obtaining a multimodal dyadic version of the deontic logic \. (...) Sequent calculus is then used to close a set of prima-facie injunctions under a restricted form of monotonicity, using specificity to avoid conflicts. We establish decidability and complexity results, and investigate the potential use of the resulting system for Mīmāṃsā philosophy and, more generally, for the formal interpretation of normative statements. (shrink)