Search

Dialogues are turn-taking games which model debates about the satisfaction of logical formulas. A novel variant played over first-order structures gives rise to a notion of first-order satisfaction. We study the induced notion of validity for classical and intuitionistic first-order logic in the constructive setting of the calculus of inductive constructions. We prove that such material dialogue semantics for classical first-order logic admits constructive soundness and completeness proofs, setting it apart from standard model-theoretic semantics of first-order logic. Furthermore, we prove that completeness with regard to intuitionistic material dialogues fails in both constructive and classical settings. As an alternative, we propose material dialogues played over Kripke structures. These Kripke material dialogues exhibit constructive completeness when restricting to the negative fragment. The results concerning classical material dialogues have been mechanized using the Coq interactive theorem prover. [ABSTRACT FROM AUTHOR]

Sedlár and Vigiani [18] have developed an approach to propositional epistemic logics wherein (i) an agent's beliefs are closed under relevant implication and (ii) the agent is located in a classical possible world (i.e., the non-modal fragment is classical). Here I construct first-order extensions of these logics using the non-Tarskian interpretation of the quantifiers introduced by Mares and Goldblatt [12], and later extended to quantified modal relevant logics by Ferenz [6]. Modular soundness and completeness are proved for constant domain semantics, using non-general frames with Mares–Goldblatt truth conditions. I further detail the relation between the demand that classical possible worlds have Tarskian truth conditions and incompleteness results in quantified relevant logics. [ABSTRACT FROM AUTHOR]

We show that the first-order logical theory of the binary overlap-free words (and, more generally, the $\alpha $ -free words for rational $\alpha $ , $2), is decidable. As a consequence, many results previously obtained about this class through tedious case-based proofs can now be proved "automatically," using a decision procedure, and new claims can be proved or disproved simply by restating them as logical formulas. [ABSTRACT FROM AUTHOR]

Let $\mathscr {C}$ be a class of finite and infinite graphs that is closed under induced subgraphs. The well-known Łoś–Tarski Theorem from classical model theory implies that $\mathscr {C}$ is definable in first-order logic by a sentence $\varphi $ if and only if $\mathscr {C}$ has a finite set of forbidden induced finite subgraphs. This result provides a powerful tool to show nontrivial characterizations of graphs of small vertex cover, of bounded tree-depth, of bounded shrub-depth, etc. in terms of forbidden induced finite subgraphs. Furthermore, by the Completeness Theorem, we can compute from $\varphi $ the corresponding forbidden induced subgraphs. This machinery fails on finite graphs as shown by our results: – There is a class $\mathscr {C}$ of finite graphs that is definable in first-order logic and closed under induced subgraphs but has no finite set of forbidden induced subgraphs. – Even if we only consider classes $\mathscr {C}$ of finite graphs that can be characterized by a finite set of forbidden induced subgraphs, such a characterization cannot be computed from a first-order sentence $\varphi $ that defines $\mathscr {C}$ and the size of the characterization cannot be bounded by $f(|\varphi |)$ for any computable function f. Besides their importance in graph theory, the above results also significantly strengthen similar known theorems for arbitrary structures. [ABSTRACT FROM AUTHOR]

Researchers and practitioners are increasingly embracing systems approaches to deal with the complexity of public service delivery and policy evaluation. However, there is little agreement on what exactly constitutes a systems approach, conceptually or methodologically. We review and critically synthesize systems literature from the fields of health, education, and infrastructure. We argue that the common theoretical core of systems approaches is the idea that multi-dimensional complementarities between a policy and other aspects of the policy context are the first-order problem of policy design and evaluation. We distinguish between macro-systems approaches, which focus on the collective coherence of a set of policies or institutions, and micro-systems approaches, which focus on how a single policy interacts with the context in which it operates. We develop a typology of micro-systems approaches and discuss their relationship to standard impact evaluation methods as well as to work in external validity, implementation science, and complexity theory. [ABSTRACT FROM AUTHOR]

