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.

Axiomatization of Some Basic and Modal Boolean Connexive Logics

Boolean connexive logic is an extension of Boolean logic that is closed under Modus Ponens and contains Aristotle’s and Boethius’ theses. According to these theses (i) a sentence cannot imply its negation and the negation of a sentence cannot imply the sentence; and (ii) if the antecedent implies the consequent, then the antecedent cannot imply the negation of the consequent and if the antecedent implies the negation of the consequent, then the antecedent cannot imply the consequent. Such a logic was first introduced by Jarmużek and Malinowski, by means of so-called relating semantics and tableau systems. Subsequently its modal extension was determined by means of the combination of possible-worlds semantics and relating semantics. In the following article we present axiomatic systems of some basic and modal Boolean connexive logics. Proofs of completeness will be carried out using canonical models defined with respect to maximal consistent sets.

Tableau Systems for Epistemic Positional Logics

The goal of the article is twofold. The first one is to provide logics basedon positional semantics which will be suitable for the analysis of epistemic modalitiessuch as ‘agent ... knows/beliefs that ...’. The second one is to define tableau systemsfor such logics. Firstly, we present the minimal positional logic MR. Then, we changethe notion of formulas and semantics in order to consider iterations of the operatorof realization and “free” classical formulas. After that, we move on to weaker logicsin order to avoid the well known problem of logical omniscience. At the same time,we keep the positional counterparts of modal axioms (T), (4) and (5). For all of theconsidered logics we present sound and complete tableau systems.

Boulesic-Doxastic Logic

In this paper, I will develop a set of boulesic-doxastic tableau systems and prove that they are sound and complete. Boulesic-doxastic logic consists of two main parts: a boulesic part and a doxastic part. By ‘boulesic logic’ I mean ‘the logic of the will’, and by ‘doxastic logic’ I mean ‘the logic of belief’. The first part deals with ‘boulesic’ concepts, expressions, sentences, arguments and theorems. I will concentrate on two types of boulesic expression: ‘individual x wants it to be the case that’ and ‘individual x accepts that it is the case that’. The second part deals with ‘doxastic’ concepts, expressions, sentences, arguments and theorems. I will concentrate on two types of doxastic expression: ‘individual x believes that’ and ‘it is imaginable to individual x that’. Boulesic-doxastic logic investigates how these concepts are related to each other. Boulesic logic is a new kind of logic. Doxastic logic has been around for a while, but the approach to this branch of logic in this paper is new. Each system is combined with modal logic with two kinds of modal operators for historical and absolute necessity and predicate logic with necessary identity and ‘possibilist’ quantifiers. I use a kind of possible world semantics to describe the systems semantically. I also sketch out how our basic language can be extended with propositional quantifiers. All the systems developed in this paper are new.

Natural deduction, tableau and sequent systems

Different presentations of the principles of logic reflect different approaches to the subject itself. The three kinds of system discussed here treat as fundamental not logical truth, but consequence, the relation holding between the premises and conclusion of a valid argument. They are, however, inspired by different conceptions of this relation. Natural deduction rules are intended to formalize the way in which mathematicians actually reason in their proofs. Tableau systems reflect the semantic conception of consequence; their rules may be interpreted as the systematic search for a counterexample to an argument. Finally, sequent calculi were developed for the sake of their metamathematical properties. All three systems employ rules rather than axioms. Each logical constant is governed by a pair of rules which do not involve the other constants and are, in some sense, inverse. Take the implication operator ‘→’, for example. In natural deduction, there is an introduction rule for ‘→’ which gives a sufficient condition for inferring an implication, and an elimination rule which gives the strongest conclusion that can be inferred from a premise having the form of an implication. Tableau systems contain a rule which gives a sufficient condition for an implication to be true, and another which gives a sufficient condition for it to be false. A sequent is an array Γ⊢Δ, where Γ and Δ are lists (or sets) of formulas. Sequent calculi have rules for introducing implication on the left of the ‘⊢’ symbol and on the right. The construction of derivations or tableaus in these systems is often more concise and intuitive than in an axiomatic one, and versions of all three have found their way into introductory logic texts. Furthermore, every natural deduction or sequent derivation can be made more direct by transforming it into a ‘normal form’. In the case of the sequent calculus, this result is known as the cut-elimination theorem. It has been applied extensively in metamathematics, most famously to obtain consistency proofs. The semantic inspiration for the rules of tableau construction suggests a very perspicuous proof of classical completeness, one which can also be adapted to the sequent calculus. The introduction and elimination rules of natural deduction are intuitionistically valid and have suggested an alternative semantics based on a conception of meaning as use. The idea is that the meaning of each logical constant is exhausted by its inferential behaviour and can therefore be characterized by its introduction and elimination rules. Although the discussion below focuses on intuitionistic and classical first-order logic, various other logics have also been formulated as sequent, natural deduction and even tableau systems: modal logics, for example, relevance logic, infinitary and higher-order logics. There is a gain in understanding the role of the logical constants which comes from formulating introduction and elimination (or left and right) rules for them. Some authors have even suggested that one must be able to do so for an operator to count as logical.