Logic, Language, Information, and Computation

The aim of this paper is to define an algorithm that produces a combinatory inhabitant for an implicational theorem of intuitionistic logic from a proof in a sequent calculus. The algorithm is applicable to standard proofs, that exist for every theorem, moreover, non-standard proofs can be straightforwardly transformed into standard ones. We prove that the resulting combinator inhabits the simple type for which it is generated.

In this work, we explore proof theoretical connections between sequent, nested and labelled calculi. In particular, we show a semantical characterisation of intuitionistic, normal and non-normal modal logics for all these systems, via a case-by-case translation between labelled nested to labelled sequent systems.

Brouwer was a founder of intuitionism and he developed intuitionistic mathematics in 1920’s. In particular, he proved the uniform continuity theorem using the fan theorem in 1927, which was derived from a stronger theorem called bar induction. For this principle Brouwer gave a justification which was an important source of BHK-interpretation, but it depends on an assumption which we call “the fundamental assumption” (FA). Since FA was neither explained or justified, many people have thought that Brouwer’s argument is highly controversial. In this paper, we propose a way of formalizing Brouwer’s argument using a method in infinitary proof theory. Also, based on our formalization, we give an explanation and justification of FA from the viewpoint of the practice of intuitionistic mathematics.

Given a logic \(\varvec{\mathcal {L}}\), the \(\varvec{\mathcal {L}}\)-Definability Problem for finite structures takes as input a finite structure \(\varvec{A}\) and a target relation T over the domain of \(\varvec{A}\), and determines whether there is a formula of \(\varvec{\mathcal {L}}\) whose interpretation in \(\varvec{A}\) coincides with T. In this note we present an algorithm that solves the definability problem for quantifier-free first order formulas. Our algorithm takes advantage of a semantic characterization of open definability via subisomorphisms, which is sound and complete. We also provide an empirical evaluation of its performance.

We introduce Arbitrary Public Announcement Logic with Memory (APALM), obtained by adding to the models a ‘memory’ of the initial states, representing the information before any communication took place (“the prior”), and adding to the syntax operators that can access this memory. We show that APALM is recursively axiomatizable (in contrast to the original Arbitrary Public Announcement Logic, for which the corresponding question is still open). We present a complete recursive axiomatization, that uses a natural finitary rule, we study this logic’s expressivity and the appropriate notion of bisimulation.

The abstract Lindenbaum lemma is a crucial result in algebraic logic saying that the prime theories form a basis of the closure systems of all theories of an arbitrary given logic. Its usual formulation is however limited to finitary logics, i.e., logics with Hilbert-style axiomatization using finitary rules only. In this contribution, we extend its scope to all logics with a countable axiomatization and a well-behaved disjunction connective. We also relate Lindenbaum lemma to the Pair extension lemma, other well-known result with many applications mainly in the theory of non-classical modal logics. While a restricted form of this lemma (to pairs with finite right-hand side) is, in our context, equivalent to Lindenbaum lemma, we show a perhaps surprising result that in full strength it holds for finitary logics only. Finally we provide examples demonstrating both limitations and applications of our results.

This paper proposes new semantics for propositional dynamic logic (PDL), replacing the standard relational semantics. Under these new semantics, program execution is represented as fundamentally deterministic (i.e., functional), while nondeterminism emerges as an epistemic relationship between the agent and the system: intuitively, the nondeterministic outcomes of a given process are precisely those that cannot be ruled out in advance. We formalize these notions using topology and the framework of dynamic topological logic (DTL) [1]. We show that DTL can be used to interpret the language of PDL in a manner that captures the intuition above, and moreover that continuous functions in this setting correspond exactly to deterministic processes. We also prove that certain axiomatizations of PDL remain sound and complete with respect to the corresponding classes of dynamic topological models. Finally, we extend the framework to incorporate knowledge using the machinery of subset space logic [2], and show that the topological interpretation of public announcements as given in [3] coincides exactly with a natural interpretation of test programs.

We analyze the parameterized complexity of the satisfiability problem for some prefix-vocabulary fragments of First-order Logic with the finite model property. Here we examine three natural parameters: the quantifier rank, the vocabulary size and the maximum arity of relation symbols. Following the classical classification of decidable prefix-vocabulary fragments, we will see that, for all relational classes of modest complexity and some classical classes, fixed-parameter tractability is achieved by using the above cited parameters.

This paper presents a formalization of the proof of the undecidability of the halting problem for a functional programming language. The computational model consists of a simple first-order functional language called PVS0 whose operational semantics is specified in the Prototype Verification System (PVS). The formalization is part of a termination analysis library in PVS that includes the specification and equivalence proofs of several notions of termination. The proof of the undecidability of the halting problem required classical constructions such as mappings between naturals and PVS0 programs and inputs. These constructs are used to disprove the existence of a PVS0 program that decides termination of other programs, which gives rise to a contradiction.