The one-variable fragment of a first-order logic may be viewed as an "S5-like" modal logic, where the universal and existential quantifiers are replaced by box and diamond modalities, respectively. Axiomatizations of these modal logics have been obtained for special cases—notably, the modal counterparts $\mathrm {S5}$ and $\mathrm {MIPC}$ of the one-variable fragments of first-order classical logic and first-order intuitionistic logic, respectively—but a general approach, extending beyond first-order intermediate logics, has been lacking. To this end, a sufficient criterion is given in this paper for the one-variable fragment of a semantically defined first-order logic—spanning families of intermediate, substructural, many-valued, and modal logics—to admit a certain natural axiomatization. More precisely, an axiomatization is obtained for the one-variable fragment of any first-order logic based on a variety of algebraic structures with a lattice reduct that has the superamalgamation property, using a generalized version of a functional representation theorem for monadic Heyting algebras due to Bezhanishvili and Harding. An alternative proof-theoretic strategy for obtaining such axiomatization results is also developed for first-order substructural logics that have a cut-free sequent calculus and admit a certain interpolation property. [ABSTRACT FROM AUTHOR]

Due to Gödel's incompleteness results, the categoricity of a sufficiently rich mathematical theory and the semantic completeness of its underlying logic are two mutually exclusive ideals. For first- and second-order logics we obtain one of them with the cost of losing the other. In addition, in both these logics the rules of deduction for their quantifiers are non-categorical. In this paper I examine two recent arguments—Warren [43] and Murzi and Topey [30]—for the idea that the natural deduction rules for the first-order universal quantifier are categorical, i.e., they uniquely determine its semantic intended meaning. Both of them make use of McGee's open-endedness requirement and the second one uses in addition Garson's [19] local models for defining the validity of these rules. I argue that the success of both these arguments is relative to their semantic or infinitary assumptions, which could be easily discharged if the introduction rule for the universal quantifier is taken to be an infinitary rule, i.e., non-compact. Consequently, I reconsider the use of the $\omega $ -rule and I show that the addition of the $\omega $ -rule to the standard formalizations of first-order logic is categorical. In addition, I argue that the open-endedness requirement does not make the first-order Peano Arithmetic categorical and I advance an argument for its categoricity based on the inferential conservativity requirement. [ABSTRACT FROM AUTHOR]

We present an adapted construction of algebraic circuits over the reals introduced by Cucker and Meer to arbitrary infinite integral domains and generalize the $\mathrm{AC}_{\mathbb{R}}$ and $\mathrm{NC}_{\mathbb{R}}^{}$ classes for this setting. We give a theorem in the style of Immerman's theorem which shows that for these adapted formalisms, sets decided by circuits of constant depth and polynomial size are the same as sets definable by a suitable adaptation of first-order logic. Additionally, we discuss a generalization of the guarded predicative logic by Durand, Haak and Vollmer, and we show characterizations for the $\mathrm{AC}_{R}$ and $\mathrm{NC}_R^{}$ hierarchy. Those generalizations apply to the Boolean $\mathrm{AC}$ and $\mathrm{NC}$ hierarchies as well. Furthermore, we introduce a formalism to be able to compare some of the aforementioned complexity classes with different underlying integral domains. [ABSTRACT FROM AUTHOR]

We extend the languages of both basic and graded modal logic with the infinity diamond, a modality that expresses the existence of infinitely many successors having a certain property. In both cases we define a natural notion of bisimilarity for the resulting formalisms, that we dub $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ , respectively. We then characterise these logics as the bisimulation-invariant fragments of the naturally corresponding predicate logic, viz., the extension of first-order logic with the infinity quantifier. Furthermore, for both $\mathtt {ML}^{\infty }$ and $\mathtt {GML}^{\infty }$ we provide a sound and complete axiomatisation for the set of formulas that are valid in every Kripke frame, we prove a small model property with respect to a widened class of weighted models, and we establish decidability of the satisfiability problem. [ABSTRACT FROM AUTHOR]

To answer database queries over incomplete data, the gold standard is finding certain answers: those that are true regardless of how incomplete data is interpreted. Such answers can be found efficiently for conjunctive queries and their unions, even in the presence of constraints. With negation added, the problem becomes intractable however. We concentrate on the complexity of certain answers under constraints and on effficiently answering queries outside the usual classes of (unions) of conjunctive queries by means of rewriting as Datalog and first-order queries. We first notice that there are three different ways in which query answering can be cast as a decision problem. We complete the existing picture and provide precise complexity bounds on all versions of the decision problem, for certain and best answers. We then study a well-behaved class of queries that extends unions of conjunctive queries with a mild form of negation. We show that for them, certain answers can be expressed in Datalog with negation, even in the presence of functional dependencies, thus making them tractable in data complexity. We show that in general, Datalog cannot be replaced by first-order logic, but without constraints such a rewriting can be done in first order. [ABSTRACT FROM AUTHOR]

