Alexander Abian. On the solvability of infinite systems of Boolean polynomial equations. Colloquium mathematicum, vol. 21 (1970), pp. 27–30. - Alexander Abian. Generalized completeness theorem and solvability of systems of Boolean polynomial equations. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 16 (1970), pp. 263–264. - Paul D. Bacsich. Injectivity in model theory. Colloquium mathematicum, vol. 25 (1972), pp. 165–176. - S. Bulman-Fleming. On equationally compact semilattices. Algebra universalis (Basel), vol. 2 no. 2 (1972), pp. 146–151. - G. Grätzer and H. Lakser. Equationally compact semilattices. Colloquium mathematicum, vol. 20 (1969), pp. 27–30. - David K. Haley. On compact commutative Noetherian rings. Mathematische Annalen, vol. 189 (1970), pp. 272–274. - Ralph McKenzie. ℵ1-incompactness of Z. Colloquium mathematicum, vol. 23 (1971), pp. 199–202. - Jan Mycielski. Some compactifications of general algebras. Colloquium mathematicum, vol. 13 no. 1 (1964), pp. 1–9. See Errata on page 281 of next paper. - Jan Mycielski and C. Ryll-Nardzewski. Equationally compact algebras II. Fundamenta mathematicae, vol. 61 (1968), pp. 271–281. Errata, Fundamenta mathematicae, vol. 62 (1968), p. 309. - L. Pacholski and B. Wȩglorz. Topologically compact structures and positive formulas. Colloquium mathematicum, vol. 19 (1968), pp. 37–42. - B. Wȩglorz. Compactness of algebraic systems. Bulletin de l'Academie Polonaise des Sciences, Série des sciences mathématiques, astronomiques et physiques, vol. 13 (1965), pp. 705–706. - B. Wȩglorz. Equationally compact algebras(I). Fundamenta mathematicae, vol. 59 (1966), pp. 289–298. - B. Wȩglorz. Equationally compact algebras (III). Fundamenta mathematicae, vol. 60 (1967), pp. 89–93. - B. Wȩglorz. Completeness and compactness of lattices. Colloquium mathematicum, vol. 16 (1967), pp. 243–248. - B. Wȩglorz and A. Wojciechowska. Summability of pure extensions of relational structures. Colloquium mathematicum, vol. 19 (1968), pp. 27–35. - Günter H. Wenzel. Subdirect irreducibility and equational compactness of unary algebras 〈A; f〉. Archiv der Mathematik, vol. 21 (1970), pp. 256–264. - Günter H. Wenzel. On -atomic compact relational systems. Mathematische Annalen, vol. 194 (1971), pp. 12–18.

1975 ◽  
Vol 40 (1) ◽  
pp. 88-92 ◽  
Author(s):  
Walter Taylor
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Noetherian Rings ◽  
Polynomial Equations ◽  
Algebraic Systems ◽  
Relational Structures ◽  
Infinite Systems ◽  
Subdirect Irreducibility ◽  
Relational Systems ◽  
Equational Compactness

Weakly atomic-compact relational structures

1971 ◽  
Vol 36 (1) ◽  
pp. 129-140 ◽  
Author(s):  
G. Fuhrken ◽  
W. Taylor
Keyword(s):  
Abelian Group ◽  
Model Theory ◽  
Compact Abelian Group ◽  
Finite Subset ◽  
Relational Structure ◽  
Similarity Type ◽  
First Order ◽  
Relational Structures ◽  
Order Language ◽  
Weakly Atomic

A relational structure is called weakly atomic-compact if and only if every set Σ of atomic formulas (taken from the first-order language of the similarity type of augmented by a possibly uncountable set of additional variables as “unknowns”) is satisfiable in whenever every finite subset of Σ is so satisfiable. This notion (as well as some related ones which will be mentioned in §4) was introduced by J. Mycielski as a generalization to model theory of I. Kaplansky's notion of an algebraically compact Abelian group (cf. [5], [7], [1], [8]).

Subdirect irreducibility and equational compactness in unary algebras

1970 ◽  
Vol 21 (1) ◽  
pp. 256-264 ◽  
Author(s):  
G�nter H. Wenzel
Keyword(s):  
Subdirect Irreducibility ◽  
Equational Compactness

