Decidable properties of finite sets of equations in trivial languages

1984 ◽  
Vol 49 (4) ◽  
pp. 1333-1338
Author(s):  
Cornelia Kalfa

In [4] I proved that in any nontrivial algebraic language there are no algorithms which enable us to decide whether a given finite set of equations Σ has each of the following properties except P2 (for which the problem is open):P0(Σ) = the equational theory of Σ is equationally complete.P1(Σ) = the first-order theory of Σ is complete.P2(Σ) = the first-order theory of Σ is model-complete.P3(Σ) = the first-order theory of the infinite models of Σ is complete.P4(Σ) = the first-order theory of the infinite models of Σ is model-complete.P5(Σ) = Σ has the joint embedding property.In this paper I prove that, in any finite trivial algebraic language, such algorithms exist for all the above Pi's. I make use of Ehrenfeucht's result [2]: The first-order theory generated by the logical axioms of any trivial algebraic language is decidable. The results proved here are part of my Ph.D. thesis [3]. I thank Wilfrid Hodges, who supervised it.Throughout the paper is a finite trivial algebraic language, i.e. a first-order language with equality, with one operation symbol f of rank 1 and at most finitely many constant symbols.

1986 ◽  
Vol 51 (1) ◽  
pp. 79-87 ◽  
Author(s):  
Cornelia Kalfa

In this paper a general method of proving the undecidability of a property P, for finite sets Σ of equations of a countable algebraic language, is presented. The method is subsequently applied to establish the undecidability of the following properties, in almost all nontrivial such languages:1. The first-order theory generated by the infinite models of Σ is complete.2. The first-order theory generated by the infinite models of Σ is model-complete.3. Σ has the joint-embedding property.4. The first-order theory generated by the models of Σ with more than one element has the joint-embedding property.5. The first-order theory generated by the infinite models of Σ has the joint-embedding property.A countable algebraic language ℒ is a first-order language with equality, with countably many nonlogical symbols but without relation symbols, ℒ is trivial if it has at most one operation symbol, and this is of rank one. Otherwise, ℒ is nontrivial. An ℒ-equation is a sentence of the form , where φ and ψ are ℒ-terms. The set of ℒ-equations is denoted by Eqℒ. A set of sentences is said to have the joint-embedding property if any two models of it are embeddable in a third model of it.If P is a property of sets of ℒ-equations, the decision problem of P for finite sets of ℒ-equations is the problem of the existence or not of an algorithm for deciding whether, given a finite Σ ⊂ Eqℒ, Σ has P or not.


2018 ◽  
Vol 83 (04) ◽  
pp. 1595-1609 ◽  
Author(s):  
STEVEN GIVANT ◽  
HAJNAL ANDRÉKA

AbstractGivant [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).


1985 ◽  
Vol 50 (4) ◽  
pp. 953-972 ◽  
Author(s):  
Anne Bauval

