A general method for generating contraction- and cut-free sequent calculi for a large family of normal modal logics is presented. The method covers all modal logics characterized by Kripke frames determined by universal or geometric properties and it can be extended to treat also Gödel-Löb provability logic. The calculi provide direct decision methods through terminating proof search. Syntactic proofs of modal undefinability results are obtained in the form of conservativity theorems.

is used to give a formalization of Artemov’s knowledge based reasoning approach to game theory, (KBR), [ 4 , 5 ]. Epistemic states of players are represented explicitly and reasoned about formally. We give a detailed analysis of the Centipede game using both proof theoretic and semantic machinery. This helps make the case that PDL + E can be a useful basis for the logical investigation of game theory.

The term verificationism is used in two different ways: the first is in relation to the verification principle of meaning, which we usually and rightly associate with the logical empiricists, although, as we now know, it derives in reality from Wittgenstein, and the second is in relation to the theory of meaning for intuitionistic logic that has been developed, beginning of course with Brouwer, Heyting and Kolmogorov in the twenties and early thirties, but in much more detail lately, particularly in (...) connection with intuitionistic type theory. It is therefore very natural to ask how these two forms of verificationism are related to one another: was the verificationism that we had in the thirties a kind of forerunner of what we have now, or was it something entirely different? I would like to discuss this question by considering a very particular problem, which was at the heart of Schlick’s interests, namely, the problem whether there might exist undecidable propositions or, if you prefer, unsolvable problems or unanswerable questions: it is merely a matter of wording which of these terms you choose. As I said, it is a problem which was at the heart of Schlick’s interests: it is explicitly discussed already in his early, programmatic paper Die Wende in der Philosophie in the first volume of Erkenntnis from 1930, and there is a short late paper, which has precisely Unanswerable Questions? as its title, from 1935, and he discussed it on several occasions in between also. (shrink)

Geometric theories are presented as contraction- and cut-free systems of sequent calculi with mathematical rules following a prescribed rule-scheme that extends the scheme given in Negri and von Plato. Examples include cut-free calculi for Robinson arithmetic and real closed fields. As an immediate consequence of cut elimination, it is shown that if a geometric implication is classically derivable from a geometric theory then it is intuitionistically derivable.

Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$, by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$. The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}$. A Gentzen-style reconstruction of the Church–Fitch paradox is presented (...) following a labelled approach to sequent calculi. First, a cut-free system for classical bimodal logic is introduced as the logical basis for the Church–Fitch paradox and the relationships between ${\mathcal {K}}$ and ${\diamondsuit}$ are taken into account. Afterwards, by exploiting the structural properties of the system, in particular cut elimination, the semantic frame conditions that correspond to KP are determined and added in the form of a block of nonlogical inference rules. Within this new system for classical and intuitionistic “knowability logic”, it is possible to give a satisfactory cut-free reconstruction of the Church–Fitch derivation and to confirm that OP is only classically derivable, but neither intuitionistically derivable nor intuitionistically admissible. Finally, it is shown that in classical knowability logic, the Church–Fitch derivation is nothing else but a fallacy and does not represent a real threat for anti-realism. (shrink)

In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.

We prove completeness and decidability results for a family of combinations of propositional dynamic logic and unimodal doxastic logics in which the modalities may interact. The kind of interactions we consider include three forms of commuting axioms, namely, axioms similar to the axiom of perfect recall and the axiom of no learning from temporal logic, and a Church–Rosser axiom. We investigate the influence of the substitution rule on the properties of these logics and propose a new semantics for the test (...) operator to avoid unwanted side effects caused by the interaction of the classic test operator with the extra interaction axioms. (shrink)

Game Logic is a modal logic which extends Propositional Dynamic Logic by generalising its semantics and adding a new operator to the language. The logic can be used to reason about determined 2-player games. We present an overview of meta-theoretic results regarding this logic, also covering the algebraic version of the logic known as Game Algebra.