Proof Compression and NP Versus PSPACE II: Addendum

In [3] we proved the conjecture NP = PSPACE by advanced proof theoretic methods that combined Hudelmaier's cut-free sequent calculus for minimal logic (HSC) [5] with the horizontal compressing in the corresponding minimal Prawitz-style natural deduction (ND) [6]. In this Addendum we show how to prove a weaker result NP = coNP without referring to HSC. The underlying idea (due to the second author) is to omit full minimal logic and compress only \naive" normal tree-like ND refutations of the existence of Hamiltonian cycles in given non-Hamiltonian graphs, since the Hamiltonian graph problem in NP-complete. Thus, loosely speaking, the proof of NP = coNP can be obtained by HSC-elimination from our proof of NP = PSPACE [3].

Higher-level Inferences in the Strong-Kleene Setting: A Proof-theoretic Approach

Building on early work by Girard (1987) and using closely related techniques from the proof theory of many-valued logics, we propose a sequent calculus capturing a hierarchy of notions of satisfaction based on the Strong Kleene matrices introduced by Barrio et al. (Journal of Philosophical Logic 49:93–120, 2020) and others. The calculus allows one to establish and generalize in a very natural manner several recent results, such as the coincidence of some of these notions with their classical counterparts, and the possibility of expressing some notions of satisfaction for higher-level inferences using notions of satisfaction for inferences of lower level. We also show that at each level all notions of satisfaction considered are pairwise distinct and we address some remarks on the possible significance of this (huge) number of notions of consequence.

A focused linear logical framework and its application to metatheory of object logics

Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks, and models for concurrency. LL’s cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. This paper formalizes the proof of cut-elimination for focused LL. For that, we propose a set of five cut-rules that allows us to prove cut-elimination directly on the focused system. We also encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have cut-elimination. We then obtain, for free, cut-elimination for first-order classical, intuitionistic, and variants of LL. We also use the LL metatheory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. Hence, we propose a framework that can be used to formalize fundamental properties of logical systems specified as LL theories.

Sequent Calculi for Orthologic with Strict Implication

In this study, new sequent calculi for a minimal quantum logic (\(\bf MQL\)) are discussed that involve an implication. The sequent calculus \(\bf GO\) for \(\bf MQL\) was established by Nishimura, and it is complete with respect to ortho-models (O-models). As \(\bf GO\) does not contain implications, this study adopts the strict implication and constructs two new sequent calculi \(\mathbf{GOI}_1\) and \(\mathbf{GOI}_2\) as the expansions of \(\bf GO\). Both \(\mathbf{GOI}_1\) and \(\mathbf{GOI}_2\) are complete with respect to the O-models. In this study, the completeness and decidability theorems for these new systems are proven. Furthermore, some details pertaining to new rules and the strict implication are discussed.

Metasequents and Tetravaluations

In this paper we treat metasequents—objects which stand to sequents as sequents stand to formulas—as first class logical citizens. To this end we provide a metasequent calculus, a sequent calculus which allows us to directly manipulate metasequents. We show that the various metasequent calculi we consider are sound and complete w.r.t. appropriate classes of tetravaluations where validity is understood locally. Finally we use our metasequent calculus to give direct syntactic proofs of various collapse results, closing a problem left open in French (Ergo, 3(5), 113–131 2016).

A Binary Quantifier for Definite Descriptions for Cut Free Free Logics

This paper presents rules in sequent calculus for a binary quantifier I to formalise definite descriptions: Ix[F, G] means ‘The F is G’. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of I. There are also brief comparisons of the present approach to the more common one that formalises definite descriptions with a term forming operator. In the final section rules for I for negative free and classical logic are also mentioned.

The consistency of arithmetic

This chapter opens the part of the book that deals with ordinal proof theory. Here the systems of interest are not purely logical ones, but rather formalized versions of mathematical theories, and in particular the first-order version of classical arithmetic built on top of the sequent calculus. Classical arithmetic goes beyond pure logic in that it contains a number of specific axioms for, among other symbols, 0 and the successor function. In particular, it contains the rule of induction, which is the essential rule characterizing the natural numbers. Proving a cut-elimination theorem for this system is hopeless, but something analogous to the cut-elimination theorem can be obtained. Indeed, one can show that every proof of a sequent containing only atomic formulas can be transformed into a proof that only applies the cut rule to atomic formulas. Such proofs, which do not make use of the induction rule and which only concern sequents consisting of atomic formulas, are called simple. It is shown that simple proofs cannot be proofs of the empty sequent, i.e., of a contradiction. The process of transforming the original proof into a simple proof is quite involved and requires the successive elimination, among other things, of “complex” cuts and applications of the rules of induction. The chapter describes in some detail how this transformation works, working through a number of illustrative examples. However, the transformation on its own does not guarantee that the process will eventually terminate in a simple proof.

Alternative Axiomatization for Logics of Agency in a G3 Calculus

In a recent paper, Negri and Pavlović (Studia Logica 1–35, 2020) have formulated a decidable sequent calculus for the logic of agency, specifically for a deliberative see-to-it-that modality, or dstit. In that paper the adequacy of the system is demonstrated by showing the derivability of the axiomatization of dstit from Belnap et al. (Facing the future: agents and choices in our indeterminist world. Oxford University Press, Oxford, 2001). And while the influence of the latter book on the study of logics of agency cannot be overstated, we note that this is not the only axiomatization of that modality available. In fact, an earlier (and arguably purer) one was offered in Xu (J Philosophical Logic 27(5):505–552, 1998). In this article we fill this lacuna by proving that this alternative axiomatization is likewise readily derivable in the system of Negri and Pavlović (Studia Logica 1–35, 2020).

Efficient loop-check for multimodal KD45n logic

We introduce sequent calculus for multi-modal logic KD45n which uses efficient loop-check. Efficiency of the used loop-check is obtained by using marked modal operator squarei which is used as an alternative to sequent with histories ([2,3]).We use inference rules with or branches to make all rules invertible or semi-invertible. We showthe maximum height of the constructed derivation tree. Also polynomial space complexity is proved.

On Polymorphic Sessions and Functions

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.