Jane Bridge. Beginning model theory. The completeness theorem and some consequences. Oxford logic guides. Clarendon Press, Oxford1977, viii + 143 pp.

1979 ◽  
Vol 44 (2) ◽  
pp. 283-283
Author(s):  
John T. Baldwin
1968 ◽  
Vol 33 (1) ◽  
pp. 1-7 ◽  
Author(s):  
Richmond H. Thomason

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.


2006 ◽  
Vol 71 (3) ◽  
pp. 863-880 ◽  
Author(s):  
Petr Hájek ◽  
Petr Cintula

AbstractIn the last few decades many formal systems of fuzzy logics have been developed. Since the main differences between fuzzy and classical logics lie at the propositional level, the fuzzy predicate logics have developed more slowly (compared to the propositional ones). In this text we aim to promote interest in fuzzy predicate logics by contributing to the model theory of fuzzy predicate logics. First, we generalize the completeness theorem, then we use it to get results on conservative extensions of theories and on witnessed models.


1996 ◽  
Vol 2 (2) ◽  
pp. 127-158 ◽  
Author(s):  
Leon Henkin

§1. Introduction. This paper deals with aspects of my doctoral dissertation which contributed to the early development of model theory. What was of use to later workers was less the results of my thesis, than the method by which I proved the completeness of first-order logic—a result established by Kurt Gödel in his doctoral thesis 18 years before.The ideas that fed my discovery of this proof were mostly those I found in the teachings and writings of Alonzo Church. This may seem curious, as his work in logic, and his teaching, gave great emphasis to the constructive character of mathematical logic, while the model theory to which I contributed is filled with theorems about very large classes of mathematical structures, whose proofs often by-pass constructive methods.Another curious thing about my discovery of a new proof of Gödel's completeness theorem, is that it arrived in the midst of my efforts to prove an entirely different result. Such “accidental” discoveries arise in many parts of scientific work. Perhaps there are regularities in the conditions under which such “accidents” occur which would interest some historians, so I shall try to describe in some detail the accident which befell me.A mathematical discovery is an idea, or a complex of ideas, which have been found and set forth under certain circumstances. The process of discovery consists in selecting certain input ideas and somehow combining and transforming them to produce the new output ideas. The process that produces a particular discovery may thus be represented by a diagram such as one sees in many parts of science; a “black box” with lines coming in from the left to represent the input ideas, and lines going out to the right representing the output. To describe that discovery one must explain what occurs inside the box, i.e., how the outputs were obtained from the inputs.


1978 ◽  
Vol 43 (4) ◽  
pp. 659-666
Author(s):  
Judy Green

An analogue of a theorem of Sierpinski about the classical operation () provides the motivation for studying κ-Suslin logic, an extension of Lκ+ω which is closed under a propositional connective based on (). This theorem is used to obtain a complete axiomatization for κ-Suslin logic and an upper bound on the κ-Suslin accessible ordinals (for κ = ω these results are due to Ellentuck [E]). It also yields a weak completeness theorem which we use to generalize a result of Barwise and Kunen [B-K] and show that the least ordinal not H(κ+) recursive is the least ordinal not κ-Suslin accessible.We assume familiarity with lectures 3, 4 and 10 of Keisler's Model theory for infinitary logic [Ke]. We use standard notation and terminology including the following.Lκ+ω is the logic closed under negation, finite quantification, and conjunction and disjunction over sets of formulas of cardinality at most κ. For κ singular, conjunctions and disjunctions over sets of cardinality κ can be replaced by conjunctions and disjunctions over sets of cardinality less than κ so that we can (and will in §2) assume the formation rules of Lκ+ω allow conjunctions and disjunctions only over sets of cardinality strictly less than κ whenever κ is singular.


Author(s):  
Shawn Hedman

We continue our study of Model Theory. This is the branch of logic concerned with the interplay between sentences of a formal language and mathematical structures. Primarily, Model Theory studies the relationship between a set of first-order sentences T and the class Mod(T) of structures that model T. Basic results of Model Theory were proved in the previous chapter. For example, it was shown that, in first-order logic, every model has a theory and every theory has a model. Put another way, T is consistent if and only if Mod(T) is nonempty. As a consequence of this, we proved the Completeness theorem. This theorem states that T ├ φ if and onlyif M ╞ φ for each M in Mod(T). So to study a theory T, we can avoid the concept of ├ and the methods of deduction introduced in Chapter 3, and instead work with the concept of ╞ and analyze the class Mod(T). More generally, we can go back and forth between the notions on the left side of the following table and their counterparts on the right. Progress in mathematics is often the result of having two or more points of view that are shown to be equivalent. A prime example is the relationship between the algebra of equations and the geometry of the graphs defined by the equations. Combining these two points of view yield concepts and results that would not be possible in either geometry or algebra alone. The Completeness theorem equates the two points of view exemplified in the above table. Model Theory exploits the relationship between these two points of view to investigate mathematical structures. First-order theories serve as our objects of study in this chapter. A first-order theory may be viewed as a consistent set of sentences T or as an elementary class of structures Mod(T). We shall present examples of theories and consider properties that the theories mayor may not possess such as completeness, categoricity, quantifier-elimination, and model-completeness. The properties that a theory possesses shed light on the structures that model the theory. We analyze examples of first-order structures including linear orders, vector spaces, the random graph, and the complex numbers.


