Logical Foundations of Computer Science

Frontmatter

Modal Logics with Hard Diamond-Free Fragments

Abstract

We investigate the complexity of modal satisfiability for certain combinations of modal logics. In particular we examine four examples of multimodal logics with dependencies and demonstrate that even if we restrict our inputs to diamond-free formulas (in negation normal form), these logics still have a high complexity. This result illustrates that having D as one or more of the combined logics, as well as the interdependencies among logics can be important sources of complexity even in the absence of diamonds and even when at the same time in our formulas we allow only one propositional variable. We then further investigate and characterize the complexity of the diamond-free, 1-variable fragments of multimodal logics in a general setting.

Antonis Achilleos

Pairing Traditional and Generic Common Knowledge

Abstract

Common Knowledge C is a standard tool in epistemic logics. Generic Common Knowledge J is an alternative which has desirable logical behavior such as cut-elmination and which can be used in place of C in the analysis of many games and epistemic senarios. In order to compare their deductive strengths directly we define the multi-agent logic \(\mathsf{S4}_n^{CJ}\) built on a language with both C and J operators in addition to agents’ \(K_i\)s so that any finite prefix of modal operators is acceptable. We prove \(\mathsf{S4}_n^{CJ}\) is complete, decidable, and that \(J\varphi \rightarrow C\varphi \) though not \(C\varphi \rightarrow J\varphi \). Additional epistemic scenarios may be investigated which take advantage of this dual layer of common knowledge agents.

Evangelia Antonakos

On Aggregating Probabilistic Evidence

Abstract

Imagine a database – a set of propositions \(\varGamma =\{F_1,\ldots ,F_n\}\) with some kind of probability estimates, and let a proposition X logically follow from \(\varGamma \). What is the best justified lower bound of the probability of X? The traditional approach, e.g., within Adams’ Probability Logic, computes the numeric lower bound for X corresponding to the worst-case scenario. We suggest a more flexible parameterized approach by assuming probability events \(u_1,u_2,\ldots ,u_n\) which support \(\varGamma \), and calculating aggregated evidence \(e(u_1,u_2,\ldots ,u_n)\) for X. The probability of e provides a tight lower bound for any, not only a worst-case, situation. The problem is formalized in a version of justification logic and the conclusions are supported by corresponding completeness theorems. This approach can handle conflicting and inconsistent data and allows the gathering both positive and negative evidence for the same proposition.

Sergei Artemov

Classical Logic with Mendler Induction

A Dual Calculus and Its Strong Normalization

Abstract

We investigate (co-)induction in Classical Logic under the propositions-as-types paradigm, considering propositional, second-order, and (co-)inductive types. Specifically, we introduce an extension of the Dual Calculus with a Mendler-style (co-)iterator that remains strongly normalizing under head reduction. We prove this using a non-constructive realizability argument.

Marco Devesas Campos, Marcelo Fiore

Index Sets for Finite Normal Predicate Logic Programs with Function Symbols

Abstract

We study the recognition problem in the metaprogramming of finite normal predicate logic programs. That is, let \(\mathcal {L}\) be a computable first order predicate language with infinitely many constant symbols and infinitely many n-ary predicate symbols and n-ary function symbols for all \(n \ge 1\). Then we can effectively list all the finite normal predicate logic programs \(Q_0,Q_1,\ldots \) over \(\mathcal L\). Given some property \(\mathcal{P}\) of finite normal predicate logic programs over \(\mathcal L\), we define the index set \(I_\mathcal{P}\) to be the set of indices e such that \(Q_e\) has property \(\mathcal P\). Then we shall classify the complexity of the index set \(I_\mathcal{P}\) within the arithmetic hierarchy for various natural properties of finite predicate logic programs.

Douglas Cenzer, Victor W. Marek, Jeffrey B. Remmel

Multiple Conclusion Rules in Logics with the Disjunction Property

Abstract

We prove that for the intermediate logics with the disjunction property any basis of admissible rules can be reduced to a basis of admissible m-rules (multiple-conclusion rules), and every basis of admissible m-rules can be reduced to a basis of admissible rules. These results can be generalized to a broad class of logics including positive logic and its extensions, Johansson logic, normal extensions of \(\mathsf {S4}\), n-transitive logics and intuitionistic modal logics.

Alex Citkin

