scholarly journals The Triguarded Fragment with Transitivity

10.29007/z359 ◽  
2020 ◽  
Author(s):  
Emanuel Kieronski ◽  
Adam Malinowski
Keyword(s):  
Decision Procedure ◽  
Order Logic ◽  
First Order Logic ◽  
Satisfiability Problem ◽  
First Order ◽  
Free Variables ◽  
Guarded Fragment

The triguarded fragment of first-order logic is an extension of the guarded fragment in which quantification for subformulas with at most two free variables need not be guarded. Thus, it unifies two prominent decidable logics: the guarded fragment and the two-variable fragment. Its satisfiability problem is known to be undecidable in the presence of equality, but becomes decidable when equality is forbidden. We consider an extension of the tri- guarded fragment without equality by transitive relations, allowing them to be used only as guards. We show that the satisfiability problem for the obtained formalism is decidable and 2-ExpTime-complete, that is, it is of the same complexity as for the analogous exten- sion of the classical guarded fragment. In fact, in our satisfiability test we use a decision procedure for the latter as a subroutine. We also show how our approach, consisting in exploiting some existing results on guarded logics, can be used to reprove some known facts, as well as to derive some other new results on triguarded logics.

Two variable first-order logic over ordered domains

2001 ◽  
Vol 66 (2) ◽  
pp. 685-702 ◽  
Author(s):  
Martin Otto
Keyword(s):  
Order Logic ◽  
Decision Problems ◽  
First Order Logic ◽  
Satisfiability Problem ◽  
Exponential Time ◽  
Infinite Domains ◽  
First Order ◽  
Computation Tree ◽  
Common Extension ◽  
Undecidability Result

AbstractThe satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations.It is shown that FO2 over ordered, respectively wellordered. domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially the same as for plain unconstrained FO2. namely non-deterministic exponential time.In contrast FO2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings. wellorderings. or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO2 and computation tree logic CTL.

The degree of the set of sentences of predicate provability logic that are true under every interpretation

1987 ◽  
Vol 52 (1) ◽  
pp. 165-171 ◽  
Author(s):  
George Boolos ◽  
Vann McGee
Keyword(s):  
Predicate Symbol ◽  
Order Logic ◽  
First Order Logic ◽  
Provability Logic ◽  
First Order ◽  
Free Variables ◽  
Unary Operator

The formalism of P(redicate) P(rovability) L(ogic) is the result of adjoining the unary operator □ to first-order logic without identity, constants, or function symbols. The term “provability” indicates that □ is to be “read” as “it is provable in P(eano) A(rithmetic) that…” and that the formulae of predicate provability logic are to be interpreted via formulae of PA as follows.Pr(x), alias Bew(x), is the standard provability predicate of PA. For any formula F of PA, Pr[F] is the formula of PA that expresses the PA-provability of F “of” the values of the variables free in F, i.e., it is the formula of PA with the same free variables as F that expresses the PA-provability of the result of substituting for each variable free in F the numeral for the value of that variable. For the details of the construction of Pr[F], the reader may consult [B2, p. 42]. If F is a sentence of PA, then Pr[F] = Pr(‘F’), the sentence that expresses the PA-provability of F.Let υ1, υ2,… be an enumeration of the variables of PA. An interpretation * of a formula ϕ of PPL is a function which assigns to each predicate symbol P of ϕ a formula P* of the language of arithmetic whose free variables are the first n variables of PA, where n is the degree of P.

On amalgamations of languages with Magidor-Malitz quantifiers

1979 ◽  
Vol 44 (4) ◽  
pp. 549-558
Author(s):  
Carl F. Morgenstern
Keyword(s):  
Universal Algebra ◽  
Model Theory ◽  
Natural Extension ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Free Variables ◽  
Countably Compact

In this paper we indicate how compact languages containing the Magidor-Malitz quantifiers Qκn in different cardinalities can be amalgamated to yield more expressive, compact languages.The language Lκ<ω, originally introduced by Magidor and Malitz [9], is a natural extension of the language L(Q) introduced by Mostowski and investigated by Fuhrken [6], [7], Keisler [8] and Vaught [13]. Intuitively, Lκ<ω is first-order logic together with quantifiers Qκn (n ∈ ω) binding n free variables which express “there is a set X of cardinality κ such than any n distinct elements of X satisfy …”, or in other words, iff the relation on determined by φ contains an n-cube of cardinality κ. With these languages one can express a variety of combinatorial statements of the type considered by Erdös and his colleagues, as well as concepts in universal algebra which are beyond the scope of first-order logic. The model theory of Lκ<ω has been further developed by Badger [1], Magidor and Malitz [10] and Shelah [12].We refer to a language as being < κ compact if, given any set of sentences Σ of the language, if Σ is finitely satisfiable and ∣Σ∣ < κ, then Σ has a model. The phrase countably compact is used in place of <ℵ1 compact.

scholarly journals Undecidable relativizations of algebras of relations

