Search

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]

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]

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]

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]

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]

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]

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]

We use axioms of abstract ternary relations to define the notion of a free amalgamation theory. These form a subclass of first-order theories, without the strict order property, encompassing many prominent examples of countable structures in relational languages, in which the class of algebraically closed substructures is closed under free amalgamation. We show that any free amalgamation theory has elimination of hyperimaginaries and weak elimination of imaginaries. With this result, we use several families of well-known homogeneous structures to give new examples of rosy theories. We then prove that, for free amalgamation theories, simplicity coincides with NTP2 and, assuming modularity, with NSOP3 as well. We also show that any simple free amalgamation theory is 1-based. Finally, we prove a combinatorial characterization of simplicity for Fraïssé limits with free amalgamation, which provides new context for the fact that the generic Kn-free graphs are SOP3, while the higher arity generic $K_n^r$-free r-hypergraphs are simple. [ABSTRACT FROM PUBLISHER]

Presburger arithmetic is the first-order theory of the natural numbers with addition (but no multiplication). We characterize sets that can be defined by a Presburger formula as exactly the sets whose characteristic functions can be represented by rational generating functions; a geometric characterization of such sets is also given. In addition, if p = (p1, . . . , pn) are a subset of the free variables in a Presburger formula, we can define a counting function g(p) to be the number of solutions to the formula, for a given p. We show that every counting function obtained in this way may be represented as, equivalently, either a piecewise quasi-polynomial or a rational generating function. Finally, we translate known computational complexity results into this setting and discuss open directions. [ABSTRACT FROM PUBLISHER]

This paper considers Henkin’s proof of completeness of classical first-order logic and extends its scope to the realm of algebraizable logics in the sense of Blok and Pigozzi. Given a propositional logic L (for which we only need to assume that it has an algebraic semantics and a suitable disjunction) we axiomatize two natural first-order extensions L∀m and L∀ and prove that the former is complete with respect to all models over algebras from , while the latter is complete with respect to all models over relatively finitely subdirectly irreducible algebras. While the first completeness result is relatively straightforward, the second requires non-trivial modifications of Henkin’s proof by making use of the disjunction connective. As a byproduct, we also obtain a form of Skolemization provided that the algebraic semantics admits regular completions. The relatively modest assumptions on the propositional side allow for a wide generalization of previous approaches by Rasiowa, Sikorski, Hájek, Horn, and others and help to illuminate the “essentially first-order” steps in the classical Henkin’s proof. [ABSTRACT FROM PUBLISHER]

We examine the reverse-mathematical strength of several theorems in classical and effective model theory concerning first-order theories and their number of models. We prove that, among these, most are equivalent to one of the familiar systems RCA0, WKL0, or ACA0. We are led to a purely model-theoretic statement that implies WKL0 but refutes ACA0 over RCA0. [ABSTRACT FROM AUTHOR]

The set theory KPΠN+1 for ΠN+1-reflecting universes is shown to be ΠN+1-conservative over iterations of ΠN-recursively Mahlo operations for each N ≥ 2. [ABSTRACT FROM AUTHOR]

Let κ be the cardinality of some saturated model of Peano Arithmetic. There is a set of 2N0 saturated models of PA. each having cardinality κ, such that whenever M and N are two distinct models from this set, then Aut(M) ≇ Aut(N). [ABSTRACT FROM AUTHOR]

Glivenko's theorem states that an arbitrary propositional formula is classically provable if and only if its double negation is intuitionistically provable. The result does not extend to full first-order predicate logic, but does extend to first-order predicate logic without the universal quantifier. A recent paper by Zdanowski shows that Glivenko's theorem also holds for second-order propositional logic without the universal quantifier. We prove that Glivenko's theorem extends to some versions of simple type theory without the universal quantifier. Moreover, we prove that Kuroda's negative translation, which is known to embed classical first-order logic into intuitionistic first-order logic, extends to the same versions of simple type theory. We also prove that the Glivenko property fails for simple type theory once a weak form of functional extensionality is included. [ABSTRACT FROM AUTHOR]

This paper is devoted to o-minimalism, the study of the first-order properties of o-minimal structures. The main protagonists are the pseudo-o-minimal structures, that is to say the models of the theory of all o-minimal ¿-structures, but we start with a more in-depth analysis of the well-known fragment DCTC (Definable Completeness/Type Completeness), and show how it already admits many of the properties of o-minimal structures: dimension theory, monotonicity. Hardy structures, and quasi-cell decomposition, provided one replaces finiteness by discreteness in all of these. Failure of cell decomposition leads to the related notion of a eukaryote structure, and we give a criterium for a pseudo-o-minimal structure to be eukaryote. To any pseudo-o-minimal structure, we can associate its Grothendieck ring, which in the non-o-minimal case is a nontrivial invariant. To study this invariant, we identify a third o-minimalistic property, the Discrete Pigeonhole Principle, which in turn allows us to define discretely valued Euler characteristics. As an application, we study certain analytic subsets, called Taylor sets. [ABSTRACT FROM AUTHOR]