Multiple Conclusion Linear Logic: Cut Elimination and More

Abstract

Full Intuitionistic Linear Logic (FILL) was first introduced by Hyland and de Paiva, and went against current beliefs that it was not possible to incorporate all of the linear connectives, e.g. tensor, par, and implication, into an intuitionistic linear logic. It was shown that their formalization of FILL did not enjoy cut-elimination by Bierman, but Bellin proposed a change to the definition of FILL in the hope to regain cut-elimination. In this note we adopt Bellin’s proposed change and give a direct proof of cut-elimination. Then we show that a categorical model of FILL in the basic dialectica category is also a LNL model of Benton and a full tensor model of Melliès’ and Tabareau’s tensorial logic. Lastly, we give a double-negation translation of linear logic into FILL that explicitly uses par in addition to tensor.

Harley Eades III, Valeria de Paiva

The Online Space Complexity of Probabilistic Languages

Abstract

In this paper, we define the online space complexity of languages, as the size of the smallest abstract machine processing words sequentially and able to determine at every point whether the word read so far belongs to the language or not. The first part of this paper motivates this model and provides examples and preliminary results.

One source of inspiration for introducing the online space complexity of languages comes from a seminal paper of Rabin from 1963, introducing probabilistic automata, which suggests studying the online space complexity of probabilistic languages. This is the purpose of the second part of the current paper.

Nathanaël Fijalkow

Type Theoretical Databases

Abstract

We show how the display-map category of finite simplicial complexes can be seen as representing the totality of database schemas and instances in a single mathematical structure. We give a sound interpretation of a certain dependent type theory in this model, and show how it allows for the syntactic specification of schemas and instances and the manipulation of the same with the usual type-theoretic operations. We indicate how it allows for the posing of queries. A novelty of the type theory is that it has non-trivial context constants.

Henrik Forssell, Håkon Robbestad Gylterud, David I. Spivak

Augmenting Subset Spaces to Cope with Multi-agent Knowledge

Abstract

Subsequently, a particular extension of the bi-modal logic of subset spaces, LSS, to the case of several agents will be provided. The basic system, which originally was designed for revealing the intrinsic relationship between knowledge and topology, has been developed in several directions in recent years, not least towards a comprehensive knowledge-theoretic formalism. However, while subset spaces have been shown to be smoothly combinable with various epistemic concepts in the single-agent case, adjusting them to general multi-agent scenarios has brought about rather unsatisfactory results up to now. This is due to reasons inherent in the system so that one is led to consider more special cases. In the present paper, such a widening of LSS to the multi-agent setting is proposed. The peculiarity is here given by the case that the agents are supplied with certain knowledge-enabling functions allowing, in particular, for comparing their respective knowledge. It turns out that such circumstances can be modeled in corresponding logical terms to a considerable extent.

Bernhard Heinemann

On Lambek’s Restriction in the Presence of Exponential Modalities

Abstract

The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called “Lambek’s restriction,” that is, the antecedent of any provable sequent should be non-empty. In this paper we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. We present several versions of the Lambek calculus extended with exponential modalities and prove that those extensions are undecidable, even if we take only one of the two divisions provided by the Lambek calculus.

Max Kanovich, Stepan Kuznetsov, Andre Scedrov

A Quest for Algorithmically Random Infinite Structures, II

Abstract

We present an axiomatic approach that introduces algorithmic randomness into various classes of structures. The central concept is the notion of a branching class. Through this technical yet simple notion we define measure, metric, and topology in many classes of graphs, trees, relational structures, and algebras. As a consequence we define algorithmically random structures. We prove the existence of algorithmically random structures with various computability-theoretic properties. We show that any nontrivial variety of algebras has an effective measure 0. We also prove a counter-intuitive result that there are algorithmically random yet computable structures. This establishes a connection between algorithmic randomness and computable model theory.

Bakhadyr Khoussainov

Probabilistic Justification Logic

Abstract

We present a probabilistic justification logic, \(\mathsf {PPJ} \), to study rational belief, degrees of belief and justifications. We establish soundness and completeness for \(\mathsf {PPJ} \) and show that its satisfiability problem is decidable. In the last part we use \(\mathsf {PPJ} \) to provide a solution to the lottery paradox.

Ioannis Kokkinis, Zoran Ognjanović, Thomas Studer

