Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts

This paper is about non-labelled proof-systems for hybrid logic, that is, proof-systems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that non-labelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations.

Sequent Systems without Improper Derivations

In the natural deduction system for classical propositional logic given by G. Gentzen, there are some inference rules with assumptions discharged by the rule. D. Prawitz calls such inference rules improper, and others proper. Improper inference rules are more complicated and are often harder to understand than the proper ones. In the present paper, we distinguish between proper and improper derivations by using sequent systems. Specifically, we introduce a sequent system \(\vdash_{\bf Sc}\) for classical propositional logic with only structural rules, and prove that \(\vdash_{\bf Sc}\) does not allow improper derivations in general. For instance, the sequent \(\Rightarrow p \to q\) cannot be derived from the sequent \(p \Rightarrow q\) in \(\vdash_{\bf Sc}\). In order to prove the failure of improper derivations, we modify the usual notion of truth valuation, and using the modified valuation, we prove the completeness of \(\vdash_{\bf Sc}\). We also consider whether an improper derivation can be described generally by using \(\vdash_{\bf Sc}\).

ON NON-MONOTONOUS PROPERTIES OF SOME CLASSICAL AND NONCLASSICAL PROPOSITIONAL PROOF SYSTEMS

We investigate the relations between the proof lines of non-minimal tautologies and its minimal tautologies for the Frege systems, the sequent systems with cut rule and the systems of natural deductions of classical and nonclassical logics. We show that for these systems there are sequences of tautologies ψn, every one of which has unique minimal tautologies φn such that for each n the minimal proof lines of φn are an order more than the minimal proof lines of ψn.

One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity

Bilinear Logic of Lambek [10] amounts to Noncommutative MALL of Abrusci [1]. Lambek [10] proves the cut–elimination theorem for a onesided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek [10], we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTIME complexity of the multiplicative fragment of NBL.

On the Numbers of Minimal Tautologies and Properties of Their Proofs in Classical and Nonclassical Logic

It is proved in this paper that the number of minimal tautologies for any given logic tautology of size п can be an exponential function in п, and it is also proved that for every tautology of the given logic there is some minimal tautology such that the number of its sequential form proof steps is equal to minimal steps in the proof of sequential form for the given tautology in cut-free sequent systems for classical, intuitionistic, Joganssons and monotone logics.

Functional Completeness in CPL via Correspondence Analysis

Kooi and Tamminga's correspondence analysis is a technique for designing proof systems, mostly, natural deduction and sequent systems. In this paper it is used to generate sequent calculi with invertible rules, whose only branching rule is the rule of cut. The calculi pertain to classical propositional logic and any of its fragments that may be obtained from adding a set (sets) of rules characterizing a two-argument Boolean function(s) to the negation fragment of classical propositional logic. The properties of soundness and completeness of the calculi are demonstrated. The proof of completeness is conducted by Kalmár's method. Most of the presented sequent-calculus rules have been obtained automatically, by a rule-generating algorithm implemented in Python. Correctness of the algorithm is demonstrated. This automated approach allowed us to analyse thousands of possible rules' schemes, hundreds of rules corresponding to Boolean functions, and to nd dozens of those invertible. Interestingly, the analysis revealed that the presented proof-theoretic framework provides a syntactic characteristics of such an important semantic property as functional completeness.