Hirsch and Hodkinson proved, for 3 ≤ m < ω and any k < ω. that the class SNrmCAm+k+1 is strictly contained in SNrmCAm+k and if A k ≥ 1 then the former class cannot be defined by any finite set of first-order formulas, within the latter class. We generalize this result to the following algebras of m-ary relations for which the neat reduct operator ... is meaningful: polyadic algebras with or without equality and substitution algebras. We also generalize this result to allow the case where m is an infinite ordinal. using quasipolyadic algebras in place of polyadic algebras (with or without equality). [ABSTRACT FROM AUTHOR]

We characterize the expressive power of extensions of Dependence Logic and Independence Logic by monotone generalized quantifiers in terms of quantifier extensions of existential second-order logic. [ABSTRACT FROM AUTHOR]

We prove that the strong polarized relation Due to image rights restrictions multiple line equation(s) cannot be graphically displayed. → Due to image rights restrictions multiple line equation(s) cannot be graphically displayed. is consistent with ZFC, for a singular μ which is a limit of measurable cardinals. [ABSTRACT FROM AUTHOR]

We study first-order logic with two variables FO² and establish a small substructure property. Similar to the small model property for FO² we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO² under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO² has the finite model property and is complete for non-deterministic exponential time, just as for plain FO². With two equivalence relations, FO² does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO² is undecidable. [ABSTRACT FROM AUTHOR]

We present sharpened lower bounds on the size of cut free proofs for first-order logic. Prior lower bounds for eliminating cuts from a proof established superexponential lower bounds as a stack of exponentials, with the height of the stack proportional to the maximum depth d of the formulas in the original proof. Our results remove the constant of proportionality, giving an exponential stack of height equal to d - O(1). The proof method is based on more efficiently expressing the Gentzen--Solovay cut formulas as low depth formulas. [ABSTRACT FROM AUTHOR]

We study relationships between certain algebraic properties of groups and rings definable in a first order structure or *-closed in a compact G-space. As a consequence, we obtain a few structural results about ω-categorical rings as well as about small, nm-stable compact G-rings, and we also obtain surprising relationships between some conjectures concerning small profinite groups. [ABSTRACT FROM AUTHOR]

The first-order theory of a string automatic structure is known to be decidable, but there are examples of string automatic structures with nonelementary first-order theories. We prove that the first-order theory of a string automatic structure of bounded degree is decidable in doubly exponential space (for injective automatic presentations, this holds even uniformly). This result is shown to be optimal since we also present a string automatic structure of bounded degree whose first-order theory is hard for 2EXPSPACE. We prove similar results also for tree automatic structures. These findings close the gaps left open in [28] by improving both the lower and the upper bounds. [ABSTRACT FROM AUTHOR]

We prove that given any first order formula Φ in the language L' = {+, ⋅, <, (fi)i∈I, (ci)i∈I}, where the fi are unary function symbols and the ci are constants, one can find an existential formula ψ such that Φ and ψ are equivalent in any L'-structure 〈ℝ, +, ⋅, <, (xci)i∈I, (ci)i∈I〉. [ABSTRACT FROM AUTHOR]

For a first-order formula φ(x; y) we introduce and study the characteristic sequence 〈Pn n < ω〉 of hypergraphs defined by Pn(yl, ..., y) ≔ (∃x) Λi≤n φ(x; yi). We show that combinatorial and classification theoretic properties of the characteristic sequence reflect classification theoretic properties of φ and vice versa. The main results are a characterization of NIP and of simplicity in terms of persistence of configurations in the characteristic sequence. Specifically, we show that some tree properties are detected by the presence of certain combinatorial configurations in the characteristic sequence while other properties such as instability and the independence property manifest themselves in the persistence of complicated configurations under localization. [ABSTRACT FROM AUTHOR]

We reformulate, in the context of continuous logic, an oscillation theorem proved by G. Hjorth and give a proof of the theorem in that setting which is similar to, but simpler than. Hjorth's original one. The point of view presented here clarifies the relation between Hjorth's theorem and first-order logic. [ABSTRACT FROM AUTHOR]

