An undecidable problem in correspondence theory

1991 ◽  
Vol 56 (4) ◽  
pp. 1261-1272 ◽  
Author(s):  
L. A. Chagrova
Keyword(s):  
Correspondence Theory ◽  
First Order ◽  
Undecidable Problem ◽  
First Order Definability ◽  
Effective Procedures

In this paper we prove undecidability of first-order definability of propositional formulas. The main result is proved for intuitionistic formulas, but it remains valid for other kinds of propositional formulas by analogous arguments or with the help of various translations.For general background on correspondence theory the reader is referred to van Benthem [1], [2] (see [3] for a survey of recent results).The method for the proofs of undecidability in this paper will be to simulate calculations of a Minsky machine by intuitionistic formulas. §3 concerns this simulation. Effective procedures for the construction of simulating modal formulas can be found in the literature (cf. [4]).The principal results of the paper are in §4. §5 gives some further undecidability results, that will be proved in another paper by modification of the method of this paper.I am indebted to the referee for drawing my attention to some errors in an earlier version of this paper.

scholarly journals Characterizing Boundedness in Chase Variants

2020 ◽  
Vol 21 (1) ◽  
pp. 51-79
Author(s):  
STATHIS DELIVORIAS ◽  
MICHEL LECLÈRE ◽  
MARIE-LAURE MUGNIER ◽  
FEDERICO ULLIANA
Keyword(s):  
Knowledge Bases ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Universal Models ◽  
Knowing That ◽  
Significant Interest ◽  
Horn Rules ◽  
Boundedness Problem ◽  
Undecidable Problem

AbstractExistential 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.

Simulating polyadic modal logics by monadic ones

2003 ◽  
Vol 68 (2) ◽  
pp. 419-462 ◽  
Author(s):  
George Goguadze ◽  
Carla Piazza ◽  
Yde Venema
Keyword(s):  
Modal Logics ◽  
Finite Model ◽  
Model Property ◽  
Finite Model Property ◽  
First Order ◽  
First Order Definability

AbstractWe define an interpretation of modal languages with polyadic operators in modal languages that use monadic operators (diamonds) only. We also define a simulation operator which associates a logic Λsim in the diamond language with each logic Λ in the language with polyadic modal connectives. We prove that this simulation operator transfers several useful properties of modal logics, such as finite/recursive axiomatizability, frame completeness and the finite model property, canonicity and first-order definability.

scholarly journals Functional first order definability of LRTP

2010 ◽  
Vol 14 (48) ◽  
Author(s):  
José Raymundo Marcial Romero ◽  
José Antonio Hernández
Keyword(s):  
First Order ◽  
First Order Definability

First-order definability

2004 ◽  
pp. 151-174
Author(s):  
Richard Lassaigne ◽  
Michel de Rougemont
Keyword(s):  
First Order ◽  
First Order Definability

Minimal predicates, fixed-points, and definability

2005 ◽  
Vol 70 (3) ◽  
pp. 696-712 ◽  
Author(s):  
Johan Van Benthem
Keyword(s):  
Mathematical Logic ◽  
Fixed Points ◽  
Expressive Power ◽  
Correspondence Theory ◽  
Order Logic ◽  
First Order Logic ◽  
Technical Result ◽  
Unique Existence ◽  
First Order ◽  
Preservation Theorem

AbstractMinimal predicates P satisfying a given first-order description ϕ(P) occur widely in mathematical logic and computer science. We give an explicit first-order syntax for special first-order ‘PIA conditions’ ϕ(P) which guarantees unique existence of such minimal predicates. Our main technical result is a preservation theorem showing PIA-conditions to be expressively complete for all those first-order formulas that are preserved under a natural model-theoretic operation of ‘predicate intersection’. Next, we show how iterated predicate minimization on PIA-conditions yields a language MIN(FO) equal in expressive power to LFP(FO), first-order logic closed under smallest fixed-points for monotone operations. As a concrete illustration of these notions, we show how our sort of predicate minimization extends the usual frame correspondence theory of modal logic, leading to a proper hierarchy of modal axioms: first-order-definable, first-order fixed-point definable, and beyond.

An undecidable problem in finite combinatorics

1984 ◽  
Vol 49 (3) ◽  
pp. 842-850 ◽  
Author(s):  
Kevin J. Compton
Keyword(s):  
Subject Area ◽  
Axiomatizable Class ◽  
First Order ◽  
Existence Proofs ◽  
Sorting Algorithms ◽  
Finite Structures ◽  
De Bruijn ◽  
Asymptotic Probability ◽  
Undecidable Problem

Problems of computing probabilities of statements about large, finite structures have become an important subject area of finite combinatorics. Within the last two decades many researchers have turned their attention to such problems and have developed a variety of methods for dealing with them. Applications of these ideas include nonconstructive existence proofs for graphs with certain properties by showing the properties occur with nonzero probabilities (for examples see Erdös and Spencer [ES] and Bollobás [Bo]), and determination of average running times for sorting algorithms by computing asymptotic probabilities of statements about permutations (see Knuth [Kn]). Two types of techniques recur in solutions to such problems: probabilistic techniques, such as those used by Erdös and Spencer [ES], and classical assymptotic techniques, such as those surveyed by Bender [Be] and de Bruijn [Br]. Studying this body of techniques, one notices that characteristics of these problems suggest certain methods of solution, in much the same way that the form of an integrand may suggest certain substitutions. The question arises, then, as to whether there is a systematic way to approach these problems: is there an algorithm for computing asymptotic probabilities? I will show that the answer is “no”—for any reasonable formulation, the problem of computing asymptotic probabilities is undecidable.The main theorem of the paper is Theorem 1.6, which says that there is a finitely axiomatizable class in which every first order sentence has an asymptotic probability of 0 or 1—i.e., is almost always true or almost always false in finite structures—but for which the problem of deciding whether a sentence has asymptotic probability 0 or 1 is undecidable. Heretofore, classes known to have such a 0-1 law have had decidable asymptotic probability problems (see Lynch [Ly] for examples and a discussion of previous work in the area).

Sign in / Sign up

Export Citation Format

Share Document