Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are (...) notational variants of each other, roughly in the same way that tableaus and Gentzen sequent calculi are notational variants. This immediately gives rise to new modal nested sequent systems which may be of independent interest. We discuss some of these, including those for some justification logics that include standard modal operators. (shrink)

Gödel's modal ontological argument is the centerpiece of an extensive examination of intensional logic. First, classical type theory is presented semantically, tableau rules for it are introduced, and the Prawitz/Takahashi completeness proof is given. Then modal machinery is added to produce a modified version of Montague/Gallin intensional logic. Finally, various ontological proofs for the existence of God are discussed informally, and the Gödel argument is fully formalized. Parts of the book are mathematical, parts philosophical.

We continue a series of papers on a family of many-valued modal logics, a family whose Kripke semantics involves many-valued accessibility relations. Earlier papers in the series presented a motivation in terms of a multiple-expert semantics. They also proved completeness of sequent calculus formulations for the logics, formulations using a cut rule in an essential way. In this paper a novel cut-free tableau formulation is presented, and its completeness is proved.

We present a logic programming language, which we call Proflog, with an operational semantics based on tableaus, and a denotational semantics based on supervaluations. We show the two agree. Negation is well-behaved, and semantic non-computability issues do not arise. This is accomplished essentially by dropping a domain closure requirement. The cost is that intuitions developed through the use of classical logic may need modification, though the system is still classical at a level once removed. Implementation problems are discussed very (...) briefly — the thrust of the paper is primarily theoretical. (shrink)

Gentzen’s singular sequential system of first-order logic was an alternative notation for his system of natural deductions. His multiple sequential system was his symmetric generalization that was more appropriate to classical logic. Beth’s tableaus system was a system that was derived directly from the semantic analysis of connectives and quantifiers. It was soon realized that the Beth’s system and the Gentzen’s multiple system were only notational variants of each other. Kneale’s system of multiple natural deductions was a generalization of (...) Gentzen’s system of natural deductions. We prove that Kneale’s natural deductions are also a notational variant of Beth’s tableaus. (shrink)

We present the design goals and metatheory of the Monadic Hybrid Calculus, a new formal system that has the same power as the Monadic Predicate Calculus. MHC allows quantification, including relative quantification, in a straightforward way without the use of bound variables, using a simple adaptation of modal logic notation. Thus “all Greeks are mortal” can be written as [G]M. MHC is also ‘hybrid’ in that it has individual constants, which allow us to formulate statements about particular individuals. Thus “Socrates (...) is Athenian and mortal” can be formalised as s.For our proof system, we use a simple adaptation of Beth-style tableaus. The availability of individual constants eliminates the need for labelled deduction.We discuss first the pragmatic and pedagogical advantages of MHC. Then we present the metatheory: formal syntax, semantics, proof rules, soundness, completeness and expressive equivalence with the Monadic Predicate Calculus. (shrink)

This text describes a single engraving of the picture encyclopediaBilder-Akademie für die Jugend published from 1780 to 1784. It consisted of 52 picture tableaus, each with nine images that were connected through the biblical topic. The particular image under examination, the “Table 38”, shows the healing wonders of Christ, the electrifying maschine, a healing physician and the structure of ear and eye. Goal of this text will be to describe the different connections and meanings of these depicted scenes, as (...) in the same time I will argue, that pictures can not only be interpreted by understanding how people looked at them, but also to take into question what people did with them. (shrink)

The article deals with an object which has hitherto been overlooked, but which was essential to Aby Warburg’s work: the desk. While in a first step sources are collected from and about Warburg, which emphasize the significance of the desk for Warburg’s work, a second step is taken to reconstruct a specific type of desk that was of great importance to Warburg. From the identification of this work table the thesis is derived that this table played a decisive role in (...) the formation of the tableaus of the Mnemosyne Atlas. (shrink)

This text describes a single engraving of the picture encyclopediaBilder-Akademie für die Jugend published from 1780 to 1784. It consisted of 52 picture tableaus, each with nine images that were connected through the biblical topic. The particular image under examination, the “Table 38”, shows the healing wonders of Christ, the electrifying maschine, a healing physician and the structure of ear and eye. Goal of this text will be to describe the different connections and meanings of these depicted scenes, as (...) in the same time I will argue, that pictures can not only be interpreted by understanding how people looked at them, but also to take into question what people did with them. (shrink)

This text describes a single engraving of the picture encyclopediaBilder-Akademie für die Jugend published from 1780 to 1784. It consisted of 52 picture tableaus, each with nine images that were connected through the biblical topic. The particular image under examination, the “Table 38”, shows the healing wonders of Christ, the electrifying maschine, a healing physician and the structure of ear and eye. Goal of this text will be to describe the different connections and meanings of these depicted scenes, as (...) in the same time I will argue, that pictures can not only be interpreted by understanding how people looked at them, but also to take into question what people did with them. (shrink)

. I give a systematic presentation of a fairly large family of multiple-conclusion modal logics that are paraconsistent and/or paracomplete. After providing motivation for studying such systems, I present semantics and tableau-style proof theories for them. The proof theories are shown to be sound and complete with respect to the semantics. I then show how the “standard” systems of classical, single-conclusion modal logics fit into the framework constructed.

First-order modal logic, in the usual formulations, is not suf- ficiently expressive, and as a consequence problems like Frege’s morning star/evening star puzzle arise. The introduction of predicate abstraction machinery provides a natural extension in which such difficulties can be addressed. But this machinery can also be thought of as part of a move to a full higher-order modal logic. In this paper we present a sketch of just such a higher-order modal logic: its formal semantics, and a proof procedure (...) using tableaus. Naturally the tableau rules are not complete, but they are with respect to a Henkinization of the “true” semantics. We demonstrate the use of the tableau rules by proving one of the theorems involved in G¨ odel’s ontological argument, one of the rare instances in the literature where higher-order modal constructs have appeared. A fuller treatment of the material presented here is in preparation. (shrink)