Decidability of the Natural Numbers with the Almost-All Quantifier

Decidability of definability

For a fixed countably infinite structure Γ with finite relational signature τ, we study the following computational problem: input are quantifier-free τ-formulas ϕ_0,ϕ_1,...,ϕ_n that define relations R_0,R_1,...,R_n over Γ. The question is whether the relation R_0 is primitive positive definable from R_1,...,R_n, i.e., definable by a first-order formula that uses only relation symbols for R_1,..., R_n, equality, conjunctions, and existential quantification (disjunction, negation, and universal quantification are forbidden). We show decidability of this problem for all structures Γ that have a …

近自由代数：从词问题到消去量词

Almost free algebras: from the word problem to elimination of quantifiers

本文研究近自由代数的多项式时间可解性，包括词问题、同余类基数计算及同构检查等，同时证明其可通过扩展语言实现量词消去。

Bundled fragments of first-order modal logic: (un)decidability

Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the doma…

On Decidability Properties of One-Dimensional Cellular Automata

In a recent paper Sutner proved that the first-order theory of the phase-space $\mathcal{S}_\mathcal{A}=(Q^\mathbb{Z}, \longrightarrow)$ of a one-dimensional cellular automaton $\mathcal{A}$ whose configurations are elements of $Q^\mathbb{Z}$, for a finite set of states $Q$, and where $\longrightarrow$ is the "next configuration relation", is decidable. He asked whether this result could be extended to a more expressive logic. We prove in this paper that this is actuallly the case. We first show that, for each one-dimensional cellular automaton $\mathcal{A}$, the phase-space $\mathcal{S}_\math…

带有测度和范畴量词的一元二阶逻辑

Monadic Second Order Logic with Measure and Category Quantifiers

本文研究了在无限词和树上，将一元二阶逻辑扩展为带有基于贝尔范畴和勒贝格测度的广义“几乎全部”量词，探讨其表达能力和性质。

Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality

Uniform one-dimensional fragment UF1^= is a formalism obtained from first-order logic by limiting quantification to applications of blocks of existential (universal) quantifiers such that at most one variable remains free in the quantified formula. The fragment is closed under Boolean operations, but additional restrictions (called uniformity conditions) apply to combinations of atomic formulas with two or more variables. The fragment can be seen as a canonical generalization of two-variable logic, defined in order to be able to deal with relations of arbitrary arities. The fragment was introd…

Conditional probability logic, lifted bayesian networks and almost sure quantifier elimination

We introduce a formal logical language, called conditional probability logic (CPL), which extends first-order logic and which can express probabilities, conditional probabilities and which can compare conditional probabilities. Intuitively speaking, although formal details are different, CPL can express the same kind of statements as some languages which have been considered in the artificial intelligence community. We also consider a way of making precise the notion of lifted Bayesian network, where this notion is a type of (lifted) probabilistic graphical model used in machine learning, data…

One-dimensional fragment of first-order logic

We introduce a novel decidable fragment of first-order logic. The fragment is one-dimensional in the sense that quantification is limited to applications of blocks of existential (universal) quantifiers such that at most one variable remains free in the quantified formula. The fragment is closed under Boolean operations, but additional restrictions (called uniformity conditions) apply to combinations of atomic formulae with two or more variables. We argue that the notions of one-dimensionality and uniformity together offer a novel perspective on the robust decidability of modal logics. We also…

Espaços pseudo-topológicos e descrições do conceito de plausível

The structure of almost topological space is a variation of the concept of topological space. It emerged as a formalization of a quantifier first order not definable from the usual existential and universal operators, named the quantifier of the plausible. Later, it sought a formalization in propositional logical context, given a deductive and axiomatic system with algebraic model. We will present these formal conceptions and as an original contribution, we describe the propositional version of the logic of almost topological spaces in tableaux.

First-Order Model Checking on Generalisations of Pushdown Graphs

We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in doubly exponential alternating time with linearly many alternations. First-order logic with regular reachability predicates is uniformly decidable on level 2 collapsible pushdown graphs. Moreover, nest…

带后继函数的完全n分支序数树的初等理论

The elementary theory of full $n$-branching ordinal trees with successor functions

该论文研究带后继函数的完全n分支序数树的初等理论，对标准树按初等等价分类，建立量词消去与可判定性结果，还发展可实现性理论并澄清树与一元二阶逻辑的关系。

超越受限量词坍缩的嵌入有限模型

Embedded Finite Models Beyond Restricted Quantifier Collapse

该研究突破嵌入有限模型论的两种极端认知，证明可判定结构内逻辑求值复杂度范围极广且表达能力与复杂度可脱节，还证实有限域等理论不满足量词坍缩并给出域理论判定复杂度新下界。

Computation in Logic and Logic in Computation

The theory of addition in the domains of natural (N), integer (Z), rational (Q), real (R) and complex (C) numbers is decidable, so is the theory of multiplication in all those domains. By Godel's Incompleteness Theorem the theory of addition and multiplication is undecidable in the domains of N, Z and Q, though Tarski proved that this theory is decidable in the domains of R and C. The theory of multiplication and order (x,<) behaves differently in the above mentioned domains of numbers. By a theorem of Robinson, addition is definable by multiplication and order in the domain of natural numbers…

On the Remarkable Features of Binding Forms

Hilbert's Entscheidungsproblem has given rise to a broad and productive line of research in mathematical logic, where the classification process of decidable classes of first-order sentences represent only one of the remarkable results. According to the criteria used to identify the particular classes of interest, this process was declined into several research programs, of which some of the most deeply investigated are the ones classifying sentences in prenex normal form in base of their prefix vocabulary. Unfortunately, almost all of these approaches did not shed any light on the reasons why…