We discuss first order theories in which individual concepts are admitted as mathematical objects along with the things that reify them. This allows very straightforward formalizations of knowledge, belief, wanting, and necessity in ordinary first order logic without modal operators. Applications are given in philosophy and in artificial intelligence. We do not treat general concepts, and we do not present any full axiomatizations but rather show how various facts can be expressed.

In this paper first order theories for nonmonotone inductive definitions are introduced, and a proof-theoretic analysis for such theories based on combined operator forms a la Richter with recursively inaccessible and Mahlo closure ordinals is given.

A maximal chain in a tree is called a path, and a tree is called bounded when all its paths contain leaves. This paper concerns itself with first-order theories of bounded trees. We establish some sufficient conditions for the existence of bounded end-extensions that are also partial elementary extensions of a given tree. As an application of tree boundedness, we obtain a conditional axiomatisation of the first-order theory of the class of trees whose paths are (...) all isomorphic to some ordinal \, given the first-order theories of certain classes of bounded trees. (shrink)

Features are unary operators used to build record-like expressions. The resulting term algebras are encountered in linguistic computation and knowledge representation. We present a general description of feature logic and of a slightly restricted version, called record logic. It is shown that every first-order theory can be faithfully interpreted in a record logic with various additional axioms. This fact is used elsewhere [15] to extend a result of Tarski and Givant [14] on expressing first order (...) theories in relation algebra. (shrink)

Some first-order theories of divisible ℓ-groups are well known, for example the theory of the totally ordered ones and the theories of the projectable ones , Lattice-ordered Groups, Kluwer Academic Press, Dordrecht, 1989, pp. 41–79). In this paper we study some theories of nonprojectable divisible ℓ-groups, the simplest example of which is . We introduce a generalization of the projectability property . We prove that the class of r-projectable special-valued divisible ℓ-groups is an elementary class and give (...) a classification of its completions. (shrink)

In this paper the modal operator "x is provable in Peano Arithmetic" is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.

In this paper a first order theory for the logics defined through literal paraconsistent-paracomplete matrices is developed. These logics are intended to model situations in which the ground level information may be contradictory or incomplete, but it is treated within a classical framework. This means that literal formulas, i.e. atomic formulas and their iterated negations, may behave poorly specially regarding their negations, but more complex formulas, i.e. formulas that include a binary connective are well behaved. This situation (...) may and does appear for instance in data bases. (shrink)

A Dedekind Algebra is an ordered pair (B,h) where B is a non-empty set and h is an injective unary function on B. Each Dedekind algebra can be decomposed into a family of disjoint, countable subalgebras called configurations of the Dedekind algebra. There are N0 isomorphism types of configurations. Each Dedekind algebra is associated with a cardinal-valued function on omega called its configuration signature. The configuration signature of a Dedekind algebra counts the number of configurations in the decomposition of the (...) algebra in each isomorphism type.The configuration signature of a Dedekind algebra encodes the structure of that algebra in the sense that two Dedekind algebras are isomorphic iff their configuration signatures are identical. Configuration signatures are used to establish various results in the first-order model theory of Dedekind algebras. These include categoricity results for the first-order theories of Dedekind algebras and existence and uniqueness results for homogeneous, universal and saturated Dedekind algebras. Fundamental to these results is a condition on configuration signatures that is necessary and sufficient for elementary equivalence. (shrink)

We investigate first order sentences valid in completions of a given partial algebraic structure - a partial model. We give semantic and syntactic description of the set of all sentences valid in every completion of the given partial model - first order theory of this model.

The standard theory of logic programming is not applicable to Prolog programs even not to pure code. Modifying the theory to take account of reality more is the motivation of this article. For this purpose we introduce the ℓ-completion and the inductive extension of a logic program. Both are first-order theories in a language with operators for success, failure and termination of goals. The ℓ-completion of a logic program is a sound and complete axiomatization of the (...) Prolog depth-first search under certain natural conditions; the inductive extension of the ℓ-completion is a suitable theory for proving termination and equivalence of pure Prolog programs with negation. (shrink)

This paper contains a formal theory of functional parthood. Since the relation of functional parthood is defined here by means of the notion of design, the theory of functional parthood turns out to be a theory of design. The formal theory of design I defend here is a result of introducing a number of constraints that are to express the rational aspects of designing practice. The ontological background for the theory is provided by a conception (...) of states of affairs. The theory is accompanied with a formal model. I prove that the theory is sound and complete with respect to this model. (shrink)