Vardanyan's Theorems [36, 37] state that $\mathsf {QPL}(\mathsf {PA})$ —the quantified provability logic of Peano Arithmetic—is $\Pi ^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge [38] generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf {QRC_1}$ was previously introduced by the authors [1] as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf {QRC_1}$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf {QRC_1}$ is the strictly positive fragment of $\mathsf {QGL}$ and a fragment of $\mathsf {QPL}(\mathsf {PA})$. [ABSTRACT FROM AUTHOR]

We take Carnap's problem to be to what extent standard consequence relations in various formal languages fix the meaning of their logical vocabulary, alone or together with additional constraints on the form of the semantics. This paper studies Carnap's problem for basic modal logic. Setting the stage, we show that neighborhood semantics is the most general form of compositional possible worlds semantics, and proceed to ask which standard modal logics (if any) constrain the box operator to be interpreted as in relational Kripke semantics. Except when restricted to finite domains, no modal logic characterizes exactly the Kripkean interpretations of $\Box $. Moreover, we show that, in contrast with the case of first-order logic, the obvious requirement of permutation invariance is not adequate in the modal case. After pointing out some known facts about modal logics that nevertheless force the Kripkean interpretation, we focus on another feature often taken to embody the gist of modal logic: locality. We show that invariance under point-generated subframes (properly defined) does single out the Kripkean interpretations, but only among topological interpretations, not in general. Finally, we define a notion of bisimulation invariance—another aspect of locality—that, together with a reasonable closure condition, gives the desired general result. Along the way, we propose a new perspective on normal neighborhood frames as filter frames, consisting of a set of worlds equipped with an accessibility relation, and a free filter at every world. [ABSTRACT FROM AUTHOR]

In the classical theory of regular languages, the concept of recognition by profinite monoids is an important tool. Beyond regularity, Boolean spaces with internal monoids (BiMs) were recently proposed as a generalization. On the other hand, fragments of logic defining regular languages can be studied inductively via the so-called "Substitution Principle." In this paper, we make the logical underpinnings of this principle explicit and extend it to arbitrary languages using Stone duality. Subsequently, we show how it can be used to obtain topo-algebraic recognizers for classes of languages defined by a wide class of first-order logic fragments. This naturally leads to a notion of semidirect product of BiMs extending the classical such construction for profinite monoids. Our main result is a generalization of Almeida and Weil's Decomposition Theorem for semidirect products from the profinite setting to that of BiMs. This is a crucial step in a program to extend the profinite methods of regular language theory to the setting of complexity theory. [ABSTRACT FROM AUTHOR]

Inquisitive first-order logic, InqBQ , is a system which extends classical first-order logic with formulas expressing questions. From a mathematical point of view, formulas in this logic express properties of sets of relational structures. This paper makes two contributions to the study of this logic. First, we describe an Ehrenfeucht–Fraïssé game for InqBQ and show that it characterizes the distinguishing power of the logic. Second, we use the game to study cardinality quantifiers in the inquisitive setting. That is, we study what statements and questions can be expressed in InqBQ about the number of individuals satisfying a given predicate. As special cases, we show that several variants of the question how many individuals satisfy $\alpha (x)$ are not expressible in InqBQ , both in the general case and in restriction to finite models. [ABSTRACT FROM AUTHOR]

Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this article, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract data types. Term-level bindings are another kind of abstraction, and these are given an elegant and direct treatment within both proof theory and these extended logic programming languages. Logic programming has also inspired new results in proof theory, such as those involving polarity and focused proofs. These recent results provide a high-level means for presenting the differences between forward-chaining and backward-chaining style inferences. Anchoring logic programming in proof theory has also helped identify its connections and differences with functional programming, deductive databases, and model checking. [ABSTRACT FROM AUTHOR]

