Inhabitation of polymorphic and existential types

This paper shows that the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable, where the inhabitation problem asks whether there exists some term that belongs to a given type. In order to do that, this paper proves the decidability of the provability in the logical system defined from the second-order natural deduction by removing implication and disjunction. This is proved by showing the quantifier elimination theorem and reducing the problem to the provability in propositional logic. The magic formulas are used for quantifier elimination such that they replace quantifiers. As a byproduct, this paper also shows the second-order witness theorem which states that a quantifier followed by negation can be replaced by a witness obtained only from the formula. As a corollary of the main results, this paper also shows Glivenko’s theorem, Double Negation Shift, and conservativity for antecedent-empty sequents between the logical system and its classical version.     

Vectorization hierarchies of some graph quantifiers

We give a sufficient condition for the inexpressibility of the k-th extended vectorization of a generalized quantifier in , the extension of first-order logic by all k-ary quantifiers. The condition is based on a model construction which, given two -equivalent models with certain additional structure, yields a pair of -equivalent models. We also consider some applications of this condition to quantifiers that correspond to graph properties, such as connectivity and planarity. Received: 15 October 1996     

A modal logic framework for reasoning about comparative distances and topology

We propose and investigate a uniform modal logic framework for reasoning about topology and relative distance in metric and more general distance spaces, thus enabling the comparison and combination of logics from distinct research traditions such as Tarski’s S4 for topological closure and interior, conditional logics, and logics of comparative similarity. This framework is obtained by decomposing the underlying modal-like operators into first-order quantifier patterns. We then show that quite a powerful and natural fragment of the resulting first-order logic can be captured by one binary operator comparing distances between sets and one unary operator distinguishing between realised and limit distances (i.e., between minimum and infimum). Due to its greater expressive power, this logic turns out to behave quite differently from both S4 and conditional logics. We provide finite (Hilbert-style) axiomatisations and ExpTime-completeness proofs for the logics of various classes of distance spaces, in particular metric spaces. But we also show that the logic of the real line (and various other important metric spaces) is not recursively enumerable. This result is proved by an encoding of Diophantine equations.     

Craig interpolation for semilinear substructural logics

The Craig interpolation property is investigated for substructural logics whose algebraic semantics are varieties of semilinear (subdirect products of linearly ordered) pointed commutative residuated lattices. It is shown that Craig interpolation fails for certain classes of these logics with weakening if the corresponding algebras are not idempotent. A complete characterization is then given of axiomatic extensions of the “R‐mingle with unit” logic (corresponding to varieties of Sugihara monoids) that have the Craig interpolation property. This latter characterization is obtained using a model‐theoretic quantifier elimination strategy to determine the varieties of Sugihara monoids admitting the amalgamation property.     

Inclusion and exclusion dependencies in team semantics — On some logics of imperfect information

We introduce some new logics of imperfect information by adding atomic formulas corresponding to inclusion and exclusion dependencies to the language of first order logic. The properties of these logics and their relationships with other logics of imperfect information are then studied. As a corollary of these results, we characterize the expressive power of independence logic, thus answering an open problem posed in Grädel and Väänänen, 2010 [9].     

Modal characterisation theorems over special classes of frames