We consider R-torsionfree modules over group rings RG, where R is a Dedekind domain and G is a finite group. In the first part of the paper [4] we compared the theory T of all R-torsionfree RG-modules and the theory T0 of RG-lattices , and we realized that they are almost always different. Now we compare their behaviour with respect to decidability, when RG-lattices are of finite, or wild representation type.

We consider R-torsionfree modules over group rings RG, where R is a Dedekind domain and G is a finite group. In the first part of the paper [4] we compared the theory T of all R-torsionfree RG-modules and the theory T0 of RG-lattices , and we realized that they are almost always different. Now we compare their behaviour with respect to decidability, when RG-lattices are of finite, or wild representation type.

We study the groups Gal L and Gal KP, and the associated equivalence relations EL and EKP, attached to a first order theory T. An example is given where EL≠ EKP. It is proved that EKP is the composition of EL and the closure of EL. Other examples are given showing this is best possible.

By a classifying topos for a first-order theory , we mean a topos such that, for any topos models of in correspond exactly to open geometric morphisms → . We show that not every first-order theory has a classifying topos in this sense, but we characterize those which do by an appropriate ‘smallness condition’, and we show that every Grothendieck topos arises as the classifying topos of such a theory. We also show that (...) every first-order theory has a conservative extension to one which possesses a classifying topos, and we obtain a Heyting-valued completeness theorem for infinitary first-order logic. (shrink)

The undecidability of the first-order theory of diagonalizable algebras is shown here.

It is shown by Parsons [2] that the first-order fragment of Frege's logical system in the Grundgesetze der Arithmetic is consistent. In this note we formulate and prove a stronger version of this result for arbitrary first-order theories. We also show that a natural attempt to further strengthen our result runs afoul of Tarski's theorem on the undefinability of truth.

For every sequence |p n } n of formulas of Peano ArithmeticPA with, every formulaA of the first-order theory diagonalizable algebras, we associate a formula 0 A, called the value ofA inPA with respect to the interpretation. We show that, ifA is true in every diagonalizable algebra, then, for every, 0 A is a theorem ofPA.

We study the first-order theory of polynomial rings over a GCD domain and of the ring of formal entire functions over a non-Archimedean field in the language $\{ 1, +, \bot \}$. We show that these structures interpret the first-order theory of the semi-ring of natural numbers. Moreover, this interpretation depends only on the characteristic of the original ring, and thus we obtain uniform undecidability results for these polynomial and entire functions rings of a (...) fixed characteristic. This work enhances results of Raphael Robinson on essential undecidability of some polynomial or formal power series rings in languages that contain no symbols related to the polynomial or power series ring structure itself. (shrink)

The aim of this paper is to introduce a formal system STW of self-referential truth, which extends the classical first-order theory of pure combinators with a truth predicate and certain approximation axioms. STW naturally embodies the mechanisms of general predicate application/abstraction on a par with function application/abstraction; in addition, it allows non-trivial constructions, inspired by generalized recursion theory. As a consequence, STW provides a smooth inner model for Myhill's systems with levels of implication.

In the paper we formulate a sufficient criterion in order for the first order theory with finite set of axioms to be represented by definitions in predicate calculus. We prove the corresponding theorem. According to this criterion such theories as the theory of equivalence relation, the theory of partial order and many theories based on the equality relation with finite set of functional and predicate symbols are represented by definitions in the first- (...) class='Hi'>order predicate calculus without equality. (shrink)

We introduce a general notion of semantic structure for first-order theories, covering a variety of constructions such as Tarski and Kripke semantics, and prove that, over Zermelo–Fraenkel set theory, the completeness of such semantics is equivalent to the Boolean prime ideal theorem. Using a result of McCarty, we conclude that the completeness of Kripke semantics is equivalent, over intuitionistic Zermelo–Fraenkel set theory, to the Law of Excluded Middle plus BPI. Along the way, we also prove the (...) equivalence, over ZF, between BPI and the completeness theorem for Kripke semantics for both first-order and propositional theories. (shrink)

We say that a first order sentence A defines a graph G if A is true on G but false on any graph non-isomorphic to G. Let L ) denote the minimum length of such a sentence. We define the succinctness function s ) to be the minimum L ) over all graphs on n vertices.We prove that s and q may be so small that for no general recursive function f we can have f)≥n for all n. (...) However, for the function q*=maxi≤nq, which is the least nondecreasing function bounding q from above, we have q*=)log*n, where log*n equals the minimum number of iterations of the binary logarithm sufficient to lower n to 1 or below.We show an upper bound qshrink)