This paper studies how dependent typed events can be used to treat verb phrase anaphora. We introduce a framework that extends Dependent Type Semantics (DTS) with a new atomic type for neo-Davidsonian events and an extended @-operator that can return new events that share properties of events referenced by verb phrase anaphora.

The proposed framework, along with illustrative examples of its use, are presented after a brief overview of the necessary background and of the major challenges posed by verb phrase anaphora.

Real complexity theory is a resource-bounded refinement of computable analysis and provides a realistic notion of running time of computations over real numbers, sequences, and functions by relying on Turing machines to handle approximations of arbitrary but guaranteed absolute error. Classical results in real complexity show that important numerical operators can map polynomial time computable functions to functions that are hard for some higher complexity class like \(\mathsf {NP}\) or \(\mathsf {\# P}\). Restricted to analytic functions, however, those operators map polynomial time computable functions again to polynomial time computable functions. Recent work by Kawamura, Müller, Rösnick and Ziegler discusses how to extend this to uniform algorithms on one-dimensional analytic functions over simple compact domains using second-order and parameterized complexity. In this paper, we extend some of their results to the case of multidimensional analytic functions. We further use this to show that the operator mapping an analytic ordinary differential equations to its solution is computable in parameterized polynomial time. Finally, we discuss how the theory can be used as a basis for verified exact numerical computation with analytic functions and provide a prototypical implementation in the iRRAM C++ framework for exact real arithmetic.

In the late 1950s A. Tarski published an abstract stating that the set of first order consequences of projective (and also affine) incidence geometry is undecidable. Although his theorem is cited in many follow up papers, a detailed proof was not published. To the best of our knowledge, we have not found a detailed complete proof in the literature. In this paper we analyze what is needed to give a correct proof which is reconstructible by practitioners of AI and automated theorem proving and extend the undecidability to many other axiomatizations of geometry. These include the geometry of Hilbert and Eulidiean planes, Wu’s geometry and Origami geometry. We also discuss applications to automated theorem proving.

Besides the better-known Nelson’s Logic and Paraconsistent Nelson’s Logic, in “Negation and separation of concepts in constructive systems” (1959), David Nelson introduced a logic called \(\mathcal {S}\) with the aim of analyzing the constructive content of provable negation statements in mathematics. Motivated by results from Kleene, in “On the Interpretation of Intuitionistic Number Theory” (1945), Nelson investigated a more symmetric recursive definition of truth, according to which a formula could be either primitively verified or refuted. The logic \(\mathcal {S}\) was defined by means of a calculus lacking the contraction rule and having infinitely many schematic rules, and no semantics was provided. This system received little attention from researchers; it even remained unnoticed that on its original presentation it was inconsistent. Fortunately, the inconsistency was caused by typos and by a rule whose hypothesis and conclusion were swapped. We investigate a corrected version of the logic \(\mathcal {S}\), and focus on its propositional fragment, showing that it is algebraizable in the sense of Blok and Pigozzi (in fact, implicative) with respect to a certain class of involutive residuated lattices. We thus introduce the first (algebraic) semantics for \(\mathcal {S}\) as well as a finite Hilbert-style calculus equivalent to Nelson’s presentation; we also compare \(\mathcal {S}\) with the other two above-mentioned logics of the Nelson family. Our approach is along the same lines of (and partly relies on) previous algebraic work on Nelson’s logics due to M. Busaniche, R. Cignoli, S. Odintsov, M. Spinks and R. Veroff.

In this paper, we study doxastic attitudes that emerge on the basis of argumentational reasoning. In order for an agent’s beliefs to be called ‘rational’, they ought to be well-grounded in strong arguments that are constructed by combining her available evidence in a specific way. A study of how these rational and grounded beliefs emerge requires a new logical setting. The language of the logical system in this paper serves this purpose: it is expressive enough to reason about concepts such as factive combined evidence, correctly grounded belief, and infallible knowledge, which are the building blocks on which our notions of argument and grounded belief can be defined. Building further on previous work, we use a topological semantics to represent the structure of an agent’s collection of evidence, and we use input from abstract argumentation theory to single out the relevant sets of evidence to construct the agent’s beliefs. Our paper provides a sound and complete axiom system for the presented logical language, which can describe the given models in full detail, and we show how this setting can be used to explore more intricate epistemic notions.

In this paper we design a new logical system to explicitly model the different deductive reasoning steps of a boundedly rational agent. We present an adequate system in line with experimental findings about an agent’s reasoning limitations and the cognitive effort that is involved. Inspired by Dynamic Epistemic Logic, we work with dynamic operators denoting explicit applications of inference rules in our logical language. Our models are supplemented by (a) impossible worlds (not closed under logical consequence), suitably structured according to the effect of inference rules, and (b) quantitative components capturing the agent’s cognitive capacity and the cognitive costs of rules with respect to certain resources (e.g. memory, time). These ingredients allow us to avoid problematic logical closure principles, while at the same time deductive reasoning is reflected in our dynamic truth clauses. We finally show that our models can be reduced to awareness-like plausibility structures that validate the same formulas and a sound and complete axiomatization is given with respect to them.