Abstract We present a sequent calculus for Scott’s theory of classes founded on positive free logic. Cut elimination, the generalised subformula property and consistency are shown to hold, also in the intuitionistic variant. Eventually the calculus is extended to cover the original Zermelo’s set theory Z without the axiom of choice by means of (systems of) rules. The calculus for Z preserves cut elimination, moreover, some of its subsystems and extensions are also provably consistent.

Abstract We present a sequent calculus GNFL for negative free logic with definite descriptions in the classical and intuitionistic versions, with empty and nonempty domains. It is shown constructively that GNFL satisfies the cut elimination theorem and its cut-free version satisfies the subformula property.

Abstract We present a uniform characterisation of three-valued logics by means of bisequent calculus (BSC). It is a generalised form of sequent calculus (SC) where rules operate on the ordered pairs of ordinary sequents. BSC may be treated as the weakest kind of system in the rich family of generalised SC operating on items being some collections of ordinary sequents. This family covers several forms of hypersequent and nested sequent calculi introduced to provide decent SC for several non-classical logics. It seems that for many non-classical logics, including some many-valued, paraconsistent and modal logics, this reasonably modest generalization of standard SC is sufficient. In this paper we examine a variety of three-valued logics and show how they can be formalised in the framework of bisequent calculus. All provided systems are cut-free and satisfy the subformula property. Also the interpolation theorem is constructively proved for some logics.

Abstract Term-forming operators (tfos), like iota- or epsilon-operator, are technical devices applied to build complex terms in formal languages. Although they are very useful in practice their theory is not well developed. In the paper we provide a proof-theoretic formulation of the general approach to tfos provided independently by several authors like Scott, Hatcher, Corcoran, and compare it with an approach proposed later by Tennant. Eventually it is shown how the general theory can be applied to specific areas like Quine’s set theory NF.

Abstract We present a sequent calculus for first-order logic with lambda terms and definite descriptions. The theory formalised by this calculus is essentially Russellian, but avoids some of its well known drawbacks and treats definite description as genuine terms. A constructive proof of the cut elimination theorem and a Henkin-style proof of completeness are the main results of this contribution.

Abstract We present a uniform syntactical characterisation of the class of quasi-relevant logics which are four-valued extensions of the basic relevant logic B of Meyer and Routley. All these logics are obtained by the addition of suitable quasi-relevant implications to the four-valued logic of First Degree Entailment FDE. So far they were characterised axiomatically and semantically in several ways but did not obtain a special proof-theoretic treatment. To this aim a generalised form of sequent calculus called bisequent calculus (BSC) is applied. In BSC rules operate on the ordered pairs of ordinary sequents. It may be treated as the weakest kind of system in the rich family of generalised sequent calculi operating on items which are some collections of ordinary sequents, like hypersequents or nested sequents. It is shown that all logics under consideration have cut-free characterisation in BSC which satisfies the subformula property and yields decidability. It is also shown that the interpolation theorem holds for these logics if their language is enriched with additional negation.