It is customary to expect from a logical system that it can be algebraizable, in the sense that an algebraic companion of the deductive machinery can always be found. Since the inception of da Costa's paraconsistent calculi, algebraic equivalents for such systems have been sought. It is known, however, that these systems are not self-extensional (i.e., they do not satisfy the replacement property). More than this, they are not algebraizable in the sense of Blok–Pigozzi. The same negative results hold for several systems of the hierarchy of paraconsistent logics known as Logics of Formal Inconsistency (LFIs). Because of this, several systems belonging to this class of logics are only characterizable by semantics of a non-deterministic nature. This paper offers a solution for two open problems in the domain of paraconsistency, in particular connected to algebraization of LFIs, by extending with rules several LFIs weaker than $C_1$ , thus obtaining the replacement property (that is, such LFIs turn out to be self-extensional). Moreover, these logics become algebraizable in the standard Lindenbaum–Tarski's sense by a suitable variety of Boolean algebras extended with additional operations. The weakest LFI satisfying replacement presented here is called RmbC, which is obtained from the basic LFI called mbC. Some axiomatic extensions of RmbC are also studied. In addition, a neighborhood semantics is defined for such systems. It is shown that RmbC can be defined within the minimal bimodal non-normal logic $\mathbf {E} {\oplus } \mathbf {E}$ defined by the fusion of the non-normal modal logic E with itself. Finally, the framework is extended to first-order languages. RQmbC, the quantified extension of RmbC, is shown to be sound and complete w.r.t. the proposed algebraic semantics. [ABSTRACT FROM AUTHOR]

We present a natural standard translation of inquisitive modal logic $\mathrm{InqML}$ into first-order logic over the natural two-sorted relational representations of the intended models, which captures the built-in higher-order features of $\mathrm{InqML}$. This translation is based on a graded notion of flatness that ties the inherent second-order, team-semantic features of $\mathrm{InqML}$ over information states to subsets or tuples of bounded size. A natural notion of pseudo-models, which relaxes the non-elementary constraints on the intended models, gives rise to an elementary, purely model-theoretic proof of the compactness property for $\mathrm{InqML}$. Moreover, we prove a Hennessy-Milner theorem for $\mathrm{InqML}$ , which crucially uses $\omega $ -saturated pseudo-models and the new standard translation. As corollaries we also obtain van Benthem style characterisation theorems. [ABSTRACT FROM AUTHOR]

In 1978, Yu. F. Borisov presented an axiom system using a few basic assumptions and four explicit axioms, the fourth being a formulation of the relativity principle, and he demonstrated that this axiom system had (up to choice of units) only two models: a relativistic one in which worldview transformations are Poincaré transformations and a classical one in which they are Galilean. In this paper, we reformulate Borisov's original four axioms within an intuitively simple, but strictly formal, first-order logic framework, and convert his basic background assumptions into explicit axioms. Instead of assuming that the structure of physical quantities is the field of real numbers, we assume only that they form an ordered field. This allows us to investigate how Borisov's theorem depends on the structure of quantities. We demonstrate (as our main contribution) how to construct Euclidean, Galilean, and Poincaré models of Borisov's axiom system over every non-Archimedean field. We also demonstrate the existence of an infinite descending chain of models and transformation groups in each of these three cases, something that is not possible over Archimedean fields. As an application, we note that there is a model of Borisov's axioms that satisfies the relativity principle, and in which the worldview transformations are Euclidean isometries. Over the field of reals it is easy to eliminate this model using natural axioms concerning time's arrow and the absence of instantaneous motion. In the case of non-Archimedean fields, however, the Euclidean isometries appear intrinsically as worldview transformations in models of Borisov's axioms, and neither the assumption of time's arrow, nor the rejection of instantaneous motion, can eliminate them. [ABSTRACT FROM AUTHOR]

We investigate the modal logic of stepwise removal of objects, both for its intrinsic interest as a logic of quantification without replacement, and as a pilot study to better understand the complexity jumps between dynamic epistemic logics of model transformations and logics of freely chosen graph changes that get registered in a growing memory. After introducing this logic (MLSR) and its corresponding removal modality, we analyze its expressive power and prove a bisimulation characterization theorem. We then provide a complete Hilbert-style axiomatization for the logic of stepwise removal in a hybrid language enriched with nominals and public announcement operators. Next, we show that model-checking for MLSR is PSPACE-complete, while its satisfiability problem is undecidable. Lastly, we consider an issue of fine-structure: the expressive power gained by adding the stepwise removal modality to fragments of first-order logic. [ABSTRACT FROM AUTHOR]