Sequent Calculus for Intuitionistic Epistemic Logic IEL

Abstract

The formal system of intuitionistic epistemic logic IEL was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer-Hayting-Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. We prove that IEL is PSPACE-complete.

Vladimir N. Krupski, Alexey Yatmanov

Interpolation Method for Multicomponent Sequent Calculi

Abstract

The proof-theoretic method of proving the Craig interpolation property was recently extended from sequents to nested sequents and hypersequents. There the notations were formalism-specific, obscuring the underlying common idea, which is presented here in a general form applicable also to other similar formalisms, e.g., prefixed tableaus. It describes requirements sufficient for using the method on a proof system for a logic, as well as additional requirements for certain types of rules. The applicability of the method, however, does not imply its success. We also provide examples from common proof systems to highlight various types of interpolant manipulations that can be employed by the method. The new results are the application of the method to a recent formalism of grafted hypersequents (in their tableau version), the general treatment of external structural rules, including the analytic cut, and the method’s extension to the Lyndon interpolation property.

Roman Kuznets

Adjoint Logic with a 2-Category of Modes

Abstract

We generalize the adjoint logics of Benton and Wadler [1994, 1996] and Reed [2009] to allow multiple different adjunctions between the same categories. This provides insight into the structural proof theory of cohesive homotopy type theory, which integrates the synthetic homotopy theory of homotopy type theory with the synthetic topology of Lawvere’s axiomatic cohesion. Reed’s calculus is parametrized by a preorder of modes, where each mode determines a category, and there is an adjunction between categories that are related by the preorder. Here, we consider a logic parametrized by a 2-category of modes, where each mode represents a category, each mode morphism represents an adjunction, and each mode 2-morphism represents a pair of conjugate natural transformations. Using this, we give mode theories that describe adjoint triples of the sort used in cohesive homotopy type theory. We give a sequent calculus for this logic, show that identity and cut are admissible, show that this syntax is sound and complete for pseudofunctors from the mode 2-category to the 2-category of adjunctions, and investigate some constructions in the example mode theories.

Daniel R. Licata, Michael Shulman

Parallel Feedback Turing Computability

Abstract

In contrast to most kinds of computability studied in mathematical logic, feedback computability has a non-degenerate notion of parallelism. Here we study parallelism for the most basic kind of feedback, namely that of Turing computability. We investigate several different possible definitions of parallelism in this context, with an eye toward specifying what is so computable. For the deterministic notions of parallelism identified we are successful in this analysis; for the non-deterministic notion, not completely.

Robert S. Lubarsky

Compactness in the Theory of Continuous Automata

Abstract

We develop a topological theory of continuous-time automata which replaces finiteness assumptions in the classical theory of finite automata by compactness assumptions. The theory is designed to be as mathematically simple as possible while still being relevant to the question of physical feasibility. We include a discussion of which behaviors are and are not permitted by the framework, and the physical significance of these questions. To illustrate the mathematical tractability of the theory, we give basic existence results and a Myhill-Nerode theorem. A major attraction of the theory is that it covers finite automata and continuous automata in the same abstract framework.

Scott Messick

Measure Quantifier in Monadic Second Order Logic

Abstract

We study the extension of Monadic Second Order logic with the “for almost all” quantifier \(\forall ^{=1}\) whose meaning is, informally, that \(\forall ^{=1}X.\phi (X)\) holds if \(\phi (X)\) holds almost surely for a randomly chosen X. We prove that the theory of \(\mathrm {MSO}+\forall ^{=1}\) is undecidable both when interpreted on \((\omega ,<)\) and the full binary tree. We then identify a fragment of \(\mathrm {MSO}+\forall ^{=1}\), denoted by \(\mathrm {MSO}+\forall ^{=1}_\pi \), and reduce some interesting problems in computer science and mathematical logic to the decision problem of \(\mathrm {MSO}+ \forall ^{=1}_\pi \). The question of whether \(\mathrm {MSO}+\forall ^{=1}_\pi \) is decidable is left open.

Henryk Michalewski, Matteo Mio

A Cut-Free Labelled Sequent Calculus for Dynamic Epistemic Logic

Abstract