1999 ◽  
Vol 64 (2) ◽  
pp. 747-760 ◽  
Author(s):  
Szabolcs Mikulás ◽  
Maarten Marx
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Similarity Type ◽  
First Order ◽  
Equational Theories ◽  
Algebras Of Relations ◽  
Guarded Fragment ◽  
Cylindric Set Algebras

AbstractIn this paper we show that relativized versions of relation set algebras and cylindric set algebras have undecidable equational theories if we include coordinatewise versions of the counting operations into the similarity type. We apply these results to the guarded fragment of first-order logic.

Abstraction Logic

2021 ◽  
Author(s):  
Steven Obua
Keyword(s):  
Binding Constants ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Algebraic Semantics ◽  
Variable Binding ◽  
First Order ◽  
Free Variables ◽  
Direct Support ◽  
Second Order Logic

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.

Interpolation for extended modal languages

2005 ◽  
Vol 70 (1) ◽  
pp. 223-234 ◽  
Author(s):  
Balder ten Cate
Keyword(s):  
Difference Operator ◽  
Relation Algebra ◽  
Order Logic ◽  
Hybrid Logic ◽  
First Order Logic ◽  
Modal Language ◽  
First Order ◽  
Language L ◽  
Guarded Fragment

AbstractSeveral extensions of the basic modal language are characterized in terms of interpolation. Our main results are of the following form: Language L′ is the least expressive extension of L with interpolation. For instance, let ℳ(D) be the extension of the basic modal language with a difference operator [7], First-order logic is the least expressive extension of ℳ(D) with interpolation. These characterizations are subsequently used to derive new results about hybrid logic, relation algebra and the guarded fragment.

scholarly journals An elementary definability theorem for first order logic

1999 ◽  
Vol 64 (3) ◽  
pp. 1028-1036 ◽  
Author(s):  
C. Butz ◽  
I. Moerdijk
Keyword(s):  
Model Theory ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Free Variables ◽  
Definable Subset ◽  
Boolean Valued Model

In this paper, we will present a definability theorem for first order logic. This theorem is very easy to state, and its proof only uses elementary tools. To explain the theorem, let us first observe that if M is a model of a theory T in a language , then, clearly, any definable subset S ⊂ M (i.e., a subset S = {a ∣ M ⊨ φ(a)} defined by some formula φ) is invariant under all automorphisms of M. The same is of course true for subsets of Mn defined by formulas with n free variables.Our theorem states that, if one allows Boolean valued models, the converse holds. More precisely, for any theory T we will construct a Boolean valued model M, in which precisely the T -provable formulas hold, and in which every (Boolean valued) subset which is invariant under all automorphisms of M is definable by a formula .Our presentation is entirely selfcontained, and only requires familiarity with the most elementary properties of model theory. In particular, we have added a first section in which we review the basic definitions concerning Boolean valued models.

scholarly journals THE FLUTED FRAGMENT REVISITED

2019 ◽  
Vol 84 (3) ◽  
pp. 1020-1048
Author(s):  
IAN PRATT-HARTMANN ◽  
WIESŁAW SZWAST ◽  
LIDIA TENDERA
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Satisfiability Problem ◽  
Complexity Bounds ◽  
First Order ◽  
Complexity Results ◽  
Decidable Fragment ◽  
Image Position ◽  
Exponential Size

AbstractWe 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$.

Axiomatizability by a schema

1968 ◽  
Vol 32 (4) ◽  
pp. 473-479 ◽  
Author(s):  
Robert L. Vaught
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Relation Symbol ◽  
First Order ◽  
Free Variables

A theory T is axiomatizable by a schema if there is a formula Γ, involving symbols of T plus a new relation symbol R, such that the set of all (universal closures of) instances of Γ in T is a set of axioms for T. (It is understood that, if R has n places, an instance of Γ in T is obtained by properly substituting for R in Γ a formula of T which has n selected free variables and is allowed to have any number of other free variables as parameters.) Obviously, the notion is unchanged if finitely many Γ's, each involving several new R's, are allowed instead. All theories we consider are assumed to be theories in the first-order logic with equality (as in [8]), to have finitely many nonlogical symbols, and to be recursively axiomatizable.

scholarly journals Two-variable First-Order Logic with Counting in Forests

10.29007/24fm ◽  
2018 ◽  
Author(s):  
Witold Charatonik ◽  
Yegor Guskov ◽  
Ian Pratt-Hartmann ◽  
Piotr Witkowski
Keyword(s):  
Decision Procedure ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Satisfiability Problems

We consider an extension of two-variable, first-order logic with counting quantifiers and arbitrarily many unary and binary predicates, in which one distinguished predicate is interpreted as the mother-daughter relation in an unranked forest. We show that both the finite satisfiability and the general satisfiability problems for the extended logic are decidable in NExpTime. We also show that the decision procedure for finite satisfiability can be extended to the logic where two distinguished predicates are interpreted as the mother-daughter relations in two independent forests.

Sign in / Sign up

Export Citation Format

Share Document