Description logics (DLs) are well-known knowledge representation formalisms focused on the representation of terminological knowledge. Due to their first-order semantics, these languages (in their classical form) are not suitable for representing and handling uncertainty. A probabilistic extension of a light-weight DL was recently proposed for dealing with certain knowledge occurring in uncertain contexts. In this paper, we continue that line of research by introducing the Bayesian extension of the propositionally closed DL. We present a tableau-based procedure for deciding consistency and adapt it to solve other probabilistic, contextual, and general inferences in this logic. We also show that all these problems remain ExpTime-complete, the same as reasoning in the underlying classical. [ABSTRACT FROM AUTHOR]

One of the central logical ideas in Wittgenstein's Tractatus logico-philosophicus is the elimination of the identity sign in favor of the so-called "exclusive interpretation" of names and quantifiers requiring different names to refer to different objects and (roughly) different variables to take different values. In this paper, we examine a recent development of these ideas in papers by Kai Wehmeier. We diagnose two main problems of Wehmeier's account, the first concerning the treatment of individual constants, the second concerning so-called "pseudo-propositions" (Scheinsätze) of classical logic such as a = a or a = b ∧ b = c → a = c. We argue that overcoming these problems requires two fairly drastic departures from Wehmeier's account: (1) Not every formula of classical first-order logic will be translatable into a single formula of Wittgenstein's exclusive notation. Instead, there will often be a multiplicity of possible translations, revealing the original "inclusive" formulas to be ambiguous. (2) Certain formulas of first-order logic such as a = a will not be translatable into Wittgenstein's notation at all, being thereby revealed as nonsensical pseudo-propositions which should be excluded from a "correct" conceptual notation. We provide translation procedures from inclusive quantifier-free logic into the exclusive notation that take these modifications into account and define a notion of logical equivalence suitable for assessing these translations. [ABSTRACT FROM AUTHOR]

The 3-valued paraconsistent logic Ciore was developed by Carnielli, Marcos and de Amo under the name LFI2, in the study of inconsistent databases from the point of view of logics of formal inconsistency (LFIs). They also considered a first-order version of Ciore called LFI2*. The logic Ciore enjoys extreme features concerning propagation and retropropagation of the consistency operator: a formula is consistent if and only if some of its subformulas is consistent. In addition, Ciore is algebraizable in the sense of Blok and Pigozzi. On the other hand, the logic LFI2* satisfies a somewhat counter-intuitive property: the universal and the existential quantifier are inter-definable by means of the paraconsistent negation, as it happens in classical first-order logic with respect to the classical negation. This feature seems to be unnatural, given that both quantifiers have the classical meaning in LFI2*, and that this logic does not satisfy the De Morgan laws with respect to its paraconsistent negation. The first goal of the present article is to introduce a first-order version of Ciore (which we call QCiore) preserving the spirit of Ciore, that is, without introducing unexpected relationships between the quantifiers. The second goal of the article is to adapt to QCiore the partial structures semantics for the first-order paraconsistent logic LPT1 introduced by Coniglio and Silvestrini, which generalizes the semantic notion of quasi-truth considered by Mikeberg, da Costa and Chuaqui. Finally, some important results of classical Model Theory are obtained for this logic, such as Robinson's joint consistency theorem, amalgamation and interpolation. Although we focus on QCiore, this framework can be adapted to other 3-valued first-order LFIs. [ABSTRACT FROM AUTHOR]

Inquisitive modal logic, InqML, is a generalisation of standard Kripke-style modal logic. In its epistemic incarnation, it extends standard epistemic logic to capture not just the information that agents have, but also the questions that they are interested in. Technically, InqML fits within the family of logics based on team semantics. From a model-theoretic perspective, it takes us a step in the direction of monadic second-order logic, as inquisitive modal operators involve quantification over sets of worlds. We introduce and investigate the natural notion of bisimulation equivalence in the setting of InqML. We compare the expressiveness of InqML and first-order logic in the context of relational structures with two sorts, one for worlds and one for information states, and characterise inquisitive modal logic as the bisimulation invariant fragment of first-order logic over various natural classes of two-sorted structures. [ABSTRACT FROM AUTHOR]

Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks, and models for concurrency. LL's cut-elimination and the completeness of focusing are two of its fundamental properties that have been exploited in such applications. This paper formalizes the proof of cut-elimination for focused LL. For that, we propose a set of five cut-rules that allows us to prove cut-elimination directly on the focused system. We also encode the inference rules of other logics as LL theories and formalize the necessary conditions for those logics to have cut-elimination. We then obtain, for free, cut-elimination for first-order classical, intuitionistic, and variants of LL. We also use the LL metatheory to formalize the relative completeness of natural deduction and sequent calculus in first-order minimal logic. Hence, we propose a framework that can be used to formalize fundamental properties of logical systems specified as LL theories. [ABSTRACT FROM AUTHOR]