On the strong semantical completeness of the intuitionistic predicate calculus

1968 ◽  
Vol 33 (1) ◽  
pp. 1-7 ◽  
Author(s):  
Richmond H. Thomason
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Predicate Calculus ◽  
First Order ◽  
Semantic Tableaux ◽  
Weak Completeness ◽  
Skolem Theorem ◽  
Completeness Theorems

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.

SMT-based verification of data-aware processes: a model-theoretic approach

2020 ◽  
Vol 30 (3) ◽  
pp. 271-313
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Model Theory ◽  
Satisfiability Modulo Theories ◽  
Theoretic Approach ◽  
Model Checker ◽  
Present Contribution ◽  
Relational Systems ◽  
Infinite State Systems ◽  
Algorithmic Techniques ◽  
The One ◽  
Infinite State

AbstractIn recent times, satisfiability modulo theories (SMT) techniques gained increasing attention and obtained remarkable success in model-checking infinite-state systems. Still, we believe that whenever more expressivity is needed in order to specify the systems to be verified, more and more support is needed from mathematical logic and model theory. This is the case of the applications considered in this paper: we study verification over a general model of relational, data-aware processes, to assess (parameterized) safety properties irrespectively of the initial database (DB) instance. Toward this goal, we take inspiration from array-based systems and tackle safety algorithmically via backward reachability. To enable the adoption of this technique in our rich setting, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems and represents the main original contribution of this paper. In this way, we pursue a twofold purpose. On the one hand, we isolate three notable classes for which backward reachability terminates, in turn witnessing decidability. Two of such classes relate our approach to conditions singled out in the literature, whereas the third one is genuinely novel. On the other hand, we are able to exploit SMT technology in implementations, building on the well-known MCMT (Model Checker Modulo Theories) model checker for array-based systems and extending it to make all our foundational results fully operational. All in all, the present contribution is deeply rooted in the long-standing tradition of the application of model theory in computer science. In particular, this paper applies these ideas in an original mathematical context and shows how these techniques can be used for the first time to empower algorithmic techniques for the verification of infinite-state systems based on arrays, so as to make such techniques applicable to the timely, challenging settings of data-aware processes.

On theories and models in fuzzy predicate logics

2006 ◽  
Vol 71 (3) ◽  
pp. 863-880 ◽  
Author(s):  
Petr Hájek ◽  
Petr Cintula
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Fuzzy Logics ◽  
Formal Systems ◽  
Conservative Extensions

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.

scholarly journals Strong quasi-ordered residuated system

2021 ◽  
Vol 5 (1) ◽  
pp. 73-79
Author(s):  
Daniel A. Romano ◽  
Keyword(s):  
Upper Bound ◽  
Order Relation ◽  
Algebraic Systems ◽  
Relational Systems ◽  
Quasi Order

The concept of residuated relational systems ordered under a quasi-order relation was introduced in 2018 by S. Bonzio and I. Chajda. In such algebraic systems, we have introduced and developed the concepts of implicative and comparative filters. In addition, we have shown that every comparative filter is an implicative filter at the same time and that converse it does not have to be. In this article, as a continuation of previous research, we introduce the concept of strong quasi-ordered residuated systems and we show that in such systems implicative and comparative filters coincide. In addition, we show that in such systems the concept of least upper bound for any two pair of elements can be determined.

The Discovery of My Completeness Proofs

1996 ◽  
Vol 2 (2) ◽  
pp. 127-158 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Model Theory ◽  
Scientific Work ◽  
Completeness Theorem ◽  
Large Classes ◽  
Mathematical Structures ◽  
First Order ◽  
Kurt Gödel ◽  
Gödel’S Completeness Theorem ◽  
The Right ◽  
Mathematical Discovery

§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.

κ-Suslin logic

1978 ◽  
Vol 43 (4) ◽  
pp. 659-666
Author(s):  
Judy Green
Keyword(s):  
Model Theory ◽  
Upper Bound ◽  
Completeness Theorem ◽  
Infinitary Logic ◽  
Complete Axiomatization ◽  
Standard Notation ◽  
Weak Completeness

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.

Sign in / Sign up

Export Citation Format

Share Document