We provide first-order axioms for the theories of finite trees with bounded branching and finite trees with arbitrary (finite) branching. The signature is chosen to express, in a natural way, those properties of trees most relevant to linguistic theories. These axioms provide a foundation for results in linguistics that are based on reasoning formally about such properties. We include some observations on the expressive power of these theories relative to traditional language complexity classes.

In this paper, some basic properties of automorphisms of first order languages and some examples are presented. In particular, an omitting types theorem is proved.

Khoussainov and Nerode [14] posed various open questions on model-theoretic properties of automatic structures. In this work we answer some of these questions by showing the following results: There is an uncountably categorical but not countably categorical theory for which only the prime model is automatic; There are complete theories with exactly 3,4,5,…3,4,5,… countable models, respectively, and every countable model is automatic; There is a complete theory for which exactly 2 models have an automatic presentation; If LOGSPACE=PLOGSPACE=P then (...) there is an uncountably categorical but not countably categorical theory for which the prime model does not have an automatic presentation but all the other countable models are automatic; There is a complete theory with countably many countable models for which the saturated model has an automatic presentation but the prime model does not have one. (shrink)

In this paper we study the idea of theories with containers, like sets, pairs, sequences. We provide a modest framework to study such theories. We prove two concrete results. First, we show that first-order theories of finite signature that have functional non-surjective ordered pairing are definitionally equivalent to extensions in the same language of the basic theory of non-surjective ordered pairing. Second, we show that a first-order theory of finite signature is sequential (is (...) a theory of sequences) iff it is definitionally equivalent to an extension in the same language of a system of weak set theory called WS. (shrink)

What has been the historical relationship between set theory and logic? On the one hand, Zermelo and other mathematicians developed set theory as a Hilbert-style axiomatic system. On the other hand, set theory influenced logic by suggesting to Schröder, Löwenheim and others the use of infinitely long expressions. The questions of which logic was appropriate for set theory - first-order logic, second-order logic, or an infinitary logic - culminated in a vigorous exchange between (...) Zermelo and Gödel around 1930. (shrink)

This paper is part of a general programme of developing and investigating particular first- order modal theories. In the paper, a modal theory of propositions is constructed under the assumption that there are genuinely singular propositions, ie. ones that contain individuals as constituents. Various results on decidability, axiomatizability and definability are established.

In this paper we introduce the notion of a first order topological structure, and consider various possible conditions on the complexity of the definable sets in such a structure, drawing several consequences thereof.Our aim is to develop, for a restricted class of unstable theories, results analogous to those for stable theories. The “material basis” for such an endeavor is the analogy between the field of real numbers and the field of complex numbers, the former being a “nicely behaved” (...) unstable structure and the latter the archetypal stable structure. In this sense we try here to situate our work ono-minimal structures [PS] in a general topological context. Note, however, that thep-adic numbers, and structures definable therein, will also fit into our analysis.In the remainder of this section we discuss several ways of studying topological structures model-theoretically. Eventually we fix on the notion of a structure in which the topology is “explicitly definable” in the sense of Flum and Ziegler [FZ]. In §2 we introduce the hypothesis that every definable set is a Boolean combination of definable open sets. In §3 we introduce a “dimension rank” on definable sets. In §4 we consider structures on which this rank is defined, and for which also every definable set has a finite number of definably connected definable components. We show that prime models over sets exist under such conditions. (shrink)

We study first-order concatenation theory with bounded quantifiers. We give axiomatizations with interesting properties, and we prove some normal-form results. Finally, we prove a number of decidability and undecidability results.

We study probabilistic characterisation of a random model of a finite set of first order axioms. Given a set of first order axioms.

We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions . As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. (...) In addition, we show that the full axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo-Fraenkel set theory. (shrink)

We show how to interpret the language of first-order set theory in an elementary topos endowed with, as extra structure, a directed structural system of inclusions (dssi). As our main result, we obtain a complete axiomatization of the intuitionistic set theory validated by all such interpretations. Since every elementary topos is equivalent to one carrying a dssi, we thus obtain a first-order set theory whose associated categories of sets are exactly the elementary toposes. (...) In addition, we show that the full axiom of Separation is validated whenever the dssi is superdirected. This gives a uniform explanation for the known facts that cocomplete and realizability toposes provide models for Intuitionistic Zermelo—Fraenkel set theory (IZF). (shrink)