We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem’s theorem, which says that a first-order formula is invariant under bisimulation if, and only if, it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes-for instance, rooted frames, finite rooted frames, finite transitive frames, well-founded transitive frames, finite equivalence frames-as these are not elementary. Instead we develop and extend the game-based analysis (first-order Ehrenfeucht-Fraïssé versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes. Over most of the classes considered, we obtain finite model theory analogues of the classically expected characterisations, with new proofs also for the classical setting. The class of transitive frames is a notable exception, with a marked difference between the classical and the finite model theory of bisimulation invariant first-order properties. Over the class of all finite transitive frames in particular, we find that monadic second-order logic is no more expressive than first-order as far as bisimulation invariant properties are concerned — though both are more expressive here than basic modal logic. We obtain ramifications of the de Jongh-Sambin theorem and a new and specific analogue of the Janin-Walukiewicz characterisation of bisimulation invariant monadic second-order for finite transitive frames.     

Dependence of variables construed as an atomic formula

We define a logic D capable of expressing dependence of a variable on designated variables only. Thus D has similar goals to the Henkin quantifiers of [4] and the independence friendly logic of [6] that it much resembles. The logic D achieves these goals by realizing the desired dependence declarations of variables on the level of atomic formulas. By [3] and [17], ability to limit dependence relations between variables leads to existential second order expressive power. Our D avoids some difficulties arising in the original independence friendly logic from coupling the dependence declarations with existential quantifiers. As is the case with independence friendly logic, truth of D is definable inside D. We give such a definition for D in the spirit of [11] and [2] and [1].     

Logical omniscience as infeasibility

Logical theories for representing knowledge are often plagued by the so-called Logical Omniscience Problem. The problem stems from the clash between the desire to model rational agents, which should be capable of simple logical inferences, and the fact that any logical inference, however complex, almost inevitably consists of inference steps that are simple enough. This contradiction points to the fruitlessness of trying to solve the Logical Omniscience Problem qualitatively if the rationality of agents is to be maintained. We provide a quantitative solution to the problem compatible with the two important facets of the reasoning agent: rationality and resource boundedness. More precisely, we provide a test for the logical omniscience problem in a given formal theory of knowledge. The quantitative measures we use are inspired by the complexity theory. We illustrate our framework with a number of examples ranging from the traditional implicit representation of knowledge in modal logic to the language of justification logic, which is capable of spelling out the internal inference process. We use these examples to divide representations of knowledge into logically omniscient and not logically omniscient, thus trying to determine how much information about the reasoning process needs to be present in a theory to avoid logical omniscience.     

Cell decomposition and definable functions for weak p‐adic structures

We develop a notion of cell decomposition suitable for studying weak p‐adic structures (reducts of p‐adic fields where addition and multiplication are not (everywhere) definable). As an example, we consider a structure with restricted addition.     

A relative interpolation theorem for infinitary universal Horn logic and its applications

In this paper we deal with infinitary universal Horn logic both with and without equality. First, we obtain a relative Lyndon-style interpolation theorem. Using this result, we prove a non-standard preservation theorem which contains, as a particular case, a Lyndon-style theorem on surjective homomorphisms in its Makkai-style formulation. Another consequence of the preservation theorem is a theorem on bimorphisms, which, in particular, provides a tool for immediate obtaining characterizations of infinitary universal Horn classes without equality from those with equality. From the theorem on surjective homomorphisms we also derive a non-standard Beth-style preservation theorem that yields a non-standard Beth-style definability theorem, according to which implicit definability of a relation symbol in an infinitary universal Horn theory implies its explicit definability by a conjunction of atomic formulas. We also apply our theorem on surjective homomorphisms, theorem on bimorphisms and definability theorem to algebraic logic for general propositional logic.     

Axiomatizing first-order consequences in dependence logic

Dependence logic, introduced in Väänänen (2007) [11], cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized, and this is what we shall do in this paper. We give an explicit axiomatization and prove the respective Completeness Theorem.     

On quasi‐varieties of multiple valued logic models

We extend the concept of quasi‐variety of first‐order models from classical logic to multiple valued logic (MVL) and study the relationship between quasi‐varieties and existence of initial models in MVL. We define a concept of ‘Horn sentence’ in MVL and based upon our study of quasi‐varieties of MVL models we derive the existence of initial models for MVL ‘Horn theories’. © 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim     

Inference of Probabilities over a Stochastic IL-System by Quantifier Elimination

An algebraic approach based on quantifier elimination is proposed for the inference of probabilistic parameters over stochastic Lindenmayer systems with interaction, IL-systems. We are concerned with a multi-cellular organism as an instance of a stochastic IL system. The organism starts with one or a few cells, and develops different types of cells with distinct functions. We have constructed a simple model with cell-type order conservation and have assessed conditions for high cell-type diversity. This model is based on the stochastic IL-system for three types of cells. The cell-type order conservation corresponds to interaction terms in the IL-system. In our model, we have successfully inferred algebraic relations between the probabilities for cell-type diversity by using a symbolic method, quantifier elimination (QE). Surprisingly, three modes for the proliferation and transition rates emerged for various ratios of the initial cells to the developed cells. Furthermore, we have found that the high cell-type diversity pattern originates from the cell-type order conservation. Thus, QE has yielded analysis of the IL-system, which has revealed that, during the developing process of multi-cellular organisms, complex but explicit relations exist between cell-type diversity patterns and developmental rates.      

Logic for abstract hoop twist-structures

In this paper, we introduce and study a logic that corresponds to abstract hoop twist-structures and present some results on this logic. We prove the local deductive theorem for this logic and show that this logic is algebraizable with respect to the quasi-variety of abstract hoop twist-structures.     

An optimal lower bound on the number of variables for graph identification

In this paper we show that (n) variables are needed for first-order logic with counting to identify graphs onn vertices. Thek-variable language with counting is equivalent to the (k–1)-dimensional Weisfeiler-Lehman method. We thus settle a long-standing open problem. Previously it was an open question whether or not 4 variables suffice. Our lower bound remains true over a set of graphs of color class size 4. This contrasts sharply with the fact that 3 variables suffice to identify all graphs of color class size 3, and 2 variables suffice to identify almost all graphs. Our lower bound is optimal up to multiplication by a constant becausen variables obviously suffice to identify graphs onn vertices.Research supported by NSF grant CCR-8709818.Research supported by NSF grant CCR-8805978 and Pennsylvania State University Research Initiation grant 428-45.Research supported by NSF grants DCR-8603346 and CCR-8806308.     

Quantifier elimination for elementary geometry and elementary affine geometry

We introduce new first‐order languages for the elementary n‐dimensional geometry and elementary n‐dimensional affine geometry (n ≥ 2), based on extending $\mathsf {FO}(\beta ,\equiv )$ and $\mathsf {FO}(\beta )$, respectively, with new function symbols. Here, β stands for the betweenness relation and ≡ for the congruence relation. We show that the associated theories admit effective quantifier elimination.     

Evidence and plausibility in neighborhood structures

The intuitive notion of evidence has both semantic and syntactic features. In this paper, we develop an evidence logic for epistemic agents faced with possibly contradictory evidence from different sources. The logic is based on a neighborhood semantics, where a neighborhood N indicates that the agent has reason to believe that the true state of the world lies in N. Further notions of relative plausibility between worlds and beliefs based on the latter ordering are then defined in terms of this evidence structure, yielding our intended models for evidence-based beliefs. In addition, we also consider a second more general flavor, where belief and plausibility are modeled using additional primitive relations, and we prove a representation theorem showing that each such general model is a p-morphic image of an intended one. This semantics invites a number of natural special cases, depending on how uniform we make the evidence sets, and how coherent their total structure. We give a structural study of the resulting ‘uniform’ and ‘flat’ models. Our main result are sound and complete axiomatizations for the logics of all four major model classes with respect to the modal language of evidence, belief and safe belief. We conclude with an outlook toward logics for the dynamics of changing evidence, and the resulting language extensions and connections with logics of plausibility change.     

Possible world semantics for first-order logic of proofs

In the tech report Artemov and Yavorskaya (Sidon) (2011) [4] an elegant formulation of the first-order logic of proofs was given, FOLP. This logic plays a fundamental role in providing an arithmetic semantics for first-order intuitionistic logic, as was shown. In particular, the tech report proved an arithmetic completeness theorem, and a realization theorem for FOLP. In this paper we provide a possible-world semantics for FOLP, based on the propositional semantics of Fitting (2005) [5]. We also give an Mkrtychev semantics. Motivation and intuition for FOLP can be found in Artemov and Yavorskaya (Sidon) (2011) [4], and are not fully discussed here.     

Quantifier‐eliminable locally finite graphs

We identify the locally finite graphs that are quantifier‐eliminable and their first order theories in the signature of distance predicates. © 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim     

SO(∀∃*) Sentences and Their Asymptotic Probabilities

We prove a 0‐1 law for the fragment of second order logic SO(∀∃*) over parametric classes of finite structures which allow only one unary atomic type. This completes the investigation of 0‐1 laws for fragments of second order logic defined in terms of first order quantifier prefixes over, e.g., simple graphs and tournaments. We also prove a low oscillation law, and establish the 0‐1 law for Σ¹₄(∀∃*) without any restriction on the number of unary types.