Existential rules are a positive fragment of first-order logic that generalizes function-free Horn rules by allowing existentially quantified variables in rule heads. This family of languages has recently attracted significant interest in the context of ontology-mediated query answering. Forward chaining, also known as the chase, is a fundamental tool for computing universal models of knowledge bases, which consist of existential rules and facts. Several chase variants have been defined, which differ on the way they handle redundancies. A set of existential rules is bounded if it ensures the existence of a bound on the depth of the chase, independently from any set of facts. Deciding if a set of rules is bounded is an undecidable problem for all chase variants. Nevertheless, when computing universal models, knowing that a set of rules is bounded for some chase variant does not help much in practice if the bound remains unknown or even very large. Hence, we investigate the decidability of the k-boundedness problem, which asks whether the depth of the chase for a given set of rules is bounded by an integer k. We identify a general property which, when satisfied by a chase variant, leads to the decidability of k-boundedness. We then show that the main chase variants satisfy this property, namely the oblivious, semi-oblivious (aka Skolem), and restricted chase, as well as their breadth-first versions. [ABSTRACT FROM AUTHOR]

We introduce the framework of AECats (abstract elementary categories), generalizing both the category of models of some first-order theory and the category of subsets of models. Any AEC and any compact abstract theory ("cat", as introduced by Ben-Yaacov) forms an AECat. In particular, we find applications in positive logic and continuous logic: the category of (subsets of) models of a positive or continuous theory is an AECat. The Kim–Pillay theorem for first-order logic characterizes simple theories by the properties dividing independence has. We prove a version of the Kim–Pillay theorem for AECats with the amalgamation property, generalizing the first-order version and existing versions for positive logic. [ABSTRACT FROM AUTHOR]

This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas. [ABSTRACT FROM AUTHOR]

Many philosophers take purportedly logical cases of ground (such as a true disjunction being grounded in its true disjunct(s)) to be obvious cases, and indeed such cases have been used to motivate the existence of and importance of ground. I argue against this. I do so by motivating two kinds of semantic determination relations. Intuitions of logical ground track these semantic relations. Moreover, our knowledge of semantics for (e.g.) first order logic can explain why we have such intuitions. And, I argue, neither semantic relation can be a species of ground even on a quite broad conception of what ground is. Hence, without a positive argument for taking so-called 'logical ground' to be something distinct from a semantic determination relation, we should cease treating logical cases as cases of ground. [ABSTRACT FROM AUTHOR]

Processing programs as data is one of the successes of functional and logic programming. Higher-order functions, as program-processing programs are called in functional programming, and meta-programs, as they are called in logic programming, are widespread declarative programming techniques. In logic programming, there is a gap between the meta-programming practice and its theory: The formalizations of meta-programming do not explicitly address its impredicativity and are not fully adequate. This article aims at overcoming this unsatisfactory situation by discussing the relevance of impredicativity to meta-programming, by revisiting former formalizations of meta-programming, and by defining Reflective Predicate Logic, a conservative extension of first-order logic, which provides a simple formalization of meta-programming. [ABSTRACT FROM AUTHOR]

Existing approaches to testing for the efficiency of a given portfolio make strong parametric assumptions about investor preferences and return distributions. Stochastic dominance-based procedures promise a useful nonparametric alternative. However, these procedures have been limited to considering binary choices. In this paper we take a new approach that considers all diversified portfolios and thereby introduce a new concept of first-order stochastic dominance (FSD) optimality of a given portfolio relative to all possible portfolios. Using our new test, we show that the U.S. stock market portfolio is significantly FSD nonoptimal relative to benchmark portfolios formed on market capitalization and book-to-market equity ratios. Without appealing to parametric assumptions about the return distribution, we conclude that no nonsatiable investor would hold the market portfolio in the face of the attractive premia of small caps and value stocks. [ABSTRACT FROM AUTHOR]

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$ , the intersection of the fluted fragment and the m -variable fragment of first-order logic, for all $m \ge 1$. We show that, for $m \ge 2$ , this subfragment forces $\left\lfloor {m/2} \right\rfloor$ -tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$ - NExpTime -hard. We further establish that, for $m \ge 3$ , any satisfiable ${\cal F}{{\cal L}^m}$ -formula has a model of at most ( $m - 2$)-tuply exponential size, whence the satisfiability (= finite satisfiability) problem for this fragment is in ( $m - 2$)- NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for ${\cal F}{{\cal L}^m}$ for all $m \le 4$. [ABSTRACT FROM AUTHOR]