2003 ◽  
Vol 68 (4) ◽  
pp. 1109-1144
Author(s):  
Timothy J. Carlson

AbstractThe theory of ranked partial structures allows a reinterpretation of several of the standard results of model theory and first-order logic and is intended to provide a proof-theoretic method which allows for the intuitions of model theory. A version of the downward Löwenheim-Skolem theorem is central to our development. In this paper we will present the basic theory of ranked partial structures and their logic including an appropriate version of the completeness theorem.


2010 ◽  
Vol 75 (1) ◽  
pp. 168-190 ◽  
Author(s):  
Itaï Ben Yaacov ◽  
Arthur Paul Pedersen

AbstractContinuous 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 anapproximatedform of strong completeness, whereby Σ⊧φ(if and) only if Σ⊢φ∸2−nfor alln < ω. 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 theoryTisdecidableif for every sentenceφ, the valueφTis a recursive real, and moreover, uniformly computable fromφ. IfTis incomplete, we say it is decidable if for every sentenceφthe real numberφTois uniformly recursive fromφ, whereφTois the maximal value ofφconsistent withT. 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.


1972 ◽  
Vol 37 (1) ◽  
pp. 81-89 ◽  
Author(s):  
Thomas J. Grilliot

Omitting-types theorems have been useful in model theory to construct models with special characteristics. For instance, one method of proving the ω-completeness theorem of Henkin [10] and Orey [20] involves constructing a model that omits the type {x ≠ 0, x ≠ 1, x ≠ 2,···} (i.e., {x ≠ 0, x ≠ 1, x ≠ 2,···} is not satisfiable in the model). Our purpose in this paper is to illustrate uses of omitting-types theorems in recursion theory. The Gandy-Kreisel-Tait Theorem [7] is the most well-known example. This theorem characterizes the class of hyperarithmetical sets as the intersection of all ω-models of analysis (the so-called hard core of analysis). The usual way to prove that a nonhyperarithmetical set does not belong to the hard core is to construct an ω-model of analysis that omits the type representing the set (Application 1). We will find basis results for and s — sets that are stronger than results previously known (Applications 2 and 3). The question of how far the natural hierarchy of hyperjumps extends was first settled by a forcing argument (Sacks) and subsequently by a compactness argument (Kripke, Richter). Another problem solved by a forcing argument (Sacks) and then by a compactness argument (Friedman-Jensen) was the characterization of the countable admissible ordinals as the relativized ω1's. Using omitting-types technique, we will supply a third kind of proof of these results (Applications 4 and 5). S. Simpson made a significant contribution in simplifying the proof of the latter result, with the interesting side effect that Friedman's result on ordinals in models of set theory is immediate (Application 6). One approach to abstract recursiveness and hyperarithmeticity on a countable set is to tenuously identify the set with the natural numbers. This approach is equivalent to other approaches to abstract recursion (Application 7). This last result may also be proved by a forcing method.


F. William Lawvere. Introduction to part I. Model theory and topoi, A collection of lectures by various authors, edited by F. W. Lawvere, C. Maurer, and G. C. Wraith, Lecture notes in mathematics, vol. 445, Springer-Verlag, Berlin, Heidelberg, and New York, 1975, pp. 3–14. - Orville Keane. Abstract Horn theories. Model theory and topoi, A collection of lectures by various authors, edited by F. W. Lawvere, C. Maurer, and G. C. Wraith, Lecture notes in mathematics, vol. 445, Springer-Verlag, Berlin, Heidelberg, and New York, 1975, pp. 15–50. - Hugo Volger. Completeness theorem for logical categories. Model theory and topoi, A collection of lectures by various authors, edited by F. W. Lawvere, C. Maurer, and G. C. Wraith, Lecture notes in mathematics, vol. 445, Springer-Verlag, Berlin, Heidelberg, and New York, 1975, pp. 51–86. - Hugo Volger. Logical categories, semantical categories and topoi. Model theory and topoi, A collection of lectures by various authors, edited by F. W. Lawvere, C. Maurer, and G. C. Wraith, Lecture notes in mathematics, vol. 445, Springer-Verlag, Berlin, Heidelberg, and New York, 1975, pp. 87–100. - G. C. Wraith. Lectures on elementary topoi. Model theory and topoi, A collection of lectures by various authors, edited by F. W. Lawvere, C. Maurer, and G. C. Wraith, Lecture notes in mathematics, vol. 445, Springer-Verlag, Berlin, Heidelberg, and New York, 1975, pp. 114–206. - Gerhard Osius. Logical and set theoretical tools in elementary topoi. Model theory and topoi, A collection of lectures by various authors, edited by F. W. Lawvere, C. Maurer, and G. C. Wraith, Lecture notes in mathematics, vol. 445, Springer-Verlag, Berlin, Heidelberg, and New York, 1975, pp. 297–346. - Gerhard Osius. A note on Kripke–Joyal semantics for the internal language of topoi. Model theory and topoi, A collection of lectures by various authors, edited by F. W. Lawvere, C. Maurer, and G. C. Wraith, Lecture notes in mathematics, vol. 445, Springer-Verlag, Berlin, Heidelberg, and New York, 1975, pp. 349–354.

1981 ◽  
Vol 46 (1) ◽  
pp. 158-161
Author(s):  
M. E. Szabo

Sign in / Sign up

Export Citation Format

Share Document