This article is a rewriting of my Ph.D. Thesis, supervised by Professor G. Sabbagh, and incorporates a suggestion from Professor B. Poizat. My main result can be crudely summarized (but see below for detailed statements) by the equality: first-order theory of F[Xi]i∈I = weak second-order theory of F.§I.1. Conventions. The letter F will always denote a commutative field, and I a nonempty set. A field or a ring (A; +, ·) will often be written A for short. We shall use symbols which are definable in all our models, and in the structure of natural numbers (N; +, ·):— the constant 0, defined by the formula Z(x): ∀y (x + y = y);— the constant 1, defined by the formula U(x): ∀y (x · y = y);— the operation ∹ x − y = z ↔ x = y + z;— the relation of division: x ∣ y ↔ ∃ z(x · z = y).A domain is a commutative ring with unity and without any zero divisor.By “… → …” we mean “… is definable in …, uniformly in any model M of L”.All our constructions will be uniform, unless otherwise mentioned.§I.2. Weak second-order models and languages. First of all, we have to define the models Pf(M), Sf(M), Sf′(M) and HF(M) associated to a model M = {A; ℐ) of a first-order language L [CK, pp. 18–20]. Let L1 be the extension of L obtained by adjunction of a second list of variables (denoted by capital letters), and of a membership symbol ∈. Pf(M) is the model (A, Pf(A); ℐ, ∈) of L1, (where Pf(A) is the set of finite subsets of A. Let L2 be the extension of L obtained by adjunction of a second list of variables, a membership symbol ∈, and a concatenation symbol ◠.


2017 ◽  
Vol 82 (1) ◽  
pp. 35-61 ◽  
Author(s):  
ALLEN GEHRET

AbstractThe derivation on the differential-valued field Tlog of logarithmic transseries induces on its value group ${{\rm{\Gamma }}_{{\rm{log}}}}$ a certain map ψ. The structure ${\rm{\Gamma }} = \left( {{{\rm{\Gamma }}_{{\rm{log}}}},\psi } \right)$ is a divisible asymptotic couple. In [7] we began a study of the first-order theory of $\left( {{{\rm{\Gamma }}_{{\rm{log}}}},\psi } \right)$ where, among other things, we proved that the theory $T_{{\rm{log}}} = Th\left( {{\rm{\Gamma }}_{{\rm{log}}} ,\psi } \right)$ has a universal axiomatization, is model complete and admits elimination of quantifiers (QE) in a natural first-order language. In that paper we posed the question whether Tlog has NIP (i.e., the Non-Independence Property). In this paper, we answer that question in the affirmative: Tlog does have NIP. Our method of proof relies on a complete survey of the 1-types of Tlog, which, in the presence of QE, is equivalent to a characterization of all simple extensions ${\rm{\Gamma }}\left\langle \alpha \right\rangle$ of ${\rm{\Gamma }}$. We also show that Tlog does not have the Steinitz exchange property and we weigh in on the relationship between models of Tlog and the so-called precontraction groups of [9].


1977 ◽  
Vol 42 (1) ◽  
pp. 83-93
Author(s):  
Nobuyoshi Motohashi

In this paper, we shall define the “partially ordered interpretation” of a first order theory in another first order theory and state some recent results. Although an exact definition will be given in §4 below, we now give a brief outline. First of all, let us recall the “interpretations” defined by A. Tarski et al. in [17] and the “parametrical interpretations” defined by P. Hájek in [6], [7] and U. Felgner in [3]. Since “interpretations” can be considered as a special case of “parametrical interpretations”, we consider only the latter type of “interpretations”. A parametrical interpretation I of a first order language L in a consistent theory T′ (formulated in another first order language L′) consists of the following formulas:(i) a unary formula C(p) (i.e. a formula with one designated free variable p), which is used to denote the range of parameters,(ii) a binary formula U(p, x), which is intended to denote the pth universe for each parameter p,(iii) an (n + 1)-ary formula Fp(p, x1 …, xn) for each n-ary predicate symbol P in L,such that the formulas (∃p)C(p) and (∀p)(C(p)→(∃x)U(p, x)) are provable in T". Then, given a formula A in L and a parameter p, we define the interpretation Ip (A ) of A by I at p to be the formula which is obtained from A by replacing every atomic subformula P(*, …, *) in A by Fp(p, *,…,*), and relativizing every occurrence of quantifiers in A by U(p, * ). A sentence A in L is said to be I-provable in T′ if the sentence (∀p) (C(p)→ Ip(A)) is provable in T′. Then, it is obvious that every provable sentence in L is I-provable in T′. This is a basic result of “parametrical interpretations” and is used to prove the “consistency” of a theory T in L by showing that every axiom of T is I-provable in T′ when I is said to be a parametrical interpretation of T in T′. As is shown above, the word “interpretation” is used in the following three senses: interpretations of languages, interpretations of formulas and interpretations of theories. So, in this introduction we let the word “interpretation” denote “interpretation of languages”, for short.


Author(s):  
John L. Bell

The chapter begins with an introduction describing the development of categorical logic from the 1960s. The next section, `Categories and Deductive Systems’, describes the relationship between categories and propositional logic, while the ensuing section, `Functorial Semantics’, is devoted to Lawvere’s provision of the first-order theory of models with a categorical formulation. In the section `Local Set Theories and Toposes’ the categorical counterparts—toposes—to higher-order logic are introduced, along with their associated theories—local set theories. In the section `Models of First-Order Languages in Categories’ the idea of an interpretation of a many-sorted first-order language is introduced, along with the concept of generic model of a theory formulated in such a language. The chapter concludes with the section `Models in Toposes’, wherein is introduced the concept of a first-order geometric theory and its associated classifying topos containing a generic model of the theory.


1983 ◽  
Vol 48 (2) ◽  
pp. 329-338 ◽  
Author(s):  
William P. Hanf ◽  
Dale Myers

AbstractAssociated with each first-order theory is a Boolean algebra of sentences and a Boolean space of models. Homomorphisms between the sentence algebras correspond to continuous maps between the model spaces. To what do recursive homomorphisms correspond? We introduce axiomatizable maps as the appropriate dual. For these maps we prove a Cantor-Bernstein theorem. Duality and the Cantor-Bernstein theorem are used to show that the Boolean sentence algebras of any two undecidable languages or of any two functional languages are recursively isomorphic where a language is undecidable iff it has at least one operation or relation symbol of two or more places or at least two unary operation symbols, and a language is functional iff it has exactly one unary operation symbol and all other symbols are for unary relations, constants, or propositions.


Axioms ◽  
2021 ◽  
Vol 10 (2) ◽  
pp. 119
Author(s):  
Marcoen J. T. F. Cabbolet

It is well known that Zermelo-Fraenkel Set Theory (ZF), despite its usefulness as a foundational theory for mathematics, has two unwanted features: it cannot be written down explicitly due to its infinitely many axioms, and it has a countable model due to the Löwenheim–Skolem theorem. This paper presents the axioms one has to accept to get rid of these two features. For that matter, some twenty axioms are formulated in a non-classical first-order language with countably many constants: to this collection of axioms is associated a universe of discourse consisting of a class of objects, each of which is a set, and a class of arrows, each of which is a function. The axioms of ZF are derived from this finite axiom schema, and it is shown that it does not have a countable model—if it has a model at all, that is. Furthermore, the axioms of category theory are proven to hold: the present universe may therefore serve as an ontological basis for category theory. However, it has not been investigated whether any of the soundness and completeness properties hold for the present theory: the inevitable conclusion is therefore that only further research can establish whether the present results indeed constitute an advancement in the foundations of mathematics.


Sign in / Sign up

Export Citation Format

Share Document