In Team Semantics, a dependency notion is strongly first order if every sentence of the logic obtained by adding the corresponding atoms to First-Order Logic is equivalent to some first-order sentence. In this work it is shown that all nontrivial dependency atoms that are strongly first order, downwards closed, and relativizable (in the sense that the relativizations of the corresponding atoms with respect to some unary predicate are expressible in terms of them) are definable in terms of constancy atoms. Additionally, it is shown that any strongly first-order dependency is safe for any family of downwards closed dependencies, in the sense that every sentence of the logic obtained by adding to First-Order Logic both the strongly first-order dependency and the downwards closed dependencies is equivalent to some sentence of the logic obtained by adding only the downwards closed dependencies. [ABSTRACT FROM AUTHOR]

Stream processing has reached the mainstream in the last years, as a new generation of open-source distributed stream processing systems, designed for scaling horizontally on commodity hardware, has brought the capability for processing high-volume and high-velocity data streams to companies of all sizes. In this work, we propose a combination of temporal logic and property-based testing (PBT) for dealing with the challenges of testing programs that employ this programming model. We formalize our approach in a discrete time temporal logic for finite words, with some additions to improve the expressiveness of properties, which includes timeouts for temporal operators and a binding operator for letters. In particular, we focus on testing Spark Streaming programs written with the Spark API for the functional language Scala, using the PBT library ScalaCheck. For that we add temporal logic operators to a set of new ScalaCheck generators and properties, as part of our testing library sscheck. [ABSTRACT FROM AUTHOR]

The Decision Model and Notation (DMN) is a recent Object Management Group standard for the elicitation and representation of decision models and for managing their interconnection with business processes. DMN builds on the notion of decision tables and their combination into more complex decision requirements graphs (DRGs), which bridge between business process models and decision logic models. DRGs may rely on additional, external business knowledge models, whose functioning is not part of the standard. In this work, we consider one of the most important types of business knowledge, namely, background knowledge that conceptually accounts for the structural aspects of the domain of interest, and propose decision knowledge bases (DKBs), which semantically combine DRGs modeled in DMN, and domain knowledge captured by means of first-order logic with datatypes. We provide a logic-based semantics for such an integration, and formalize different DMN reasoning tasks for DKBs. We then consider background knowledge formulated as a description logic (DL) ontology with datatypes, and show how the main verification tasks for DMN in this enriched setting can be formalized as standard DL reasoning services and actually carried out in ExpTime. We discuss the effectiveness of our framework on a case study in maritime security. [ABSTRACT FROM AUTHOR]

First-order formalisations are often preferred to propositional ones because they are thought to underwrite the validity of more arguments. We compare and contrast the ability of some well-known logics—these two in particular—to formally capture valid and invalid arguments. We show that there is a precise and important sense in which first-order logic does not improve on propositional logic in this respect. We also prove some generalisations and related results of philosophical interest. The rest of the article investigates the results' philosophical significance. A first moral is that the correct way to state the oft-cited superiority of first-order logic vis- à -vis propositional logic is more nuanced than often thought. The second moral concerns semantic theory; the third logic's use as a tool for discovery. A fourth and final moral is that second-order logic's transcendence of first-order logic is greater than first-order logic's transcendence of propositional logic. [ABSTRACT FROM AUTHOR]