We show that there is a first order sentence φ(x;a,b,l) such that for every computable partial order 퓟 and Δ20-degree u > 0e, there are Δ20-enumeration degrees a ≤ u, b, and l such that 퓟 ≅ {x : φ(x;a,b,l)}. Allowing 퓟 to be a suitably defined standard model of arithmetic gives a parametefized interpretation of true arithmetic in the Δ20-enumeration degrees. Finally we show that there is a first order sentence that correctly identifies a subset of the standard models, which gives a parameterless interpretation of true arithmetic in the Δ20-enumeration degrees. [ABSTRACT FROM AUTHOR]

We construct a computable א0-catesorical structure whose first order theory is computably equivalent to the true first order theory of arithmetic. [ABSTRACT FROM AUTHOR]

As is well-known, the Bernays-Schönfinkel-Ramsey class of all prenex ∃* ∀* -sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are ∈ and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach, the remaining part of the decidability result being postponed to a forthcoming paper. [ABSTRACT FROM AUTHOR]

The undecidability of first-order logic implies that there is no computable bound on the length of shortest proofs of valid sentences of first-order logic. Some valid sentences can only have quite long proofs. How hard is it to prove such "hard" valid sentences? The polynomial time tractability of this problem would imply the fixed-parameter tractability of the parameterized problem that, given a natural number n in unary as input and a first-order sentence ψ as parameter, asks whether ψ has a proof of length ≤ n. As the underlying classical problem has been considered by Gödel we denote this problem by p-GÖDEL. We show that p-GÖDEL is not fixed-parameter tractable if DTIME(h0(1)) ≠ NTIME(h0(1)) for all time constructible and increasing functions h. Moreover we analyze the complexity of the construction problem associated with p-GÖDEL. [ABSTRACT FROM AUTHOR]

Continuous first-order logic has found interest among model theorists who wish to extend the classical analysis of "algebraic" structures (such as fields, group, and graphs) to various natural classes of complete metric structures (such as probability algebras, Hilbert spaces, and Banach spaces). With research in continuous first-order logic preoccupied with studying the model theory of this framework, we find a natural question calls for attention. Is there an interesting set of axioms yielding a completeness result? The primary purpose of this article is to show that a certain, interesting set of axioms does indeed yield a completeness result for continuous first-order logic. In particular, we show that in continuous first-order logic a set of formulae is (completely) satisfiable if (and only if) it is consistent. From this result it follows that continuous first-order logic also satisfies an approximated form of strong completeness, whereby Σ ⊩ ψ (if and) only if Σ ⊢ ψ ∸ 2-n for all n < ω. This approximated form of strong completeness asserts that if Σ ⊩ ψ, then proofs from Σ being finite, can provide arbitrarily better approximations of the truth of ψ. Additionally, we consider a different kind of question traditionally arising in model theory--that of decidability. When is the set of all consequences of a theory (in a countable, recursive language) recursive? Say that a complete theory T is decidable if for every sentence ψ, the value ψT is a recursive real, and moreover, uniformly computable from ψ. If T is incomplete, we say it is decidable if for every sentence ψ the real number ψoT is uniformly recursive from ψ, where ψoT is the maximal value of ψ consistent with T. As in classical first-order logic, it follows from the completeness theorem of continuous first-order logic that if a complete theory admits a recursive (or even recursively enumerable) axiomatization then it is decidable. [ABSTRACT FROM AUTHOR]

Let {M,X} |= ACA, be such that P(X), the collection of ail unbounded sets in X, admits a definable complete ultrafilter and let T be a theory extending first order arithmetic coded in X such that M thinks T is consistent. We prove that there is an end-extension N \= T of M such that the subsets of M coded in N are precisely those in X. As a special case we get that any Scott set with a definable ultrafilter coding a consistent theory T extending first order arithmetic is the standard system of a recursively saturated model of T. [ABSTRACT FROM AUTHOR]

A monadic formula ψ(Y) is a selector for a formula ϕ(Y) in a structure ... if there exists a unique subset P of ... which satisfies ψ and this P also satisfies ϕ. We show that for every ordinal α ≥ ωω there are formulas having no selector in the structure (α, <). For α < ω1, we decide which formulas have a selector in (α, <), and construct selectors for them. We deduce the impossibility of a full generalization of the Büchi-Landweber solvability theorem from (ω, <) to (ωω, <). We state a partial extension of that theorem to all countable ordinals. To each formula we assign a selection degree which measures "how difficult it is to select". We show that in a countable ordinal all non-selectable formulas share the same degree. [ABSTRACT FROM AUTHOR]

