Prague Workshop on Nonclassical Logics

We propose a general framework for dynamic epistemic logics (DELs). It consists of a generic language for DELs and a class of structures, called model transition systems (MTSs), that describe model transformations in a static way. An MTS can be viewed as a two-layered Kripke model and consequently inherits standard concepts such as bisimulation and bounded morphism from the ordinary Kripke models. In the second half, we add the global operator to the language, which enables us to define the notions of a canonical MTS and canonicity of a DEL formula for a property of MTSs. Using these notions, we clarify correspondences between axioms of DELs and properties of MTSs.

Algorithmic randomness is a study of randomness which is based on the notion of computability. One of the most standard way to define randomness is using the notion of test; on the Cantor space 2^ω, it is a sequence of open sets of 2^ω of which intersection has a measure zero and which has certain computability condition. Each test represents the set of strings that has some "constructive exceptional property", and a string that is not contained by any test is said to be random.

Since the notion of test has been proposed by Martin-Lőf in 1966 various classes of randomness have been studied, which led us to organize the "randomness zoo", while we do not have enough knowledge to treat them in a uniform way. We try to develop the theory to the latter direction via category theory. Specifically, we define test as coalgebra that satisfies certain computability and exceptionality condition, based on an observation that tests can be naturally seen as certain labeled transition systems.

As is well-known, the idea of three-valued interpretation has been playing a fundamental role in the pursuit of cut elimination for higher order logics. It dates back to Schuette's work in 1950's, where the concept of semivaluation is introduced to semantically explain Takeuti's conjecture. It has led to semantic and impredicative proofs of cut elimination by Tait, Takahashi and Prawitz in 1960's. It is further turned into a three-valued interpretation and a topological semantics by (Girard 1976). Along the same line are the algebraic proofs of cut elimination for various non-classical logics by Maehara and Okada in 1990's, leading to the concept of residuated frame of Jipsen and Galatos in 2000's. All these works, and in fact many more, are intimately connected.

The same idea can be used to mathematically formalize a semantic criterion for cut elimination, known as the "harmony" property. Namely, we consider a new logical connective defined by a set of inference rules in the setting of substructural logics. Under a certain (rather strong) restriction, any such connective admits an interpretation in the "three-valued" semantics for substructural logics (i.e., the intervals of a residuated lattice). Now one can show that cut elimination holds for the new logic if and only if the interpretation collapses to the standard "two-valued" one (Ciabattoni-Terui 06), thus leading to a semantic criterion for cut elimination.

The talk will be an introductory exposition of this line of research.

We introduce fibred type-theoretic fibration categories which are fibred categories between categorical models of dependent type theory with identity types. Fibred type-theoretic fibration categories give a categorical description of logical relations for identity types. As an application, we show that in homotopy type theory, a polymorphic function from a loop space to itself must be homotopic to some iterated concatenation of a loop.

Dung's seminal paper introducing abstract argumentation frames (1995) lead to an impressive amount of research devoted to a host of different semantics, corresponding algorithms, instantiation mechanisms, classifications of argument forms, etc, but also to various applications in AI and beyond. Nevertheless, we claim that there is still room for alternative foundations inspired by Dung's basic concept. In this spirit we propose to extract (new and old) consequence relations from given semi-abstract argumentation frames. Semi-abstract argumentation arises from abstract argumentation by instantiating the claims of arguments with (potentially logically complex) propositions, while ignoring the structure of their support. In this manner one may define logical consequence as arising from first principles like "every argument attacking A also attacks the conjunction of A and B" and "every argument attacking a disjunctive claim also attacks each of its disjuncts". This amounts to an alternative semantic framework, closer to, e.g., Brandom's incompatibility semantics than to the traditional Tarskian notion of truth in a model. We will show that classical logic emerges only if principles are imposed that, arguably, are too strong with respect to intended interpretations. Nonclassical consequence relations arise from principles that correspond to some, but not all logical introduction rules of Gentzen's sequent calculus LK. This observation allows one to relate corresponding "argumentative consequence relations" to nondeterministic matrix semantics as studied by Avron, Lahav. Lev, and Zamansky. If time permits, we will also indicate various routes for relating argumentative consequence to relevant consequence, in the the sense of Anderson, Belnap, Dunn, etc.

The strict-tolerant (ST) approach to paradox, recently proposed by Cobreros, Egré, Ripley and van Rooy, promises to erect theories of naïve truth and tolerant vagueness on the firm bedrock of classical logic. We assess the extent to which this claim is founded. We show that the usual proof-theoretic formulation of propositional ST in terms of the classical sequent calculus without primitive Cut is incomplete with respect to ST-valid metainferences, and exhibit a complete calculus for the same class of metainferences. Capitalising on results by Pynko and Barrio et al., we also argue that the latter calculus, far from coinciding with classical logic, is a close kin of Priest's LP.

The SAT problem for classical propositional logic has been in the limelight of complexity theory research for decades. We present it in the setting of residuated lattices (FLew-algebras and beyond), identifying, i.a., a large class of algebras whose SAT is classical. We outline the position of satisfiability among fragments of the existential/universal theory, using the class of MV-algebras as model example and building on strong algebraic results of Gispert and Mundici. Time permitting, satisfiability of first-order formulas, with implications for consistency of theories, will be discussed. Parts of the presentation are based on a recent joint paper with Savický.

We apply methods of coalgebraic logic to investigate expressivity of many-valued modal logics, which we therefore consider as coalgebraic languages interpreted over set-coalgebras with genuinely many-valued valuations. The languages are based on modalities understood as many-valued predicate liftings. We provide a sufficient condition for a language generated by a set of such modalities to be expressive for bisimilarity: the condition says that we can separate behaviours using the propositional language and modalities. The condition is a generalization of the usual separation condition on the set of predicate liftings, but now it also involves the algebra of truth values substantially. Thus, adapting results of Schrőder concerning expressivity of boolean coalgebraic logics to many-valued setting, we generalize results of Metcalfe and Martí, concerning Hennessy-Milner property for many-valued modal logics based on box and diamond.