Givant [6] generalized the notion of an atomic pair-dense relation algebra from Maddux [13] by defining the notion of a measurable relation algebra , that is to say, a relation algebra in which the identity element is a sum of atoms that can be measured in the sense that the "size" of each such atom can be defined in an intuitive and reasonable way (within the framework of the first-order theory of relation algebras). In Andréka--Givant [2], a large class of examples of such algebras is constructed from systems of groups, coordinated systems of isomorphisms between quotients of the groups, and systems of cosets that are used to "shift" the operation of relative multiplication. In Givant--Andréka [8], it is shown that the class of these full coset relation algebras is adequate to the task of describing all measurable relation algebras in the sense that every atomic and complete measurable relation algebra is isomorphic to a full coset relation algebra. Call an algebra $\mathfrak{A}$ a coset relation algebra if $\mathfrak{A}$ is embeddable into some full coset relation algebra. In the present article, it is shown that the class of coset relation algebras is equationally axiomatizable (that is to say, it is a variety), but that no finite set of sentences suffices to axiomatize the class (that is to say, the class is not finitely axiomatizable). [ABSTRACT FROM AUTHOR]

The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this article we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics. [ABSTRACT FROM AUTHOR]

We provide algebraic conditions ensuring the decidability of the theory of modules over effectively given Prüfer (in particular Bézout) domains with infinite residue fields in terms of a suitable generalization of the prime radical relation. For Bézout domains these conditions are also necessary. [ABSTRACT FROM AUTHOR]

We study universal minimal flows of the homeomorphism groups of generalized Ważewski dendrites W P , $P \subseteq \left\{ {3,4, \ldots ,\omega } \right\}$. If P is finite, we prove that the universal minimal flow of the homeomorphism group H (W P ) is metrizable and we compute it explicitly. This answers a question of Duchesne. If P is infinite, we show that the universal minimal flow of H (W P ) is not metrizable. This provides examples of topological groups which are Roelcke precompact and have a nonmetrizable universal minimal flow with a comeager orbit. [ABSTRACT FROM AUTHOR]

In this article, we will show that ${\rm{R}}{{\rm{T}}^2} + WK{L_0}$ is a ${\rm{\Pi }}_1^1$ -conservative extension of ${\rm{B\Sigma }}_3^0$. [ABSTRACT FROM AUTHOR]

The study of algebraic modelling of labelled non-deterministic concurrent processes leads us to consider a category LB, obtained from a complete meet-semilattice B and from B-valued equivalence relations. We prove that, if B has enough properties, then LB presents a two-fold internal logical structure, induced by two doctrines definable on it: one related to its families of subobjects and one to its families of regular subobjects. The first doctrine is Heyting and makes LB a Heyting category, the second one is Boolean. We will see that the difference between these two logical structures, namely the different behaviour of the negation operator, can be interpreted in terms of a distinction between non-deterministic and deterministic behaviours of agents able to perform computations in the context of the same process. Moreover, the sorted first-order logic naturally associated with LB can be extended to a modal/temporal logic, again using the doctrinal setting. Relations are also drawn to other computational models. [ABSTRACT FROM AUTHOR]

It is well known that Gödel’s incompleteness theorems hold for ∑1-definable theories containing Peano arithmetic. We generalize Gödel’s incompleteness theorems for arithmetically definable theories. First, we prove that every ∑n+1-definable ∑n-sound theory is incomplete. Secondly, we generalize and improve Jeroslow and Hájek’s results. That is, we prove that every consistent theory having ∏n+1 set of theorems has a true but unprovable ∏n sentence. Lastly, we prove that no ∑n+1-definable ∑n -sound theory can prove its own ∑n-soundness. These three results are generalizations of Rosser’s improvement of the first incompleteness theorem, Gödel’s first incompleteness theorem, and the second incompleteness theorem, respectively. [ABSTRACT FROM AUTHOR]

This article introduces a new reflection principle. It is based on the idea that whatever is true in all entities of some kind is also true in a set-sized collection of them. Unlike standard reflection principles, it does not re-interpret parameters or predicates. This allows it to be both consistent in all higher-order languages and remarkably strong. For example, I show that in the language of second-order set theory with predicates for a satisfaction relation, it is consistent relative to the existence of a 2-extendible cardinal (Theorem 7.12) and implies the existence of a proper class of 1-extendible cardinals (Theorem 7.9). [ABSTRACT FROM AUTHOR]

We present abstract complexity results about Coquand and Hyland–Ong game semantics, that will lead to new bounds on the length of first-order cut-elimination, normalization, interaction between expansion trees and any other dialogical process game semantics can model and apply to. In particular, we provide a novel method to bound the length of interactions between visible strategies and to measure precisely the tower of exponentials defining the worst-case complexity. Our study improves the old estimates on average by several exponentials. [ABSTRACT FROM PUBLISHER]