The logic L(Qu) extends first-order logic by a generalized form of counting quantifiers ("the number of elements satisfying… belongs to the set C"). This logic is investigated for structures with an injectively ω-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [6]. It is shown that, as in the case of automatic structures [21], also modulo-counting quantifiers as well as infinite cardinality quantifiers ("there are x many elements satisfying…") lead to decidable theories. For a structure of bounded degree with injective ω-automatic presentation, the fragment of L(Qu) that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (ω-automaticity and bounded degree) are necessary for this result to hold. [ABSTRACT FROM AUTHOR]

We give a novel application of algebraic logic to first order logic. A new, flexible construction is presented for representable but not completely representable atomic relation and cylindric algebras of dimension n (for finite n > 2) with the additional property that they are one-generated and the set of all n by n atomic matrices forms a cylindric basis. We use this construction to show that the classical Henkin-Orey omitting types theorem fails for the finite variable fragments of first order logic as long as the number of variables available is > 2 and we have a binary relation symbol in our language. We also prove a stronger result to the effect that there is no finite upper bound for the extra variables needed in the witness formulas. This result further emphasizes the ongoing interplay between algebraic logic and first order logic. [ABSTRACT FROM AUTHOR]

We define a higher order logic which has only a notion of sort rather than a notion of type, and which permits all terms of the untyped lambda calculus and allows the use of the Y combinator in writing recursive predicates. The consistency of the logic is maintained by a distinction between use and mention, as in Gilmore's logics. We give a consistent model theory, a proof system which is sound with respect to the model theory, and a cut-elimination proof for the proof system. We also give examples showing what formulas can and cannot be used in the logic. [ABSTRACT FROM AUTHOR]

A new axiom is proposed, the Ground Axiom, asserting that the universe is not a nontrivial set forcing extension of any inner model. The Ground Axiom is first-order expressible, and any model of ZFC has a class forcing extension which satisfies it. The Ground Axiom is independent of many well-known set-theoretic assertions including the Generalized Continuum Hypothesis, the assertion V=HOD that every set is ordinal definable, and the existence of measurable and supercompact cardinals. The related Bedrock Axiom, asserting that the universe is a set forcing extension of a model satisfying the Ground Axiom, is also first-order expressible, and its negation is consistent. [ABSTRACT FROM AUTHOR]

We consider successor-invariant first-order logic (FO + succ)inv, consisting of sentences involving an "auxiliary" binary relation S such that (U, S1) ⊨ Φ ⇔ (U, S2) ⊨ Φ for all finite structures U and successor relations S1, S2 on U. A successor-invariant sentence Φ has a well-defined semantics on finite structures U with no given successor relation: one simply evaluates Φ on (U, S) for an arbitrary choice of successor relation S. In this article, we prove that (FO + succ)inv is more expressive on finite structures than first-order logic without a successor relation. This extends similar results for order-invariant logic [8] and epsilon-invariant logic [10]. [ABSTRACT FROM AUTHOR]

Let A be the category of all reduced compact complex spaces. viewed as a multi-sorted first order structure, in the standard way. Let U be a sub-category of A, which is closed under the taking of products and analytic subsets, and whose morphisms include the projections. Under the assumption that Th(U) is unidimensional. we show that Morley rank is equal to Noetherian dimension, in any elementary extension of U. As a result, we are able to show that Morley degree is definable in Th(U). when Th(U) is unidimensional. [ABSTRACT FROM AUTHOR]

We prove a categoricity transfer theorem for tame abstract elementary classes. [ABSTRACT FROM AUTHOR]

Nominal logic is a variant of first-order logic in which abstract syntax with names and binding is formalized in terms of two basic operations: name-swapping and freshness. It relies on two important principles: equivariance (validity is preserved by name-swapping), and fresh name generation ("new" or fresh names can always be chosen). It is inspired by a particular class of models for abstract syntax trees involving names and binding, drawing on ideas from Fraenkel-Mostowski set theory: finite-support models in which each value can depend on only finitely many names. Although nominal logic is sound with respect to such models, it is not complete. In this paper we review nominal logic and show why finite-support models are insufficient both in theory and practice. We then identify (up to isomorphism) the class of models with respect to which nominal logic is complete: ideal-supported models in which the supports of values are elements of a proper ideal on the set of names. We also investigate an appropriate generalization of Herbrand models to nominal logic. After adjusting the syntax of nominal logic to include constants denoting names, we generalize universal theories to nominal-universal theories and prove that each such theory has an Herbrand model. [ABSTRACT FROM AUTHOR]

We show that infinite sets whose power-sets arc Dedekind-finite can only carry N-categorical first order structures. We identify other subclasses of this class of Dedekind-finite sets, and discuss their possible first order Structures. [ABSTRACT FROM AUTHOR]