Dynamic Epistemic Logic is a logic that is aimed at formally expressing how a person’s knowledge changes. We provide a cut-free labelled sequent calculus (\(\mathbf {GDEL}\)) on the background of existing studies of Hilbert-style axiomatization \(\mathbf {HDEL}\) by Baltag et al. (1989) and labelled calculi for Public Announcement Logic by Maffezioli et al. (2011) and Nomura et al. (2015). We first show that the cut rule is admissible in \(\mathbf {GDEL}\). Then we show \(\mathbf {GDEL}\) is sound and complete for Kripke semantics. Lastly, we touch briefly on our on-going work of an automated theorem prover of \(\mathbf {GDEL}\).

Shoshin Nomura, Hiroakira Ono, Katsuhiko Sano

The Urysohn Extension Theorem for Bishop Spaces

Abstract

Bishop’s notion of function space, here called Bishop space, is a function-theoretic analogue to the classical set-theoretic notion of topological space. Bishop introduced this concept in 1967, without exploring it, and Bridges revived the subject in 2012. The theory of Bishop spaces can be seen as a constructive version of the theory of the ring of continuous functions. In this paper we define various notions of embeddings of one Bishop space to another and develop their basic theory in parallel to the classical theory of embeddings of rings of continuous functions. Our main result is the translation within the theory of Bishop spaces of the Urysohn extension theorem, which we show that it is constructively provable. We work within Bishop’s informal system of constructive mathematics \(\mathrm {BISH}\), inductive definitions with countably many premises included.

Iosif Petrakis

An Arithmetical Interpretation of Verification and Intuitionistic Knowledge

Abstract

Intuitionistic epistemic logic introduces an epistemic operator, which reflects the intended BHK semantics of intuitionism, to intuitionistic logic. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the Logic of Proofs and its arithmetical semantics. We show here that this interpretation can be extended to the notion of verification upon which intuitionistic knowledge is based, thereby providing the systems of intuitionistic epistemic logic extended by an epistemic operator based on verification with an arithmetical semantics too.

Tudor Protopopescu

Definability in First Order Theories of Graph Orderings

Abstract

We study definability in the first order theory of graph order: that is, the set of all simple finite graphs ordered by either the minor, subgraph or induced subgraph relation. We show that natural graph families like cycles and trees are definable, as also notions like connectivity, maximum degree etc. This naturally comes with a price: bi-interpretability with arithmetic. We discuss implications for formalizing statements of graph theory in such theories of order.

R. Ramanujam, R. S. Thinniyam

The Complexity of Disjunction in Intuitionistic Logic

Abstract

In the formal study of security protocols and access control systems, fragments of intuitionistic logic play a vital role. These are required to be efficient, and are typically disjunction-free. In this paper, we study the complexity of adding disjunction to these subsystems. Our lower bound results show that very little needs to be added to disjunction to get co-NP-hardness, while our upper bound results show that even a system with conjunction, disjunction, and restricted forms of negation and implication is in co-NP. Our upper bound proofs also suggest parameters which we can bound to obtain PTIME algorithms.

R. Ramanujam, Vaishnavi Sundararajan, S. P. Suresh

Intransitive Temporal Multi-agent’s Logic, Knowledge and Uncertainty, Plausibility

Abstract

We study intransitive temporal logic implementing multi-agent’s approach and formalizing knowledge and uncertainty. An innovative point here is usage of non-transitive linear time and multi-valued models - the ones using separate valuations \(V_j\) for agent’s knowledge of facts and summarized (agreed) valuation together with rules for computation truth values for compound formulas. The basic mathematical problems we study here are - decidability and decidability w.r.t. admissible rules. First, we study general case - the logic with non-uniform intransitivity and solve its decidability problem. Also we consider a modification of this logic - temporal logic with uniform non-transitivity and solve problem of recognizing admissibility in this logic.

Vladimir Rybakov

Ogden Property for Linear Displacement Context-Free Grammars

Abstract

It is known that Ogden lemma fails for the class of k-well-nested multiple context-free languages for \(k \ge 3\). In this article we prove a relaxed version of this lemma for linear well-nested MCFLs and show that its statement may be applied to generate counterexamples of linear well-nested MCFLs by the method already existing for the stronger variant.

Alexey Sorokin

Levy Labels and Recursive Types

Abstract

In this note we introduce a generalization of the Levy label technique which applies easily to lambda calculus with beta-eta conversion and lambda calculus with surjective pairing a’ la PSP.

Rick Statman

Backmatter