ALBERT

Description: We present a proof system for the provability logic GLP in the formalism of nested sequents and prove the cut elimination theorem for it. As an application, we obtain the reduction of GLP to its important fragment called J syntactically.

Description: Intuitionistic sentential logic is shown to be sound and complete with respect to a semantics centered around extensions of atomic bases (i.e. sets of inference rules for atomic sentences). The result is made possible through a non-standard interpretation of disjunction, whereby, roughly speaking, a disjunction is taken to hold just in case every atomic sentence that follows from each of the disjuncts separately holds; it is argued that this interpretation makes good sense provided that rules in atomic bases are conceived of as being accepted hypothetically rather than categorically.

Description: Motivated by both established and new applications, we study navigational query languages for graphs (binary relations). The simplest language has only the two operators union and composition, together with the identity relation. We make more powerful languages by adding any of the following operators: intersection; set difference; projection; coprojection; converse; transitive closure; and the diversity relation. All these operators map binary relations to binary relations. We compare the expressive power of all resulting languages, both for binary-relation queries as well as for boolean queries. In the absence of transitive closure, a complete Hasse diagram of relative expressiveness has already been established [ 8 ]. Moreover, it has already been shown that for boolean queries over a single edge label, transitive closure does not add any expressive power when only projection and diversity may be present [ 11 ]. In the present article, we now complete the Hasse diagram in the presence of transitive closure, both for the case of a single edge label, as well as for the case of at least two edge labels. The main technical results are the following: (1) In contrast to the above-stated result [ 11 ] transitive closure does add expressive power when coprojection is present. (2) Transitive closure also adds expressive power as soon as converse is present. (3) Conversely, converse adds expressive power in the presence of transitive closure. In particular, the converse elimination result from [ 8 ] no longer works in the presence of transitive closure. (4) As a corollary, we show that the converse elimination result from [ 8 ] necessitates an exponential blow-up in the degree of the expressions.

Description: Many authors have argued that, when performing simultaneous statistical test procedures, one should seek for solutions that lead to decisions that are consistent and, consequently, easier to communicate to practitioners of statistical methods. In this way, the set of hypotheses that are rejected and the set of hypotheses that are not rejected by a testing procedure should be consistent from a logic standpoint. For instance, if hypothesis A implies hypothesis B , a procedure that rejects B should also reject A , a property not always met by multiple test procedures. We contribute to this discussion by exploring how far one can go in constructing coherent procedures while still preserving statistical optimality. This is done by studying four types of logical consistency relations. We show that although the only procedures that satisfy more than (any) two of these properties are simple tests based on point estimation, it is possible to construct various interesting methods that fulfil one or two of them while preserving different statistical optimality criteria. This is illustrated with several Bayesian and frequentist examples. We also characterize some of these properties under a decision-theoretic framework.

Description: The Svenonius theorem describes the (first-order) definability in a structure in terms of permutations preserving the relations of elementary extensions of the structure. In the present article, we prove a version of this theorem using permutations of sequences over the original structure (these are permutations of sequences of tuples of the structure elements as well). We say that such a permutation almost preserves a relation if for every sequence of its arguments the value of the relation on an n -th element of the sequence and on its image under coincide for almost all numbers n . We prove that a relation is definable in a structure iff the relation is almost preserved by all permutations almost preserving the relations of the structure. This version limits consideration to the original structure only and does not refer to any logical notion, such as ‘elementary equivalence’.

Description: The celebrated theorem proved by Goldblatt and Thomason in 1974 gives necessary and sufficient conditions for an elementary class of Kripke frames to be modally definable. Here we obtain a local analogue of this result, which deals with modal definability of classes of pointed frames. Furthermore, we generalize it to the case of n -frames , which are frames with n distinguished worlds. For talking about n -frames, we generalize modal formulas to modal expressions . While a modal formula is evaluated at a single world of a model, a modal expression with n individual variables is evaluated at an n -tuple of worlds, just as a first-order formula with n free variables. We introduce operations on n -frames that preserve validity of modal expressions, and show that closure under these operations is a necessary and sufficient condition for an elementary class of n -frames to be modally definable. We also discuss the relationship between modal expressions and hybrid logic and leave open questions.

Description: We add strong negation N to classical logic and interpret the attack relation of ‘ x attacks y ’ in argumentation as (x-〉Ny) . We write a corresponding object level (using N only) classical theory for each argumentation network and show that the classical models of this theory correspond exactly to the complete extensions of the argumentation network. We show by example how this approach simplifies the study of abstract argumentation networks. We compare with other translations of abstract argumentation networks into logic, such as classical predicate logic or modal logics, or logic programming, and we also compare with Abstract Dialectical Frameworks.

Description: This article uses possible-world semantics to model the changes that may occur in an agent's knowledge as she loses information. This builds on previous work in which the agent may forget the truth-value of an atomic proposition, to a more general case where she may forget the truth-value of a propositional formula. The generalization poses some challenges, since in order to forget whether a complex proposition is the case, the agent must also lose information about the propositional atoms that appear in it, and there is no unambiguous way to go about this. We resolve this situation by considering expressions of the form [] , which quantify over all possible (but ‘minimal’) ways of forgetting whether . Propositional atoms are modified non-deterministically, although uniformly, in all possible worlds. We then represent this within action model logic in order to give a sound and complete axiomatization for a logic with knowledge and forgetting. Finally, some variants are discussed, such as when an agent forgets (rather than forgets whether ) and when the modification of atomic facts is done non-uniformly throughout the model.

Description: There are various ways of achieving an enlarged understanding of a concept of interest. One way is by giving its proper definition. Another is by giving something else a proper definition and then using it to model or formally represent the original concept. Between the two we find varying shades of grey. We might open up a concept by a direct lexical definition of the predicate that expresses it, or by a theory whose theorems define it implicitly. At the other end of the spectrum, the modelling-this-as-that option also admits of like variation, ranging from models rooted in formal representability theorems to models conceived of as having only heuristic value. There exist on both sides of this divide further differences still. In one of them, both the definiendum and definiens of a definition are words or phrases of some common natural language. In others, the item of interest is a natural language expression and its representation is furnished by the artificial linguistic system that models it. The modern history of these approaches is both very large and growing. Much of this evolution has given too short a shrift to the history of the demotion of ‘intuitive’ concepts in favour of the artificially contrived ones intended to model them. A working assumption of this article is that in the absence of a good understanding of what motivated the modelling-turn in the foundations of mathematics and the intuitive theory of truth, the whole notion of formal representability will have been inadequately understood. In the interests of space, I will concentrate on seminal issues in set theory as dealt with by Russell and Frege, and in the theory of truth in natural languages as dealt with by Tarski. The nub of the present focus is the representational role of model theory in the logics of formalized languages.